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

The Caesar 2.1 release adds contains various improvements to existing features and fixes some bugs.

Overview:

1. UI and Documentation Improvements
2. More Guardrails
3. Slicing Improvements
4. Minor Fixes

The paper "A Game-Based Semantics for the Probabilistic Intermediate Verification Language HeyVL" by Christoph Matheja was published at AISoLA 2024 and is now available online.

We are happy to announce Caesar 2.0: the next release of Caesar packed with a lot of new features.

Overview:

1. Caesar Verifier Visual Studio Code Extension
2. Slicing for Error Reporting and Correctness
3. Calculus Annotations for Proof Rules
4. Model Checking Support via JANI

We are happy to announce that RWTH's MOVES group, headed by Prof. Joost-Pieter Katoen, will receive funding from the European Research Council (ERC) for a Proof of Concept Grant to improve Caesar.

On January 14, 2024, I presented Caesar and the basics of our quantitative intermediate language HeyVL at the Dafny 2024 workshop. The workshop was part of the POPL 2024 conference.

The artifact associated with our OOPSLA '23 publication A Deductive Verification Infrastructure for Probabilistic Programs has received the Distinguished Artifact award, praising exceptionally high quality.

HeyVL and Caesar were accepted at OOPSLA '23: A Deductive Verification Infrastructure for Probabilistic Programs by Schröer et al. The artifact received the reusable badge, which is the highest possible badge.