Goals

This fork of Rust is for developing 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