Getting started on the command line

1. Install Verus.

To install Verus, follow the instructions at INSTALL.md.

2. Verify a sample program.

Create a file called getting_started.rs, and paste in the following contents:

use vstd::prelude::*; verus! { spec fn min(x: int, y: int) -> int { if x <= y { x } else { y } } fn main() { assert(min(10, 20) == 10); assert(min(-10, -20) == -20); assert(forall|i: int, j: int| min(i, j) <= i && min(i, j) <= j); assert(forall|i: int, j: int| min(i, j) == i || min(i, j) == j); assert(forall|i: int, j: int| min(i, j) == min(j, i)); } } // verus!

To run Verus on the file:

If on macOS, Linux, or similar system, run:

/path/to/verus getting_started.rs

If on Windows, run:

.\path\to\verus.exe getting_started.rs

You should see the following output:

note: verifying root module verification results:: 1 verified, 0 errors

This indicates that Verus successfully verified 1 function (the main function).

Try it on code that won’t verify

If you want, you can try editing the getting_started.rs file to see a verification failure. For example, if you add the following line to main:

assert(forall|i: int, j: int| min(i, j) == min(i, i));

you will see an error message:

note: verifying root module error: assertion failed --> getting_started.rs:19:12 | 19 | assert(forall|i: int, j: int| min(i, j) == min(i, i)); | ^^^^^^ assertion failed error: aborting due to previous error verification results:: 0 verified, 1 errors

3. Compile the program

The command above only verifies the code, but does not compile it. If you also want to compile it to a binary, you can verus with the --compile flag.

If on macOS, Linux, or similar system, run:

/path/to/verus getting_started.rs --compile

If on Windows, run:

.\path\to\verus.exe getting_started.rs --compile

Either will create a binary getting_started.

However, in this example, the binary won’t do anything interesting because the main function contains no executable code — it contains only statically-checked assertions, which are erased before compilation.

4. Learn more about Verus

Continue with the tutorial, starting with an explanation of the verus! macro from the above example.