Skip to main content

Installing Caesar

The VS Code extension installs Caesar and lets you verify HeyVL files in the editor. For command-line use, download a binary, use Docker, or build from source.

Caesar in VS Code, showing a verified geometric loop and inline verification conditions.

Install Caesar for VS Code

  1. Install Caesar Verifier from the VS Code Marketplace or, for VSCodium, the Open VSX Registry.
  2. Follow the extension's getting-started page to download the Caesar binary. You can reopen it from the command palette with Caesar: Show Getting Started.
  3. Open the HeyVL file from First Example: Expected Runtime and save it to run verification.

The extension shows verification results next to the code, reports diagnostics, and explains verification conditions inline. It also provides syntax highlighting, snippets, and automatic updates of Caesar. See the extension documentation for its commands and settings.

The following installation methods are alternatives for using Caesar from a terminal.

Option B: Download Pre-Built Releases​

Option B.1: Pre-Built Binary​

  1. Go to the latest stable release on GitHub (or latest nightly release) and download the release for your operating system.

  2. Extract the caesar binary from the downloaded archive.

  3. Add its directory to your PATH to run caesar from any folder. Alternatively, use ./caesar from the extracted directory (.\caesar.exe in PowerShell).

  4. On macOS, you may have to release the binary from quarantine to allow execution.

    # Execute in the extracted folder
    xattr -d com.apple.quarantine ./caesar

Continue with First Example: Expected Runtime to verify a program with caesar verify.

Option B.2: Docker Image​

We also provide a Docker image (multi-platform targeting linux/amd64 and linux/arm64).

docker pull ghcr.io/moves-rwth/caesar:latest

You can use this Docker image just like the caesar binary. To access files from your system you need to mount them as volumes. For the first example, save geometric-runtime.heyvl in a directory named programs, then run:

docker run --rm -v "$PWD/programs:/programs" ghcr.io/moves-rwth/caesar:latest verify /programs/geometric-runtime.heyvl

This mounts the local programs directory at /programs inside the container.

Option C: Build From Source​

Option C.1: Compile Binary​

Installing Dependencies​

Compiling Caesar requires a few dependencies. You can either

  1. install them manually (see below) or
  2. use the provided DevContainer configuration. The configuration is in the .devcontainer folder and can be opened in VS Code with the Dev Containers: Open Folder in Container... command.

Rust: To install Rust, we recommend installation via rustup. You might need to restart your terminal after installing Rust.

Build Tools: Caesar builds Z3 itself, so we need Python and cmake.

  1. Install Rust via rustup:
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
  1. Install Python and CMake using the package manager Homebrew:
brew install python cmake

Compiling Caesar​

  1. Clone the Git repository:
git clone https://github.com/moves-rwth/caesar.git
cd caesar
  1. Build caesar using cargo:
cargo install --path . caesar

Because this will compile a large number of dependencies, this might take a couple of minutes (especially Z3 takes some time). Using cargo install makes caesar available on the command-line.

From the repository root, verify the first example:

caesar verify website/static/examples/geometric-runtime.heyvl

Caesar reports that geo_expected_runtime is verified.

Option C.2: Build Docker Image​

We also support building a Docker image. This does not require installing dependencies and will build and package the caesar binary in a Docker image.

  1. Clone the Git repository:
git clone git@github.com:moves-rwth/caesar.git
cd caesar
  1. Build the Docker image, named caesar, using docker build:
docker build -t caesar -f docker/Dockerfile .
Multi-platform image

You can build and load a multi-platform image using docker buildx:

docker buildx build --platform linux/amd64,linux/arm64 -t caesar -f docker/Dockerfile . --load

With the Docker image caesar built, you can use it just like the caesar binary. To access files from your system you need to mount them as volumes. From the repository root, verify the same example by mounting its directory into the container:

docker run --rm -v "$PWD/website/static/examples:/examples" caesar verify /examples/geometric-runtime.heyvl

Continue with First Example: Expected Runtime for an explanation of the program, its annotations, and the verification result.