Caesar 4.0 improves expression parsing, adds explicit soundness guarantees for refutations in CLI/LSP feedback, introduces new weigh and additive choice (if +) statements, and experimental entailment checking.

Overview:

1. Expression Parsing Changes
2. Soundness Checks and Better Diagnostics
3. New HeyVL Statements: weigh and Additive Choice
4. Experimental Entailment Checking
5. Other Improvements

Our new paper "Highly Incremental: A Simple Programmatic Approach for Many Objectives" by Philipp Schröer and Joost-Pieter Katoen presents a one-fits-all approach for quantitative objectives on probabilistic programs, applicable to verification with Caesar.

The paper will be presented at The 27th International Symposium on Formal Methods (FM 2026) in Tokyo, Japan.

A preprint with a detailed appendix of proofs and case studies is available on arXiv: "Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)".

In this post, we:

1. show how reward statements model runtime and related quantities.
2. explain why verification of variance is difficult for runtime objectives.
3. introduce our sound program transformation for these objectives, including higher moments, tail probabilities, CDFs, expected excess, and moment-generating functions.
4. work through a Caesar example for the second moment of runtime.

Programmatic Reward Modeling​

The paper explores what can be encoded into probabilistic programs with reward statements, which collect a certain quantity — rewards — during execution. We then consider expected rewards, i.e. the expected value of rewards collected over the distribution of program executions. This approach enables more applications for Caesar's weakest pre-expectation reasoning out-of-the-box.

The paper "Verifying Almost-Sure Termination for Randomized Distributed Algorithms" was presented at the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL) 2026 held in Rennes, France. The authors are Constantin Enea (LIX, CNRS, Ecole Polytechnique), Rupak Majumdar (MPI-SWS), Harshit Jitendra Motwani (MPI-SWS), V.R. Sathiyanarayana (MPI-SWS).

The paper presents a verification technique for liveness properties of randomized distributed algorithms. It introduces a proof rule for fair almost-sure termination of distributed systems, combining martingale-based arguments for probabilistic termination with reasoning about weak fairness. The proof rules are implemented in Caesar and were used to verify termination of randomized asynchronous consensus protocols, including Ben-Or’s protocol and graded binary consensus, under both crash and Byzantine faults.

Darion Haase presented our work on slicing-based diagnostics for probabilistic program verification at Dafny 2026, which took place on January 11, 2026, in Rennes, France.

The presentation gave an overview of the main ideas behind our ESOP 2026 paper "Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing". It gave an introduction to our three notions of slicing (error-witnessing, verification-witnessing, and verification-preserving slices) and explained how they can be used to provide useful and formally justified diagnostics for deductive verifiers like Caesar and Dafny.

Our paper "Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing" was accepted at the European Symposium on Programming (ESOP) 2026 to be held in Turin, Italy. The authors are Philipp Schröer, Darion Haase, and Joost-Pieter Katoen. An extended version of the paper is already available on arXiv.

The paper presents theoretical foundations and the implementation of our slicing-based user diagnostics in Caesar, which we dub Brutus. On this website, you can also find the user guide-level documentation on slicing in Caesar. See also the announcement of Caesar 2.0, which introduced the first slicing implementation in Caesar.

On August 26, 2025, Christoph Matheja gave the opening keynote talk at QEST + FORMATS 2025 in Aarhus, Denmark titled "Automating Proof Rules for Probabilistic Programs", featuring Caesar and HeyVL.

The slides are available in PDF format.

Caesar 3.0 improves the SMT reasoning capabilities of Caesar, making verification more powerful, stable, and predictable. This release marks the conclusion of a project that started more than 9 months ago, including a successful Master's thesis by Emil-Beothy Elo.

Overview:

1. Limited Functions
2. Other SMT-related Improvements
3. Other Improvements

We had the pleasure to present Caesar at the 14th Summer School for Formal Techniques at Menlo College in Menlo Park, California, organized by the SRI Formal Methods Group. It took place from May 24th to May 30th.

Joost-Pieter Katoen gave two lectures on the theoretical foundations of probabilistic programming and their verification, and together we hosted two accompanying lab sessions where students could try out Caesar and HeyVL.

Here is the lecture abstract:

Probabilistic programs encode randomized algorithms, robot controllers, learning components, security mechanisms, and much more. They are however hard to grasp. Not only by humans, also by computers: checking elementary properties related to e.g., termination are "more undecidable" than for ordinary programs. The analysis of probabilistic programs requires manipulating irrational or even transcendental numbers.

Although this all sounds like a no-go for (semi-)automated analysis, I will present a deductive verification technique to analyse probabilistic programs. In contrast to simulation (like MCMC), this analysis yields exact results. Our technique is based on weakest precondition reasoning. We will explain the foundations of this approach, present some proof rules to reason about probabilistic while-loops, and discuss how the analysis can be automated — either fully or with the help of invariants.

The material is available online.

The Caesar 2.2 is an incremental release that adds various improvements to existing features and fixes some bugs.

Overview:

1. UI Improvements
2. Guardrail Against Unsound Recursion
3. Better Model Checking Support
4. AST Rule Improvements
5. Other Changes

The paper "Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back" by Kevin Batz, Joost-Pieter Katoen, Francesca Randone, and Tobias Winkler was recently published at OOPSLA 2025.

Before this work, Caesar was able to only verify simple discrete probabilistic programs, i.e. programs that only sample from discrete distributions. This paper lays out the formal foundations for us to verify probabilistic programs that sample from continuous distributions, with support for loops, and conditioning. One challenge is to integrate the integrals for the expected values that arise from continuous distributions into the deductive verification framework of Caesar. The key idea is to soundly under- or over-approximate these integrals via Riemann sums. In addition to theoretical results such as convergence and completeness of the approach, the paper also provides case studies of continuous probabilistic programs that are encoded in HeyVL and verified with Caesar.

In this post:

1. Encoding Riemann Sums in HeyVL
2. Tortoise-Hare Race Example
3. Beyond The Continuous Uniform Distribution