Skip to main content

Installing Caesar

Caesar can be used through our VSCode extension and as a command-line application. The required Caesar binary can be downloaded automatically by the VSCode extension. You can also download binaries manually, pull a Docker image, or build locally from source.

Our Caesar Verifier for VSCode extension is the recommended way to install Caesar. The extension can automatically download and update the pre-built releases of Caesar.

The extension is available in the VSCode and VSCodium extension marketplaces and can be installed by searching for Caesar Verifier.

Go to Caesar Verifier on VSCode Marketplace

Features:

  • 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.

Installation: After installing the extension in VSCode, a getting started page will open from where you can install the Caesar binaries (open manually with Caesar: Open Getting Started command).

The extension is also published on the Open VSX Registry if you are using VSCodium.

Options B: Download Pre-Built Releases​

If you do not want to use the automatic installation from our VSCode extension, you can download Caesar manually.

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. 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

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 example, if you want to verify a program in ./programs/example.heyvl, the following command mounts the ./programs/ directory as /root/caesar/programs/ inside the container and uses caesar to verify example.heyvl.

docker run -it -v $PWD/programs:/root/caesar/programs/ ghcr.io/moves-rwth/caesar:latest /root/caesar/programs/example.heyvl

Options 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 DevContainer configuration is available in the .devcontainer folder and can be used with e.g. the DevContainer VSCode extension by running 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.

Then, you can run an example:

caesar verify tests/zeroconf.heyvl

And this will print:

tests/zeroconf.heyvl::arp: Verified.
tests/zeroconf.heyvl::zeroconf: 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. For example, if you want to verify a program in ./programs/example.heyvl, the following command mounts the ./programs/ directory as /root/caesar/programs/ inside the container and uses caesar to verify example.heyvl.

docker run -it -v $PWD/programs:/root/caesar/programs/ caesar /root/caesar/programs/example.heyvl