Caesar is a deductive verification platform for probabilistic programs. It accepts input in a verification language called HeyVL. Caesar generates so-called verification conditions of the HeyVL input program(s). These verification conditions are in the form of logical formulas of a logic we call HeyLo. If the verification conditions are valid, then we say the HeyVL program verifies. If a counter-example is found, Caesar will reject the input program.
This is research software and we're still working on a nice user interface, documentation, and fixing bugs. Do not hesitate to open an issue or send an email to [email protected] with questions or ideas. I am also happy to discuss anything via Zoom as well!
The documentation is available at www.caesarverifier.org. Start at with the introduction, then walk through the getting started guide.
We have an OOPSLA 2023 paper on Caesar and its theory: A Deductive Verification Infrastructure for Probabilistic Programs. You can find the preprint on arxiv.
There is also a development guide if you want to work on Caesar itself.