I'm going to talk about the tool we've been building, called Verus, which is a tool to verify Rust, and specifically to verify Rust code in the domain of system software: operating systems, file systems, things like that.

This post is based, in part, on the talk "Verified Rust for low-level systems code - Rust Zürisee June 2023".

Checking code correctness with testing

Instead of trying to explain what verification is, I'm just going to jump into an example. You're writing a very simple max function here. What you might do is try to write a test for it.

1
fn max(a: u64, b: u64) -> u64 {
2
    if a >= b { b } else { a }
3
}
4

5
fn max_test_1() {
6
    let x = 4;
7
    let y = 4;
8
    let ret = max(x, y);
9
    assert!(ret == 4);
10
}
11

12
fn main() {
13
    max_test_1();
14
    println!("success");
15
}

I'm keeping things extremely simple here, just writing a simple test. We have a max function, we call it with certain arguments, and check that the result is the one we expect. If we run this program, it passes. We wrote a test, it passes, we're happy.

You may have already spotted the problem here. Two problems, in fact: there's a bug, but also that the test case I wrote was insufficient. It was testing a very specific case and didn't catch the "edge" case. You could go and write another test and run it, and now finally, we get the test failing because we swapped DNA over here.

1
fn max_test_2() {
2
    let x = 4;
3
    let y = 3;
4
    let ret = max(x, y);
5
    assert_eq!(ret, 4);
6
}
7

8
fn main() {
9
    max_test_1();
10
    max_test_2();
11
    println!("success");
12
}

That's how test-based development works, and it can work well. One needs to pay attention that the tests they write will catch edge cases or unexpected behavior. Let's see if we can do better: the way I'm writing this next test is a bit different. Instead of writing the return value that we expect exactly, I'm stating the property I want the return value to have.

1
fn max_test_3() {
2
    let x = 4;
3
    let y = 3;
4
    let ret = max(x, y);
5
    assert!(ret == x || ret == y);
6
    assert!(ret >= x && ret >= y);
7
}
8

9
fn main() {
10
    max_test_3();
11
    println!("success");
12
}

I'm saying the return value here should be either of the two arguments and should be the greater one of the two. In this test we would fail the assertion on line 6, because max is not returning the maximum.

When writing tests you have to write a test case for each point in the input space of this function, but you never really know that you've caught all the possible issues and bugs because you can't possibly test for all the cases.

From tests to formal specifications

To use our tool, Verus, we need to re-organize the code a bit.

1
use vstd::prelude::*;
2
verus! {
3

4
fn max(a: u64, b: u64) -> u64 {
5
    if a >= b { a } else { b }
6
}
7

8
fn max_test() {
9
    let x = 4;
10
    let y = 3;
11
    let ret = max(x, y);
12
    assert(ret == x || ret == y);
13
    assert(ret >= x && ret >= y);
14
}
15

16
} // verus!

I took the max function from before, fixed the issue, and then wrote Verus assertions as part of the max_test functions (on lines 12 and 13): these look different from regular rust assertion but I'm keeping the property that we wanted: the return value is either of the inputs and it is greater or equal to both.

error: assertion failed
  --> /Users/andreal1/Demo/A2-program-0.rs:13:12
   |
13 |     assert(ret == x || ret == y);
   |            ^^^^^^^^^^^^^^^^^^^^ assertion failed

error: assertion failed
  --> /Users/andreal1/Demo/A2-program-0.rs:14:12
   |
14 |     assert(ret >= x && ret >= y);
   |            ^^^^^^^^^^^^^^^^^^^^ assertion failed

error: aborting due to 2 previous errors

verification results:: 1 verified, 1 errors

The error message we get from Verus is different; it's not a panic. We actually never run the code here. What Verus does is it statically checks every possible way that the program could run and checks whether these assertions are true in every possible case.

...