Skip to main content

· 5 min read
Philipp Schroer

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


  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

Caesar Verifier Visual Studio Code Extension

Our new Caesar Verifier VSCode extension is now the recommended way to use Caesar. The extension is available in the VSCode and VSCodium extension marketplaces and can be installed by searching for Caesar Verifier.

The extension is built on the Language Server Protocol and uses the Caesar binary under the hood.

Go to Caesar Verifier on VSCode Marketplace


  • Syntax highlighting and language configuration for HeyVL.
  • Snippets for HeyVL.
  • Verify HeyVL files on file save or on command.
  • Verification errors and successes are shown in the gutter via icons.
  • Diagnostics such as errors or warnings are shown in the code and in the "Problems" menu in VSCode powered by slicing!
  • Inline explanations of computed verification conditions (shown in picture!).
  • Automatic installation and updating of Caesar.

Slicing for Error Reporting and Correctness

Assertion Slicing

The error reports in Caesar are driven by the first implementation of specification-based slicing for probabilistic programs. By default, our slicing implementation is used to identify which assert-like statements are responsible for errors (Caesar's assertion slicing).

An example is shown on the right. The slicing algorithm has determined that the invariant might not be inductive and could rule out e.g. that the pre does not entail the invariant.

Caesar's slicing does not operate on high-level programs with loops, but instead on the low-level HeyVL statements, including verification statements. This enables error reporting (and other slicing applications) for any verification problems that you can encode in HeyVL. Custom error messages can be added via slice message annotations.

Assumption Slicing

Whereas assertion slicing is concerned with finding a minimal set of assertions in the program so that the program still has an error, assumption slicing tries to find a minimal set of assumptions so that the program still verifies.

In the example on the right, we can see a slightly modified version of the geometric loop example from above. Now it has a constant starting value of zero. With the correct invariant, the program verifies. But Caesar can also tell us that this while loop could also be an if statement no loop is required to satisfy the specification. The interpretation of this result is up to the user. Maybe the program can be simplified, but maybe the specification is not as strong as one thought and needs to be strengthened!

General Slicing

Caesar's implementation of slicing is not restricted to verification statements such as assertions and assumptions. With program annotations, Caesar can be instructed to run slicing for correctness and try to eliminate unnecessary assignments from the program.

In the example on the right, we have a probabilistic program that encodes a Bayesian network.1 We have added the @slice_verify annotation to have Caesar also try to slice assignments. Caesar determined that most assignments are not necessary to satisfy the specification.

There is also a corresponding @slice_error annotation to do slicing for errors on statements that are not assert-like.

Calculus Annotations for Proof Rules

Caesar's HeyVL was designed as a quantitative intermediate verification language, therefore it allows encoding all sorts of potentially unsound proof rules. To make it easier to use Caesar to verify high-level programs with loops with respect to well-known expectation-based calculi and proof rules, we have added calculus annotations to Caesar. They are @wp, @wlp and @ert. When they are added to a proc/coproc, Caesar will do some additional checks to ensure that proof rules are actually sound.

Model Checking Support via JANI

While deductive verification can deal with infinite state spaces, infinite data types, and is generally pretty awesome, sometimes you want to analyze a proabilistic program whose state space can be finitely represented. With Caesar's model checking support via JANI, you can export your probabilistic program to the JANI format to use probabilistic model checkers.

Caesar's support is limited to executable probabilistic programs. That means that quantitative verification statements like assert, assume, and havoc are restricted or not supported.

Caesar's JANI export was designed as a replacement for the recently deleted storm-pgcl, and can now be used as a pGCL frontend for model checkers that accept JANI inputs.

· One min read
Philipp Schroer

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.

Caesar was originally built in part through FRAPPANT, the 2018 ERC Advanced Grant "Formal Reasoning about Probabilistic Programs: Breaking New Ground for Automation". The new ERC Proof of Concept research proposal "A Deductive Verifier for Probabilistic Programs (VERIPROB)" is about applying knowledge from FRAPPANT to build Caesar into a prototype that can be made use of by industry "to turn science into practice".

See also the press release by the university and the ERC announcement.

· One min read
Philipp Schroer

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 talk starts at timestamp 7:16:23 and ends at timestamp 7:34:00.

· One min read
Philipp Schroer

Philipp Schroer and Joost-Pieter Katoen receive a Research Award from WhatsApp, through its parent company, Meta Platforms, Inc. for their research proposal “A Deductive Verification Infrastructure for Probabilistic Programs”. Out of 62 research proposals that were submitted to WhatsApp Privacy Aware Program Analysis, 6 projects have been awarded. For more information, see here.