Tutorial: Verifying Rust code with Verus

Setting up Verus

There are two options, listed below: setting up Verus natively (which requires installing rust on your system) or running Verus in an `x86_64` Docker container.

Option A: Download Verus release and install rust toolchain (if necessary)

To get Verus, download the relevant package from this release page: https://github.com/verus-lang/verus/releases (open the "Assets" dropdown and select your platform).

If you're on MacOS the binaries and libraries will be quarantined by Gatekeeper, which will pop up a number of messages about running software downloaded from the internet. To avoid this issue, once you have unpacked the `zip` file, open a shell in the newly unzipped directory and run `bash macos_allow_gatekeeper.sh`, which will remove the Gatekeeper quarantine flag from all the relevant files (you can inspect the file first, if you'd like, it only makes changes inside the directory you just unpacked).

You can then run Verus with ./verus (or .\verus.exe on Windows). If you already have `rustup` installed, `verus` will instruct you on how to install the necessary rust toolchain (1.79.0). If you don't have `rustup` installed, `verus` will instruct you on how to install it, and the necessary rust toolchain (1.79.0). `rustup` is Rust's installer.

Option B: Use Verus via Docker

If you have a machine that can run Linux `x86_64` docker containers, you can also use a docker image we've prepared for the tutorial to run `verus` without having to install any dependencies separately.

From the directory that contains the files you want to verify (e.g. a file named `fibo.rs`), run:

docker run -it --rm -v .:/root/cwd ghcr.io/verus-lang/verus verus fibo.rs

This will download the Verus container and mount the current folder as /root/cwd  which corresponds to the working directory inside the container and will let Verus find the file `fibo.rs` in this case.

Verifying your first program

To check that Verus is properly installed, please download fibo.rs and run Verus on it.

If you set up Verus with Option A, you can verify the fibo.rs example with ./verus path/to/fibo.rs (or .\verus.exe path\to\fibo.rs on Windows).

If you set up Verus with Option B, make sure that fibo.rs is in the current working directory, and then you can verify it with
docker run -it --rm -v .:/root/cwd ghcr.io/verus-lang/verus verus fibo.rs.

You should get the following output:
verification results:: 4 verified, 0 errors

Verus Standard Library (vstd) documentation

The Verus Standard Library documentation is accessible at: https://principled-systems.github.io/verus/verusdoc/vstd/