Test-Driving the Rust Model Checker (RMC)

The Rust Model Checker (RMC) allows Rust programs to be model checked using the C Bounded Model Checker (CBMC). In essence, RMC is an extension to the Rust compiler which converts Rust’s MIR into the input language of CBMC (GOTO).

Using RMC provide can provide much stronger guarantees than, for example, testing with cargo-fuzz or proptest. To understand how it works, I’m going to walk through the process of checking the following simple function:

This is a good function for testing verification systems, since it has some nice post-conditions. To get started we need to add some helper methods, the first of which is:

This function is known to RMC and has special significance. Here, __nondet<T>() returns a non-deterministic value. We can think of this as an arbitrary value of the type T in question. This is where the power of RMC comes from as, instead of testing individual values of T, we’re testing all possible values of T! The second helper method we need is this:

Again this has specifical significance to RMC and, as we’ll see, it is used for constraining non-determinstic values. For example, we might do something like this:

Leave a Comment