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.