Verus is an experimental verification framework for Rust-like code. The main goal is to verify full functional correctness of low-level systems code, building on ideas from existing verification frameworks like Dafny, Boogie, F*, VCC, Prusti, Cogent, Coq, and Isabelle/HOL.
Goals:
- provide a pure mathematical language for expressing specifications (like Dafny, F*, Coq, Isabelle/HOL)
- provide a mathematical language for expressing proofs (like Dafny, F*, Coq, Isabelle/HOL) based exclusively on classical logic (like Dafny)
- provide a low-level, imperative language for expressing executable code (like VCC), based on Rust (like Prusti)
- generate small, simple verification conditions that an SMT solver like Z3 can solve efficiently, based on the following principles:
- keep the mathematical specification language close to the SMT solver's mathematical language (like Boogie)
- use lightweight linear type checking, rather than SMT solving, to reason about memory and aliasing (like Cogent and linear Dafny)
We do not intend to ...
- ... support all Rust features and libraries (instead, we will focus a subset that is easy to verify)
- ... verify unsafe Rust code (instead, verification will rely on Rust's type safety, as ensured by Rust's type checker)
- ... verify the verifier itself
- ... verify the Rust/LLVM compilers