Rust verification tools (2021)

This is a list of Rust verification tools with a bias towards ‘formal methods’ tools. An update of Alastair Reid's 2020 list. Tool types are listed in approximate (and subjective!) increasing order of the level of expertise required and approximate increasing order of the level of assurance that they provide.

Dynamic checking tools

  • Miri for general UB checking (including data race detection, but only on a single execution) Concurrency checkers
  • Loom, which focuses on exhaustive checking
  • Shuttle, which focuses on randomized checking

Automatic verification tools

Typically relies on a verification harness to generate symbolic input values for the code under test (although those can sometimes be generated from the function argument types). Typically checks assertions, panics, overflows, etc.

Bounded model checking / Static Symbolic Execution

Abstract interpreter ++

Dynamic Symbolic Execution

  • RVT Rust → LLVM → {KLEE,SeaHorn} Plus a DSL for writing verification harnesses based on the property-based testing library proptest
  • Haybale symbolic execution engine for LLVM written in Rust
  • Seer symbolic execution engine based on Miri (not sure it is active)
  • KLEE-Rust KLEE bindings for Rust (inactive for 6 years) Unbounded (?)

Fully Automated Verification

  • RustHorn Automated loop-invariant finding by reduction to CHCs; First proposed the 'prophetic' verification method of Rust

Auto-Active Verification

Midway between automatic and interactive verification. Relies on hints/annotations/etc inserted in source code such as function contracts, loop invariants, data structure invariants, etc.

Interactive verification

Converts Rust to code in an interactive theorem prover which is then verified with human input. This allows one to treat more complex programs.

Very safe subset of rust

  • HacSpec A specification language for cryptographic primitives in Rust. Has backends in F-star, Coq and EasyCrypt. Also has non-cryptographic applications: riot bootloader, the part of the bootloader that selects which image to boot : involves a small hash algorithm and a list traversal. RIOT link

Coq

  • ConCert extracts functional programs in Coq to Rust by using arenas. It originated from smart contract verification.
  • fiat cryptography is a verified compiler for cryptographic primitives in Coq that generates Rust implementations (and other languages). WIP on extending bedrock2 with a rust printer.

Interactive verification of the foundations of Rust

  • RustBelt Semantics close to MIR, focuses on verification of unsafe code,

Interactive verification of core subsets of Rust

  • Oxicide, arxiv link type systems account of Rust's borrow checker, close to surface rust.
  • WASMCert Formalization of the wasm standard
  • VeLLVM Formalization of the LLVM compilation infrastructure

LEAN prover

  • Electrolysis Rust → LEAN translator (no longer active, MSc thesis)

Standardization/Specification

  • HacSpec A specification language for cryptographic primitives in Rust.
  • Ferrocene (previously called Sealed Rust)