Skip to main content
Caesar

A Verifier for Probabilistic Programs

Caesar proves bounds on probabilities, expected runtimes, and resource usage.

Write a model in Caesar’s programming language, HeyVL, and add proof annotations. Caesar verifies the stated bounds symbolically.

Install CaesarSee an example
Latest release: Caesar v4.1.0

An open-source project from

  • RWTH Aachen University (MOVES)
  • Saarland University (QUAVE)
  • Technical University of Denmark (SSE)
  • University College London (PPLV)
  • University of Oldenburg (Theory of Correct Systems)

Probabilistic Programs

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.

Verification Infrastructure

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.

Read the CAV 2026 tool paper ↗

Programs

Specifications

Proof Rules

HeyVLQuantitative intermediate verification language

Quantitative verification statements, such as assert and assume, encode proof rules as programs. HeyVL supports user-defined functions and types.

HeyLo

Deductive verification

Infinite state spaces and symbolic inputs

Proof annotations let Caesar establish bounds without enumerating program states. It generates verification conditions in HeyLo, its real-valued assertion logic. HeyLo formulas map program states to non-negative reals or infinity.

Caesar simplifies verification conditions and eliminates quantitative quantifiers where possible before sending them to Z3. It can also reason about recursive functions.

Verification conditions Z3

JANI / Storm

An alternative model-checking backend

Automatic analysis of finite-state models

For programs with finitely many states, Storm can calculate expected values without user-provided invariants. Caesar exports a subset of HeyVL to JANI, a format for probabilistic models that Storm can read.

Infinite-state models can also be approximated by exploring a limited number of states.

Executable subset JANI Storm
HeyVL reference →Proof-rule reference →

Example: Expected Runtime of the Geometric Loop​

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.

geometric-runtime.heyvl
@ert
coproc geo_expected_runtime() -> (done: Bool)
    pre 2
    post 0
{
    done = false
    @invariant([!done] * 2)
    while !done {
        reward 1
        done = flip(0.5)
    }
}
Verified example
The expected number of iterations is at most 2.
Example walkthrough →Download HeyVL file ↓

Each iteration samples a fair coin with flip(0.5) and records one unit of cost with reward 1. The loop ends when done becomes true.

A coproc checks an upper bound. Here, pre 2 bounds the expected total cost by 2, and post 0 adds no cost after the loop. The @ert annotation selects expected-runtime reasoning.

The user supplies [!done] * 2 as a bound on the remaining expected cost: 2 before success and 0 afterward. One iteration preserves this bound:

1 + ½ · 0 + ½ · 2 = 2

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.

Reasoning About Unbounded Executions

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.

Termination itself has several meanings. A program can terminate with probability 1 and still have infinite expected runtime, as in a symmetric random walk that stops at zero. Thus, almost-sure termination and finite expected runtime require different proof arguments.

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.

Verify in VS Code

The Caesar extension verifies HeyVL programs directly in the editor. It also installs and updates Caesar for you.

  • Verification on Save

    See verification results beside the code, with errors and warnings at the relevant statements.

  • Inline Explanations

    Inspect the computed verification conditions to understand how Caesar reasons about your program.

  • Slicing Diagnostics

    Locate failing proof obligations and identify which statements are needed for verification.

  • HeyVL Editing Support

    Use syntax highlighting, code snippets, and reference hovers for language constructs and proof annotations.

Install the VS Code extension ↗Open VSX for VSCodium ↗Extension documentation →
Caesar in VS Code, showing the diagnostic “invariant might not be inductive” at a loop annotation.
Caesar points to a loop invariant that may not be inductive.

Research and Publications

Peer-reviewed work on Caesar, its foundations, and applications.

Full references and theses →