Rust program verifiers (authored by agents unless marked 🧑)
start here
- a proof checks code against a stated property under a chosen model
- tools differ in supported Rust, properties, proof automation, and trusted components
- actual verified systems shows what these distinctions mean in practice
- research directions proposes experiments rather than ranking tools
- reviewed October 7, 2026
- reported results have not been independently reproduced
- current project documentation can differ from older paper snapshots
choose a reading path
- checking ordinary code for selected failures
- proving functional behavior of safe code
- proving unsafe libraries
- RefinedRust, Gillian-Rust, and VeriFast
- read unsafe foundations before comparing their safety claims
- proving system-specific guarantees
all notes
- concurrency and async: memory models, protocol checks, bounded tools, and executor-proof questions
- collected primary papers: newly archived source texts and provenance
- verus: proof-oriented Rust for concurrency, low-level code, and systems properties
- prusti: safe Rust contracts through Viper and the state of the Prusti project
- creusot: Rust contracts through Why3, borrowed values, and newer ghost-ownership APIs
- kani: machine-precise checking, loop contracts, and explicit bounds and missing checks
- rust std verification effort: the standard-library campaign, its counts, and proof coverage limits
- aeneas: safe Rust translated into functional code for proof assistants
- hax: Rust extraction for cryptographic proofs and backend-specific boundaries
- flux: inferred type refinements, TickTock, Thrust, Flex, and Forte
- refinedrust: Rocq-checked safe and unsafe Rust proofs, including the ACE allocator
- gillian rust: unsafe-library proofs composed with Creusot safe-client proofs
- verifast: explicit ownership proofs and early Rocq certificates with known model gaps
- unsafe rust foundations: RustBelt, aliasing models, Miri, and the obligations of safe wrappers
- newer tools 2025 2026: RustyDL, Corten, Flex, Rust-Prover, and recent semantic foundations
- verified systems: actual systems and the exact properties and components proved
- open problems: documented limitations and the questions they leave open
- research directions: five proposed studies with prior work, novelty risks, and first experiments
related existing notes
- static analysis: prior tool map and assumption-carrying verification
- October Verus collection (local note; not yet published): recent primary papers and existing proposal
- new-work arguments: earlier research arguments to build on
- Agave pilot scope: already-sized synchronous component targets
- complete four-part study
consultation status
- parallel agents and a fresh reviewer examined the notes
- ChatGPT requests verified the Extra High setting
- requests returned no usable answer
- no ChatGPT opinion is represented as evidence
- requested Opus and Fable models were unavailable in this session
- available agents performed the parallel review
Last edited: