1<!doctype html> 2<html lang="en" dir="ltr" class="plugin-pages plugin-id-default" data-has-hydrated="false"> 3<head> 4<meta charset="UTF-8"> 5<meta name="generator" content="Docusaurus v3.10.2"> 6<title data-rh="true">Caesar â Verification infrastructure for probabilistic programs</title><meta data-rh="true" name="viewport" content="width=device-width,initial-scale=1"><meta data-rh="true" name="twitter:card" content="summary_large_image"><meta data-rh="true" property="og:image" content="https://www.caesarverifier.org/img/social-card-v2.png"><meta data-rh="true" name="twitter:image" content="https://www.caesarverifier.org/img/social-card-v2.png"><meta data-rh="true" property="og:url" content="https://www.caesarverifier.org/"><meta data-rh="true" property="og:locale" content="en"><meta data-rh="true" name="docusaurus_locale" content="en"><meta data-rh="true" name="docusaurus_tag" content="default"><meta data-rh="true" name="docsearch:language" content="en"><meta data-rh="true" name="docsearch:docusaurus_tag" content="default"><meta data-rh="true" property="og:image:width" content="1200"><meta data-rh="true" property="og:image:height" content="630"><meta data-rh="true" property="og:image:type" content="image/png"><meta data-rh="true" property="og:image:alt" content="Caesar, verification infrastructure for probabilistic programs, beside a coin-flip loop and the verified bound ð¼[iterations] ⤠2."><meta data-rh="true" name="twitter:image:alt" content="Caesar, verification infrastructure for probabilistic programs, beside a coin-flip loop and the verified bound ð¼[iterations] ⤠2."><meta data-rh="true" name="description" content="Caesar is a verification infrastructure for probabilistic programs, combining HeyVL, reusable proof rules, and SMT-based verification to prove quantitative bounds."><meta data-rh="true" property="og:description" content="Caesar is a verification infrastructure for probabilistic programs, combining HeyVL, reusable proof rules, and SMT-based verification to prove quantitative bounds."><meta data-rh="true" property="og:title" content="Caesar â Verification infrastructure for probabilistic programs"><link data-rh="true" rel="preload" href="/assets/fonts/IBMPlexSans-SemiBold-afac882843fb31756bc6e9886b5c5285.woff2" as="font" type="font/woff2" crossorigin="anonymous"><link data-rh="true" rel="preload" href="/assets/fonts/SourceCodePro-Regular.otf-a7968a8070a7b4cfb4050a96e1eea6eb.woff2" as="font" type="font/woff2" crossorigin="anonymous"><link data-rh="true" rel="preload" href="/assets/fonts/SourceCodePro-Medium.otf-5af999e57f11474e09e2ab8ff3f32089.woff2" as="font" type="font/woff2" crossorigin="anonymous"><link data-rh="true" rel="icon" href="/favicon.ico"><link data-rh="true" rel="canonical" href="https://www.caesarverifier.org/"><link data-rh="true" rel="alternate" href="https://www.caesarverifier.org/" hreflang="en"><link data-rh="true" rel="alternate" href="https://www.caesarverifier.org/" hreflang="x-default"><link data-rh="true" rel="preconnect" href="https://Q93W1TPDIE-dsn.algolia.net" crossorigin="anonymous">
6<script data-rh="true">function insertBanner(){var n=document.createElement("div");n.id="__docusaurus-base-url-issue-banner-container";n.innerHTML='\n<div id="__docusaurus-base-url-issue-banner" style="border: thick solid red; background-color: rgb(255, 230, 179); margin: 20px; padding: 20px; font-size: 20px;">\n <p style="font-weight: bold; font-size: 30px;">Your Docusaurus site did not load properly.</p>\n <p>A very common reason is a wrong site <a href="https://docusaurus.io/docs/docusaurus.config.js/#baseUrl" style="font-weight: bold;">baseUrl configuration</a>.</p>\n <p>Current configured baseUrl = <span style="font-weight: bold; color: red;">/</span> (default value)</p>\n <p>We suggest trying baseUrl = <span id="__docusaurus-base-url-issue-banner-suggestion-container" style="font-weight: bold; color: green;"></span></p>\n</div>\n',document.body.prepend(n);var e=document.getElementById("__docusaurus-base-url-issue-banner-suggestion-container"),s=window.location.pathname,o="/"===s.substr(-1)?s:s+"/";e.textContent=o}document.addEventListener("DOMContentLoaded",function(){void 0===window.docusaurus&&insertBanner()})</script>
6<link rel="alternate" type="application/rss+xml" href="/blog/rss.xml" title="Caesar Verifier RSS Feed"> 7<link rel="alternate" type="application/atom+xml" href="/blog/atom.xml" title="Caesar Verifier Atom Feed"> 8 9<link rel="preconnect" href="https://www.google-analytics.com"> 10<link rel="preconnect" href="https://www.googletagmanager.com">
vendor: 64 bytes, lines 10-11
10 11<script async src="https://www.googletagmanager.com/gtag/js?id=
11G-73RDXJSM5X
vendor: 12 bytes, line 11
11"></script>
12<script>function gtag(){dataLayer.push(arguments)}window.dataLayer=window.dataLayer||[],gtag("js",new Date),gtag("config","G-73RDXJSM5X",{anonymize_ip:!0})</script>
12 13 14 15 16<link rel="search" type="application/opensearchdescription+xml" title="Caesar Verifier" href="/opensearch.xml"> 17 18 19<link rel="icon" type="image/png" sizes="48x48" href="/favicon-48x48.png"> 20<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png"> 21<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png"> 22<link rel="icon" type="image/svg+xml" href="/img/laurel-square.svg"> 23<link rel="apple-touch-icon" sizes="180x180" href="/apple-touch-icon.png"> 24<meta name="theme-color" content="#146c59"><link rel="stylesheet" href="/assets/css/styles.906a2489.css">
25<script src="/assets/js/runtime~main.248b0056.js" defer="defer"></script>
vendor: 1 bytes, line 25
25
26<script src="/assets/js/main.d92e227f.js" defer="defer"></script>
26 27</head> 28<body> 29<svg style="display: none;"><defs> 30<symbol id="theme-svg-external-link" viewBox="0 0 24 24"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"/></symbol> 31</defs></svg>
32<script>!function(){var t=function(){try{return new URLSearchParams(window.location.search).get("docusaurus-theme")}catch(t){}}()||function(){try{return window.localStorage.getItem("theme")}catch(t){}}();document.documentElement.setAttribute("data-theme",t||"light"),document.documentElement.setAttribute("data-theme-choice",t||"light")}(),function(){try{const c=new URLSearchParams(window.location.search).entries();for(var[t,e]of c)if(t.startsWith("docusaurus-data-")){var a=t.replace("docusaurus-data-","data-");document.documentElement.setAttribute(a,e)}}catch(t){}}()</script>
32<div id="__docusaurus"><link rel="preload" as="image" href="/img/laurel.svg"><link rel="preload" as="image" href="/img/institutions/rwth-aachen.svg"><link rel="preload" as="image" href="/img/institutions/saarland.svg"><link rel="preload" as="image" href="/img/institutions/dtu.svg"><link rel="preload" as="image" href="/img/institutions/ucl.svg"><link rel="preload" as="image" href="/img/institutions/oldenburg.svg"><div role="region" aria-label="Skip to main content"><a class="skipToContent_fXgn" href="#__docusaurus_skipToContent_fallback">Skip to main content</a></div><nav aria-label="Main" class="theme-layout-navbar navbar navbar--fixed-top"><div class="navbar__inner"><div class="theme-layout-navbar-left navbar__items"><button aria-label="Toggle navigation bar" aria-expanded="false" class="navbar__toggle clean-btn" type="button"><svg width="30" height="30" viewBox="0 0 30 30" aria-hidden="true"><path stroke="currentColor" stroke-linecap="round" stroke-miterlimit="10" stroke-width="2" d="M4 7h22M4 15h22M4 23h22"></path></svg></button><a class="navbar__brand" href="/"><div class="navbar__logo"><img src="/img/laurel.svg" alt="Caesar Logo" class="themedComponent_mlkZ themedComponent--light_NVdE"><img src="/img/laurel.svg" alt="Caesar Logo" class="themedComponent_mlkZ themedComponent--dark_xIcU"></div><b class="navbar__title text--truncate">Caesar</b></a><a class="navbar__item navbar__link" href="/docs/getting-started">Getting Started</a><a class="navbar__item navbar__link" href="/docs/">Docs</a><a class="navbar__item navbar__link" href="/about">About</a><a class="navbar__item navbar__link" href="/blog">News</a></div><div class="theme-layout-navbar-right navbar__items navbar__items--right"><a href="https://github.com/moves-rwth/caesar" target="_blank" rel="noopener noreferrer" class="navbar__item navbar__link">GitHub<svg width="13.5" height="13.5" aria-label="(opens in new tab)" class="iconExternalLink_nPIU"><use href="#theme-svg-external-link"></use></svg></a><a class="navbar__item navbar__link" href="/docs/publications">Publications</a><div class="toggle_vylO colorModeToggle_DEke"><button class="clean-btn toggleButton_gllP toggleButtonDisabled_aARS" type="button" disabled="" title="system mode" aria-label="Switch between dark and light mode (currently system mode)"><svg viewBox="0 0 24 24" width="24" height="24" aria-hidden="true" class="toggleIcon_g3eP lightToggleIcon_pyhR"><path fill="currentColor" d="M12,9c1.65,0,3,1.35,3,3s-1.35,3-3,3s-3-1.35-3-3S10.35,9,12,9 M12,7c-2.76,0-5,2.24-5,5s2.24,5,5,5s5-2.24,5-5 S14.76,7,12,7L12,7z M2,13l2,0c0.55,0,1-0.45,1-1s-0.45-1-1-1l-2,0c-0.55,0-1,0.45-1,1S1.45,13,2,13z M20,13l2,0c0.55,0,1-0.45,1-1 s-0.45-1-1-1l-2,0c-0.55,0-1,0.45-1,1S19.45,13,20,13z M11,2v2c0,0.55,0.45,1,1,1s1-0.45,1-1V2c0-0.55-0.45-1-1-1S11,1.45,11,2z M11,20v2c0,0.55,0.45,1,1,1s1-0.45,1-1v-2c0-0.55-0.45-1-1-1C11.45,19,11,19.45,11,20z M5.99,4.58c-0.39-0.39-1.03-0.39-1.41,0 c-0.39,0.39-0.39,1.03,0,1.41l1.06,1.06c0.39,0.39,1.03,0.39,1.41,0s0.39-1.03,0-1.41L5.99,4.58z M18.36,16.95 c-0.39-0.39-1.03-0.39-1.41,0c-0.39,0.39-0.39,1.03,0,1.41l1.06,1.06c0.39,0.39,1.03,0.39,1.41,0c0.39-0.39,0.39-1.03,0-1.41 L18.36,16.95z M19.42,5.99c0.39-0.39,0.39-1.03,0-1.41c-0.39-0.39-1.03-0.39-1.41,0l-1.06,1.06c-0.39,0.39-0.39,1.03,0,1.41 s1.03,0.39,1.41,0L19.42,5.99z M7.05,18.36c0.39-0.39,0.39-1.03,0-1.41c-0.39-0.39-1.03-0.39-1.41,0l-1.06,1.06 c-0.39,0.39-0.39,1.03,0,1.41s1.03,0.39,1.41,0L7.05,18.36z"></path></svg><svg viewBox="0 0 24 24" width="24" height="24" aria-hidden="true" class="toggleIcon_g3eP darkToggleIcon_wfgR"><path fill="currentColor" d="M9.37,5.51C9.19,6.15,9.1,6.82,9.1,7.5c0,4.08,3.32,7.4,7.4,7.4c0.68,0,1.35-0.09,1.99-0.27C17.45,17.19,14.93,19,12,19 c-3.86,0-7-3.14-7-7C5,9.07,6.81,6.55,9.37,5.51z M12,3c-4.97,0-9,4.03-9,9s4.03,9,9,9s9-4.03,9-9c0-0.46-0.04-0.92-0.1-1.36 c-0.98,1.37-2.58,2.26-4.4,2.26c-2.98,0-5.4-2.42-5.4-5.4c0-1.81,0.89-3.42,2.26-4.4C12.92,3.04,12.46,3,12,3L12,3z"></path></svg><svg viewBox="0 0 24 24" width="24" height="24" aria-hidden="true" class="toggleIcon_g3eP systemToggleIcon_QzmC"><path fill="currentColor" d="m12 21c4.971 0 9-4.029 9-9s-4.029-9-9-9-9 4.029-9 9 4.029 9 9 9zm4.95-13.95c1.313
321.313 2.05 3.093 2.05 4.95s-0.738 3.637-2.05 4.95c-1.313 1.313-3.093 2.05-4.95 2.05v-14c1.857 0 3.637 0.737 4.95 2.05z"></path></svg></button></div><div class="navbarSearchContainer_Bca1"><button type="button" class="DocSearch DocSearch-Button" aria-label="Search (Meta+k)" aria-keyshortcuts="Meta+k"><span class="DocSearch-Button-Container"><svg width="20" height="20" class="DocSearch-Search-Icon" viewBox="0 0 24 24" aria-hidden="true"><circle cx="11" cy="11" r="8" stroke="currentColor" fill="none" stroke-width="1.4"></circle><path d="m21 21-4.3-4.3" stroke="currentColor" fill="none" stroke-linecap="round" stroke-linejoin="round"></path></svg><span class="DocSearch-Button-Placeholder">Search</span></span><span class="DocSearch-Button-Keys"></span></button></div></div></div><div role="presentation" class="navbar-sidebar__backdrop"></div></nav><div id="__docusaurus_skipToContent_fallback" class="theme-layout-main main-wrapper mainWrapper_z2l0"><div class="homepage_Tf7U code_oZrQ"><header class="hero_aEcG"><div class="container heroGrid_ibpR"><div><div class="brand_x3Gm"><img src="/img/laurel.svg" alt="" width="36" height="56"><span>Caesar</span></div><h1>A Verifier for Probabilistic Programs</h1><div class="introduction_mtGB"><p>Caesar proves bounds on probabilities, expected runtimes, and resource usage.</p><p>Write a model in Caesarâs programming language, <a href="/docs/heyvl">HeyVL</a>, and add proof annotations. Caesar verifies the stated bounds symbolically.</p></div><ul class="capabilities_WtdB" aria-label="Caesar capabilities"><li><a href="/docs/stdlib/numbers">Infinite state spaces</a></li><li><a href="/docs/proof-rules">Unbounded loops</a></li><li><a href="/docs/heyvl/procs#calling-procedures">Recursion</a></li><li><a href="/docs/heyvl/statements#nondeterministic-choices">Nondeterminism</a></li><li><a href="/docs/proof-rules/approximations">Sound proofs and refutations</a></li></ul><div class="actions_OvQX"><a class="button button--primary" href="/docs/getting-started/installation">Install Caesar</a><a href="#example" class="button button--outline button--primary">See an example</a></div><a href="https://github.com/moves-rwth/caesar/releases/tag/v4.1.0" target="_blank" rel="noopener noreferrer" class="release_soEU"><span class="releaseDot_F9tw" aria-hidden="true"></span>Latest release: Caesar v4.1.0<span aria-hidden="true"> â</span></a></div><aside class="program_Cl2q" aria-labelledby="program-title"><h2 id="program-title">A Probabilistic Program</h2><p>Each iteration ends the loop with probability ½.</p><div class="language-heyvl codeBlockContainer_Ckt0 theme-code-block" style="--prism-color:#403f53;--prism-background-color:#FBFBFB"><div class="codeBlockContent_QJqH"><pre tabindex="0" class="prism-code language-heyvl codeBlock_bY9V thin-scrollbar" style="color:#403f53;background-color:#FBFBFB"><code class="codeBlockLines_e6Vv"><div class="token-line" style="color:#403f53"><span class="token plain">done </span><span class="token operator" style="color:rgb(12, 150, 155)">=</span><span class="token plain"> </span><span class="token boolean" style="color:rgb(188, 84, 84)">false</span><span class="token plain"></span><br></div><div class="token-line" style="color:#403f53"><span class="token plain"></span><span class="token keyword" style="color:rgb(12, 150, 155)">while</span><span class="token plain"> </span><span class="token operator" style="color:rgb(12, 150, 155)">!</span><span class="token plain">done </span><span class="token punctuation" style="color:rgb(153, 76, 195)">{</span><span class="token plain"></span><br></div><div class="token-line" style="color:#403f53"><span class="token plain"> done </span><span class="token operator" style="color:rgb(12, 150, 155)">=</span><span class="token plain"> </span><span class="token builtin" style="color:rgb(72, 118, 214)">flip</span><span class="token punctuation" style="color:rgb(153, 76, 195)">(</span><span class="token number" style="color:rgb(170, 9, 130)">0.5</span><span class="token punctuation" style="color:rgb(153, 76, 195)">)</span><span class="token plain"></span><br></div><div class="token-line" style="color:#403f53"><span class="token plain"></span><span class="token punctuation" style="color:rgb(153, 76, 195)">}</span><br></div></code></pre></div></div><div class="proofStep_cAwm"><span aria-hidden="true">â</span><span>Caesar checks the supplied loop invariant.</span></div><div class="guarantee_megB"><span class="check_oIx5" aria-hidden="true">â</span><div><strong class="guaranteeFormula_y5QM" aria-hidden="true">ð¼[iterations] ⤠2</strong><p class="guaranteeDescription_jJWe">The expected number of iterations is at most 2.</p><a href="#example">See the specification and proof â</a></div></div></aside></div></header><main>
32<section class="institutions_z436" aria-label="Universities contributing to Caesar"><div class="container institutionsInner_znab"><p>An open-source project from</p><ul class="institutionLogos_k5OJ"><li><a href="https://moves.rwth-aachen.de/" target="_blank" rel="noopener noreferrer"><img src="/img/institutions/rwth-aachen.svg" alt="RWTH Aachen University (MOVES)" width="168" height="56"></a></li><li><a href="https://quave.cs.uni-saarland.de/" target="_blank" rel="noopener noreferrer"><img src="/img/institutions/saarland.svg" alt="Saarland University (QUAVE)" width="168" height="56"></a></li><li><a href="https://www.compute.dtu.dk/english/research/research-sections/software-systems-engineering" target="_blank" rel="noopener noreferrer"><img src="/img/institutions/dtu.svg" alt="Technical University of Denmark (SSE)" width="168" height="56"></a></li><li><a href="http://pplv.cs.ucl.ac.uk/welcome/" target="_blank" rel="noopener noreferrer"><img src="/img/institutions/ucl.svg" alt="University College London (PPLV)" width="168" height="56"></a></li><li><a href="https://uol.de/en/computingscience/groups/theorie-korrekter-systeme" target="_blank" rel="noopener noreferrer"><img src="/img/institutions/oldenburg.svg" alt="University of Oldenburg (Theory of Correct Systems)" width="168" height="56"></a></li></ul></div></section><section class="motivation_QdkR" aria-labelledby="programs-title"><div class="container sectionHeading_pyX_"><h2 id="programs-title">Probabilistic Programs</h2><p>Probabilistic programs make random choices that affect their results and control flow. They model randomized algorithms and protocols, such as communication over an unreliable channel. Verification can establish bounds on the probability of transmission failure, the expected number of retries, or the resources consumed.</p></div></section>
32<section class="section_f0cM" aria-labelledby="infrastructure-title"><div class="container"><div class="sectionHeading_pyX_"><h2 id="infrastructure-title">Verification Infrastructure</h2><div><p>Caesarâs intermediate verification language, HeyVL, expresses probabilistic programs together with quantitative specifications and proof rules. New proof rules can be encoded in HeyVL without changing the verifier.</p><a href="https://link.springer.com/content/pdf/10.1007/978-3-032-32537-2_27.pdf?pdf=inline%20link" target="_blank" rel="noopener noreferrer" class="button button--outline button--primary paperOverview_hgb6">Read the CAV 2026 tool paper â</a></div></div><figure class="architecture_krHE"><div class="architectureBody_XqyA"><div class="inputs_Hrek"><div class="inputGroup_x9xb"><h3>Programs</h3><ul><li><a href="/docs/stdlib/distributions">Sampling from discrete distributions</a></li><li><a href="/docs/proof-rules">Unbounded <code>while</code> loops</a></li><li><a href="/docs/heyvl/procs#calling-procedures">Procedure calls and recursion</a></li><li><a href="/docs/heyvl/statements#nondeterministic-choices"><em>Angelic</em> and <em>demonic</em> nondeterminism</a></li><li><a href="/docs/stdlib">Booleans, integers, reals, and lists</a></li></ul></div><div class="inputGroup_x9xb"><h3>Specifications</h3><ul><li><a href="/docs/heyvl/procs">Lower and upper bounds on expected values</a></li><li><a href="/docs/heyvl/procs">Probability bounds</a></li><li><a href="/docs/heyvl/statements#reward-and-weigh">Expected runtime and resource consumption</a></li><li><a href="/docs/proof-rules/ast">Almost-sure termination</a></li><li><a href="/blog/2026/03/04/highly-incremental#example-with-caesar-second-moment-of-runtime">Higher moments</a></li><li><a href="/blog/2026/03/04/highly-incremental#programmatic-reward-transformations">Tail probabilities</a></li></ul></div><div class="inputGroup_x9xb"><h3>Proof Rules</h3><ul><li><a href="/docs/proof-rules/induction">Induction and <i>k</i>-induction</a></li><li><a href="/docs/proof-rules/unrolling">Loop unrolling</a> and <a href="/docs/proof-rules/omega-invariants">Ï-invariants</a></li><li><a href="/docs/proof-rules/ost">Optional stopping</a></li><li><a href="/docs/proof-rules/ast">Almost-sure termination</a></li><li><a href="/docs/proof-rules/past">Positive almost-sure termination</a></li></ul></div></div><div class="merge_omcg" aria-hidden="true"><span></span><span></span><span></span></div><div class="heyvl_d1zR"><div><a href="/docs/heyvl">HeyVL</a><span>Quantitative intermediate verification language</span></div><p><em>Quantitative verification statements</em>, such as <code>assert</code> and <code>assume</code>, encode proof rules as programs. HeyVL supports user-defined <a href="/docs/heyvl/domains#definitional-functions">functions</a> and <a href="/docs/heyvl/domains#defining-types-with-domains">types</a>.</p></div><div class="fork_toSE" aria-hidden="true"></div><div class="backends_xIRD"><div class="logicBackend_o8HW"><h3><a href="/docs/heyvl/expressions">HeyLo</a></h3><span class="backendLabel_d4c1">Deductive verification</span><p class="backendScope_CK9a">Infinite state spaces and symbolic inputs</p><p class="backendDescription_kMMB">Proof annotations let Caesar establish bounds without enumerating program states. It generates <em>verification conditions</em> in HeyLo, its <em>real-valued assertion logic</em>. HeyLo formulas map program states to non-negative reals or infinity.</p><p class="backendDescription_kMMB">Caesar simplifies verification conditions and eliminates quantitative quantifiers where possible before sending them to <a href="https://github.com/Z3Prover/z3" target="_blank" rel="noopener noreferrer">Z3</a>.<!-- --> <!-- -->It can also reason about <a href="/docs/caesar/debugging#function-encodings-and-limited-functions">recursive functions</a>.</p><div class="backendRoute_cZro">Verification conditions <span aria-hidden="true">â</span> <a href="https://github.com/Z3Prover/z3" target="_blank" rel="noopener noreferrer">Z3</a></div></div><div><h3><a href="https://jani-spec.org/" target="_blank" rel="noopener noreferrer">JANI</a> / <a href="https://www.stormchecker.org/" target="_blank" rel="noopener noreferrer">Storm</a></h3><a class="backendLabel_d4c1" href="/docs/model-checking">An alternative model-checking backend</a><p class="backendScope_CK9a">Automatic analysis of finite-state models</p><p class="backendDescription_kMMB">
32For programs with finitely many states, <a href="https://www.stormchecker.org/" target="_blank" rel="noopener noreferrer">Storm</a> can calculate expected values without user-provided invariants. Caesar exports a <a href="/docs/model-checking#supported-programs">subset of HeyVL</a> to <a href="https://jani-spec.org/" target="_blank" rel="noopener noreferrer">JANI</a>, a format for probabilistic models that Storm can read.</p><p class="backendDescription_kMMB">Infinite-state models can also be <a href="/docs/model-checking#parametric-and-infinite-state-models">approximated by exploring a limited number of states</a>.</p><div class="backendRoute_cZro">Executable subset <span aria-hidden="true">â</span> <a href="https://jani-spec.org/" target="_blank" rel="noopener noreferrer">JANI</a> <span aria-hidden="true">â</span> <a href="https://www.stormchecker.org/" target="_blank" rel="noopener noreferrer">Storm</a></div></div></div></div></figure><div class="sectionLinks_cF5X"><a href="/docs/heyvl">HeyVL reference â</a><a href="/docs/proof-rules">Proof-rule reference â</a></div></div></section><section class="example_wtsb" aria-labelledby="example"><div class="container"><div class="heading_RT6Z"><h2 class="anchor anchorTargetStickyNavbar_Vzrq" id="example">Example: Expected Runtime of the Geometric Loop<a href="#example" class="hash-link" aria-label="Direct link to Example: Expected Runtime of the Geometric Loop" title="Direct link to Example: Expected Runtime of the Geometric Loop" translate="no">â</a></h2><p>The number of iterations follows a geometric distribution: each iteration terminates the loop with probability ½, but the loop can run for arbitrarily many iterations. There are infinitely many possible execution paths. Caesar checks a supplied loop invariant to bound the expected number of iterations without enumerating these paths.</p></div><div class="controls_pEpp" role="group" aria-label="Highlight example lines"><button type="button" aria-pressed="true" aria-controls="geometric-code"><span aria-hidden="true">1</span>Program</button><button type="button" aria-pressed="false" aria-controls="geometric-code"><span aria-hidden="true">2</span>Specification</button><button type="button" aria-pressed="false" aria-controls="geometric-code"><span aria-hidden="true">3</span>Invariant</button><button type="button" aria-pressed="false" aria-controls="geometric-code"><span aria-hidden="true">4</span>Verification</button></div><div class="layout_GeoR"><div class="codeColumn_RB8V"><div id="geometric-code" class="code_SFq6" role="region" aria-label="Geometric loop in HeyVL"><div class="language-heyvl codeBlockContainer_Ckt0 theme-code-block" style="--prism-color:#403f53;--prism-background-color:#FBFBFB"><div class="codeBlockTitle_OeMC">geometric-runtime.heyvl</div><div class="codeBlockContent_QJqH"><pre tabindex="0" class="prism-code language-heyvl codeBlock_bY9V thin-scrollbar" style="color:#403f53;background-color:#FBFBFB"><code class="codeBlockLines_e6Vv codeBlockLinesWithNumbering_o6Pm" style="counter-reset:line-count 0"><div class="token-line codeLine_lJS_" style="color:#403f53"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token annotation keyword" style="color:rgb(12, 150, 155)">@ert</span><span class="token plain"></span></span><br></div><div class="token-line codeLine_lJS_" style="color:#403f53"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"></span><span class="token keyword" style="color:rgb(12, 150, 155)">coproc</span><span class="token plain"> geo_expected_runtime</span><span class="token punctuation" style="color:rgb(153, 76, 195)">(</span><span class="token punctuation" style="color:rgb(153, 76, 195)">)</span><span class="token plain"> </span><span class="token keyword" style="color:rgb(12, 150, 155)">-></span><span class="token plain"> </span><span class="token punctuation" style="color:rgb(153, 76, 195)">(</span><span class="token plain">done</span><span class="token punctuation" style="color:rgb(153, 76, 195)">:</span><span class="token plain"> </span><span class="token builtin" style="color:rgb(72, 118, 214)">
32Bool</span><span class="token punctuation" style="color:rgb(153, 76, 195)">)</span><span class="token plain"></span></span><br></div><div class="token-line codeLine_lJS_" style="color:#403f53"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:rgb(12, 150, 155)">pre</span><span class="token plain"> </span><span class="token number" style="color:rgb(170, 9, 130)">2</span><span class="token plain"></span></span><br></div><div class="token-line codeLine_lJS_" style="color:#403f53"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:rgb(12, 150, 155)">post</span><span class="token plain"> </span><span class="token number" style="color:rgb(170, 9, 130)">0</span><span class="token plain"></span></span><br></div><div class="token-line codeLine_lJS_" style="color:#403f53"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"></span><span class="token punctuation" style="color:rgb(153, 76, 195)">{</span><span class="token plain"></span></span><br></div><div class="token-line theme-code-block-highlighted-line codeLine_lJS_" style="color:#403f53"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> done </span><span class="token operator" style="color:rgb(12, 150, 155)">=</span><span class="token plain"> </span><span class="token boolean" style="color:rgb(188, 84, 84)">false</span><span class="token plain"></span></span><br></div><div class="token-line codeLine_lJS_" style="color:#403f53"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token annotation keyword" style="color:rgb(12, 150, 155)">@invariant</span><span class="token punctuation" style="color:rgb(153, 76, 195)">(</span><span class="token operator" style="color:rgb(12, 150, 155)">[</span><span class="token operator" style="color:rgb(12, 150, 155)">!</span><span class="token plain">done</span><span class="token operator" style="color:rgb(12, 150, 155)">]</span><span class="token plain"> </span><span class="token operator" style="color:rgb(12, 150, 155)">*</span><span class="token plain"> </span><span class="token number" style="color:rgb(170, 9, 130)">2</span><span class="token punctuation" style="color:rgb(153, 76, 195)">)</span><span class="token plain"></span></span><br></div><div class="token-line theme-code-block-highlighted-line codeLine_lJS_" style="color:#403f53"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:rgb(12, 150, 155)">while</span><span class="token plain"> </span><span class="token operator" style="color:rgb(12, 150, 155)">!</span><span class="token plain">done </span><span class="token punctuation" style="color:rgb(153, 76, 195)">{</span><span class="token plain"></span></span><br></div><div class="token-line theme-code-block-highlighted-line codeLine_lJS_" style="color:#403f53"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:rgb(12, 150, 155)">reward</span><span class="token plain"> </span><span class="token number" style="color:rgb(170, 9, 130)">1</span><span class="token plain"></span></span><br></div><div class="token-line theme-code-block-highlighted-line codeLine_lJS_" style="color:#403f53"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> done </span><span class="token operator" style="color:rgb(12, 150, 155)">=</span><span class="token plain"> </span><span class="token builtin" style="color:rgb(72, 118, 214)">flip</span><span class="token punctuation" style="color:rgb(153, 76, 195)">(</span><span class="token number" style="color:rgb(170, 9, 130)">0.5</span><span class="token punctuation" style="color:rgb(153, 76, 195)">)</span><span class="token plain"></span></span><br></div><div class="token-line theme-code-block-highlighted-line codeLine_lJS_" style="color:#403f53"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token punctuation" style="color:rgb(153, 76, 195)">}</span><span class="token plain"></span></span><br></div><div class="token-line codeLine_lJS_" style="color:#403f53"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"></span><span class="token punctuation" style="color:rgb(153, 76, 195)">}</span></span><br></div></code></pre></div></div></div><div class="result_ikai"><span class="check_MXUY" aria-hidden="true">â</span><div><strong>Verified example</strong><br>The expected number of iterations is at most 2.</div></div><div class="links_y4vy"><a href="/docs/getting-started/first-proof">Example walkthrough â</a><a href="/examples/geometric-runtime.heyvl" download="">Download HeyVL file â</a></div></div><div><div class="explanation_R7xr selected_I9Yd"><h3><button class="explanationButton_iptV" type="button" aria-pressed="true" aria-controls="geometric-code"><span class="number_r7jb" aria-hidden="true">1</span>Program</button></h3><p>Each iteration samples a fair coin with <code>flip(0.5)</code> and records one unit of cost with <code>reward 1</code>. The loop ends when <code>done</code> becomes true.</p></div><div class="explanation_R7xr"><h3><button class="explanationButton_iptV" type="button" aria-pressed="false" aria-controls="geometric-code"><span class="number_r7jb" aria-hidden="true">2</span>Specification</button></h3><p>A <code>coproc</code> checks an upper bound. Here, <code>pre 2</code> bounds the expected total cost by 2, and <code>post 0</code> adds no cost after the loop. The <code>@ert</code> annotation selects expected-runtime reasoning.</p></div><div class="explanation_R7xr"><h3><button class="explanationButton_iptV" type="button" aria-pressed="false" aria-controls="geometric-code"><span class="number_r7jb" aria-hidden="true">3</span>Invariant</button></h3><p>The user supplies <code>[!done] * 2</code> as a bound on the remaining expected cost: 2 before success and 0 afterward. One iteration preserves this bound:</p><p class="equation_OSa8">1 + ½ · 0 + ½ · 2 = 2</p></div><div class="explanation_R7xr"><h3><button class="explanationButton_iptV" type="button" aria-pressed="false" aria-controls="geometric-code"><span class="number_r7jb" aria-hidden="true">4</span>Verification</button></h3><p>Caesar checks that the supplied invariant establishes the specification. The expected number of iterations is at most 2. Individual executions can take more than two iterations.</p></div></div></div></div></section><section class="motivation_QdkR" aria-labelledby="motivation-title"><div class="container sectionHeading_pyX_"><h2 id="motivation-title">Reasoning About Unbounded Executions</h2><div><p>The loop above has no finite worst-case iteration bound, although its expected number of iterations is at most 2. Proving this requires reasoning about the whole distribution of execution lengths, including arbitrarily long runs.</p><p>Termination itself has several meanings. A program can terminate with probability 1 and still have infinite expected runtime, as in a <a href="https://arxiv.org/pdf/1711.03588#page=2" target="_blank" rel="noopener noreferrer">symmetric random walk that stops at zero</a>. Thus, <a href="/docs/proof-rules/ast"><em>almost-sure termination</em></a> and <a href="/docs/proof-rules/past">finite expected runtime</a> require different proof arguments.</p><p>Caesar checks these arguments using invariants, martingale-based rules, and symbolic verification. Bounds can depend on program inputs, so a single proof can cover all input values satisfying its assumptions.</p></div></div></section><section class="section_f0cM" aria-labelledby="tools-title"><div class="container tools_AuFc"><div><h2 id="tools-title">Verify in VS Code</h2><p>The Caesar extension verifies HeyVL programs directly in the editor. It also installs and updates Caesar for you.</p><ul class="editorFeatures_YtLD"><li><h3>Verification on Save</h3><p>See verification results beside the code, with errors and warnings at the relevant statements.</p></li><li><h3><a href="/blog/2024/05/20/caesar-2-0#caesar20-vscode-extension">Inline Explanations</a></h3><p>Inspect the computed verification conditions to understand how Caesar reasons about your program.</p></li><li><h3><a href="/docs/caesar/slicing">Slicing Diagnostics</a></h3><p>Locate failing proof obligations and identify which statements are needed for verification.</p></li><li><h3>HeyVL Editing Support</h3><p>Use syntax highlighting, code snippets, and reference hovers for language constructs and proof annotations.</p></li></ul><div class="toolLinks_b1Yo"><a href="https://marketplace.visualstudio.com/items?itemName=rwth-moves.caesar" target="_blank" rel="noopener noreferrer" class="button button--primary">Install the VS Code extension â</a><a href="https://open-vsx.org/extension/rwth-moves/caesar" target="_blank" rel="noopener noreferrer">Open VSX for VSCodium â</a><a href="/docs/caesar/vscode-and-lsp">Extension documentation â</a></div></div><figure class="editor_u5te"><a href="/img/slicing-demo.png" aria-label="View the VS Code diagnostic screenshot at full size"><img src="/img/slicing-demo.png" alt="Caesar in VS Code, showing the diagnostic âinvariant might not be inductiveâ at a loop annotation." width="994" height="818" loading="lazy"></a><figcaption>Caesar points to a loop invariant that may not be inductive.</figcaption></figure></div></section><section class="section_f0cM" aria-labelledby="news-title"><div class="container news_pJOq"><div><h2 id="news-title">News</h2><a href="/blog">All posts â</a></div><article><time class="venue_RGNh" datetime="2026-09-30T00:00:00.000Z">30 September 2026</time><h3><a href="/blog/2026/09/30/caesar-4-1">
32Caesar 4.1: Soundness Fixes and Unbounded WLP</a></h3><p>Caesar 4.1 fixes soundness bugs in @ast, @past, and @omega_invariant that could let invalid proofs pass verification.</p></article></div></section><section class="section_f0cM research__Tbr" aria-labelledby="research-title"><div class="container"><div class="sectionHeading_pyX_"><h2 id="research-title">Research and Publications</h2><p>Peer-reviewed work on Caesar, its foundations, and applications.</p></div><ul class="publications_dSyn" aria-label="Peer-reviewed publications"><li class="publication_P3xc"><span class="venue_RGNh">ITP 2026</span><div><h3><a href="/blog/2026/07/22/itp26-securing-foundations">Securing the Foundations of an Intermediate Language for Probabilistic Program Verification</a></h3><p>Mechanized foundations in Lean for the correctness of HeyVL encodings and probabilistic verification techniques.</p></div></li><li class="publication_P3xc"><span class="venue_RGNh">CAV 2026</span><div><h3><a href="/blog/2026/04/20/caesar-tool-paper-cav">Caesar: A Deductive Verifier for Probabilistic Programs</a></h3><p>The Caesar tool paper, covering its verification workflow, editor support, and backends.</p></div></li><li class="publication_P3xc"><span class="venue_RGNh">FM 2026</span><div><h3><a href="/blog/2026/03/04/highly-incremental">Highly Incremental: A Simple Programmatic Approach for Many Objectives</a></h3><p>Reward transformations for verifying higher moments, tail probabilities, and other quantitative objectives.</p></div></li><li class="publication_P3xc"><span class="venue_RGNh">POPL 2026</span><div><h3><a href="/blog/2026/01/15/popl26-ast-distributed">Verifying Almost-Sure Termination for Randomized Distributed Algorithms</a></h3><p>Proof rules for almost-sure termination under weak fairness, used to verify randomized consensus protocols.</p></div></li><li class="publication_P3xc"><span class="venue_RGNh">ESOP 2026</span><div><h3><a href="/blog/2025/12/23/esop26-slicing">Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing</a></h3><p>The foundations of Caesarâs slicing diagnostics for locating errors and simplifying proofs.</p></div></li><li class="publication_P3xc"><span class="venue_RGNh">OOPSLA 2025</span><div><h3><a href="/blog/2025/04/11/foundations-continuous">Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back</a></h3><p>HeyVL encodings of Riemann-sum approximations to verify expectation bounds for continuous distributions.</p></div></li><li class="publication_P3xc"><span class="venue_RGNh">AISoLA 2024</span><div><h3><a href="/blog/2024/12/31/game-based-semantics">A Game-Based Semantics for the Probabilistic Intermediate Verification Language HeyVL</a></h3><p>An operational semantics for HeyVL based on refereed stochastic games.</p></div></li><li class="publication_P3xc"><span class="venue_RGNh">OOPSLA 2023</span><div><h3><a href="/blog/2023/09/28/oopsla23">A Deductive Verification Infrastructure for Probabilistic Programs</a></h3><p>The foundations of Caesar: HeyLo, HeyVL, and encodings of probabilistic proof rules.</p></div></li></ul><a href="/docs/publications">Full references and theses â</a></div></section><nav class="projectLinks_Oszc" aria-label="Caesar project links"><div class="container sectionLinks_cF5X"><a href="https://github.com/moves-rwth/caesar" target="_blank" rel="noopener noreferrer">Source code â</a><a href="/about">About Caesar â</a></div></nav></main></div></div><footer class="theme-layout-footer footer footer--dark"><div class="container container-fluid"><div class="row footer__links"><div class="theme-layout-footer-column col footer__col"><div class="footer__title">Documentation</div><ul class="footer__items clean-list"><li class="footer__item"><a class="footer__link-item" href="/docs/getting-started">Getting Started</a></li><li class="footer__item"><a class="footer__link-item" href="/docs/heyvl">HeyVL</a></li><li class="footer__item"><a class="footer__link-item" href="/docs/stdlib">Standard Library</a></li><li class="footer__item"><a class="footer__link-item" href="/docs/proof-rules">Proof Rules</a></li></ul></div>
32<div class="theme-layout-footer-column col footer__col"><div class="footer__title">Community</div><ul class="footer__items clean-list"><li class="footer__item"><a href="https://github.com/moves-rwth/caesar/discussions" target="_blank" rel="noopener noreferrer" class="footer__link-item">Caesar Discussions<svg width="13.5" height="13.5" aria-label="(opens in new tab)" class="iconExternalLink_nPIU"><use href="#theme-svg-external-link"></use></svg></a></li><li class="footer__item"><a class="footer__link-item" href="/docs/publications">Academic Publications</a></li></ul></div><div class="theme-layout-footer-column col footer__col"><div class="footer__title">More</div><ul class="footer__items clean-list"><li class="footer__item"><a class="footer__link-item" href="/about">About</a></li><li class="footer__item"><a class="footer__link-item" href="/blog">News</a></li><li class="footer__item"><a href="https://github.com/moves-rwth/caesar" target="_blank" rel="noopener noreferrer" class="footer__link-item">GitHub<svg width="13.5" height="13.5" aria-label="(opens in new tab)" class="iconExternalLink_nPIU"><use href="#theme-svg-external-link"></use></svg></a></li></ul></div></div><div class="footer__bottom text--center"><div class="footer__copyright">Copyright © 2026 Caesar Developers. Built with Docusaurus.</div></div></div></footer></div> 33</body> 34</html>
Line numbers count LF bytes from the start of the resource, as the search results do. Vendor segments are library code the classifier recognised; they are stored but not indexed. Bytes are shown as Latin1 characters, one per byte.