Our tool paper "Caesar: A Deductive Verifier for Probabilistic Programs" was accepted as a tool paper at CAV 2026, to be held in Lisbon, Portugal. The authors are Philipp Schröer, Kevin Batz, Umut Yiğit Dural, Darion Haase, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja.

The paper reports on five years of Caesar development and presents Caesar as a deductive verifier for probabilistic programs in its current form: from the HeyVL/HeyLo core and the SMT-based pipeline via Z3 to the surrounding tooling and verification features. Compared to our earlier OOPSLA 2023 paper, which introduced the formal foundations of HeyVL and HeyLo, the new tool paper focuses on Caesar as a practical verification tool. Among the additions highlighted in the paper are the Caesar Verifier VSCode extension, support for limited functions and improved quantifier handling, the model checking backend via JANI and Storm, stronger soundness checks and guardrails for proof-rule usage, and slicing-based diagnostics.

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