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.