Verus: Verifying Rust Programs Using Linear Ghost Types

Explore a groundbreaking 18-minute conference talk from OOPSLA 2023 that introduces Verus, an innovative SMT-based tool for formally verifying Rust programs. Delve into how Verus leverages Rust's powerful type system to prove functional correctness properties beyond type safety in low-level, high-assurance systems. Learn about the novel mode system that distinguishes between specifications, executable code, and proofs, allowing for effective manipulation of linearly typed permissions. Discover the tool's applications through various examples, including pointer manipulation, interior mutability, and concurrent code. Gain insights into the formalization of Verus' linearity, borrowing, and modes in a small lambda calculus, with proofs of type safety and termination. This talk, presented by a team of researchers from VMware Research, Carnegie Mellon University, ETH Zurich, UNSW Sydney, and Microsoft Research, offers a deep dive into advanced program verification techniques for Rust developers and researchers in formal methods.