This is the VSCode extension for the Caesar deductive verifier.
Caesar is a verifier for probabilistic and quantitative programs and thus supports reasoning about quantitative specifications such as "the expected runtime is at most 2x".
Caesar uses the HeyVL language as its quantitative intermediate verification language (IVL).
This VSCode extension recognizes the .heyvl file extension.
You can find more information about Caesar and HeyVL on the website: https://www.caesarverifier.org/.
On the website, you can also download the Caesar command-line binary for more advanced use cases that are not included in this VSCode extension.
The extension will open a walkthrough on first startup to guide you through the installation.
If this does not happen for you after installation, you can open the guide with the command Caesar: Show Getting Started.
The command palette can be opened with Shift + Command + P (Mac) / Ctrl + Shift + P (Windows/Linux).
- 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.
- Inline explanations of computed verification conditions.
- Automatic installation and updating of Caesar.
You will need to provide the Caesar binary for the extension to run. See installation instructions for more information.
We provide binaries for MacOS (ARM and x86-64), Windows (x86-64), and Debian/Linux (x86-64).
You can find Caesar's settings in the settings menu in the "Caesar" section.
This is a very new VSCode extension for Caesar. If you encounter any issues, feel free to open an issue.
On Github, we have a list of all of Caesar's releases along with binaries.