Skip to content

Latest commit

 

History

History
15 lines (13 loc) · 1.75 KB

project-goals.md

File metadata and controls

15 lines (13 loc) · 1.75 KB
Raw

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