# Verus overview Verus is a tool for verifying the correctness of code written in Rust. The main goal is to verify full functional correctness of low-level systems code, building on ideas from existing verification frameworks like [Dafny](https://github.com/dafny-lang/dafny), [Boogie](https://github.com/boogie-org/boogie), [F*](https://github.com/FStarLang/FStar), [VCC](https://www.microsoft.com/en-us/research/project/vcc-a-verifier-for-concurrent-c/), [Prusti](https://github.com/viperproject/prusti-dev), [Creusot](https://github.com/xldenis/creusot), [Aeneas](https://github.com/AeneasVerif/aeneas), [Cogent](https://github.com/NICTA/cogent), [Rocq](https://rocq-prover.org/), and [Isabelle/HOL](https://isabelle.in.tum.de/overview.html). Verification is static: Verus adds no run-time checks, but instead uses computer-aided theorem proving to statically verify that executable Rust code will always satisfy some user-provided specifications for all possible executions of the code. In more detail, Verus aims to: - provide a pure mathematical language for expressing specifications (like Dafny, Creusot, F*, Rocq, Isabelle/HOL) - provide a mathematical language for expressing proofs (like Dafny, F*, Rocq, 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, Creusot, and Aeneas) - generate small, simple verification conditions that an SMT solver like [Z3](https://microsoft.github.io/z3guide/docs/logic/intro) 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, Creusot, Aeneas, and [linear Dafny](https://github.com/secure-foundations/dafny/tree/betr/docs/Linear)) We believe that Rust is a good language for achieving these goals. Rust combines low…