To run verification, invoke Verus with the crate-type library on the src/lib.rs file:
$ verus --crate-type=lib src/lib.rs
Currently, Verus works by invoking rustc and Cargo support is on the way.
To support cross-crate verification, we need to run commands like these:
For the lib crate
verus --crate-type=lib --export vl.vir src/lib.rs
For the main crate
verus src/main.rs --extern=verified_lib -L target/debug/deps --import verified_lib=../verified_lib/vl.vir
- Mutable reference(
&mut T) as return value or struct field not supported &mut data[i]not supported- Deref type conversion not supported
- Comparison operators for non SMT-arith types not supported
- Insufficient external specification for
stdinvstd - Supports atomic primitives with only sequential consistency ordering
- Floating point numbers unsupported
- Language items
std-only features- High level invariants
-
Ghost code: specifies all safety invariants explicitly and statically checks them
- Number of safety conditions in STD comments
rg -i --type rust '^\s*//.*safety:' -o | wc -l 2475
- Panic possibility in STD comments
rg -i '^\s*//[/!]+\s*#\s*Panics' | wc -l 397
- Number of safety conditions in STD comments
-
Eliminates debug and runtime asserts in STD
- Number of runtime assertions:
rg -i --type rust '^(?!\s*//).*assert!' --pcre2 | wc -l 9089
- Number of debug assertions
rg -i --type rust '^(?!\s*//).*debug_assert!' --pcre2 | wc -l 678
- Number of runtime assertions:
-
Removes redundant safety abstractions
-
Verus by default checks for possible arithmetic overflow/underflow.
- Select an abstract model(
impl View) of the target data structure. For example,BinaryHeap<T>can be represented asSeq<T> - Define a well-formedness specification(usually recursively) in terms of the abstract model. For example, in a
BinaryHeap, both left and right children are less than or equal to their parent. For allpub fn x(&mut self, ...)API, the precondition and postcondition both include well-formedness.- There are usually more than one way to define well-formedness: bottom-up, top-down, etc. Need to find one that is easy for Verification.
- Reuse spec and proof code blocks as functions like regular programming.
- Write external specifications for functions, types and traits that are out of the scope of verification.
- Use assumptions to temporarily finish proofs.
The examples directory contains small code snippets we write for testing Verus features.
- Develop and debug proofs like programming
- Refactor specs and proofs like refactoring code
- Incrementally prove stronger properties
- Linear ghost state, ghost tokens
- Rust Compiler
- Verus itself including vstd
- The specifications
- All assumptions in the proofs:
admit(),assume(),#[verifier::external_body],assume_specificationetc - An implicit assumption: the internal data structures of the std are only mutated by external code through the public API. It is difficult to enforce this in memory unsafe languages like C/C++ but easy in Rust: if all external Rust code is safe Rust.