Verus -- SMT-based verification of Rust systems code

Abstract:

We are building Verus, a new tool for semi-automatic verification of Rust code using an SMT solver (Z3). Verus can efficiently verify full functional correctness of low-level systems code written in a safe Rust dialect that supports expressing specifications and proofs. Verus leverages the fact that safe Rust has a natural, direct encoding in SMT (for code without interior mutability, which we need to address separately). Algebraic data types (ADTs) and sound generics complement safe Rust to make it a solid basis for a mathematical language for expressing specifications and proofs.

In this talk I'll discuss Verus' design, its mathematical language to express specification and proofs built from a subset of Rust, and how Verus prioritizes lean, efficient encoding of safe Rust to SMT queries. I will present Verus' features that aid verification of complex systems, such as linear ghost variables: these are proof-time variables that are not compiled, but retain the unique-ownership and safe reference rules established by the borrow checker. Linear ghost variables let us efficiently reason about interior mutability and shared-memory concurrency, and let us provide safe alternatives for many situations where unsafe would be required in vanilla Rust.

About the speaker:

Andrea is a researcher for VMWare Research, previously he was a PhD candidate in ETH Zurich's Systems Group.