Mathematically prove properties about your Rust code. This extension integrates with cargo verify to provide real-time formal verification feedback directly in VS Code.
Features
Inline Diagnostics — Verification failures appear as squiggly underlines with counterexamples
SMT TreeView — Browse generated SMT-LIB2 scripts organized by module / function / verification condition
Counterexample Display — See concrete inputs that violate your specifications
Auto-Refresh — Results update automatically when you save or run cargo verify
rust-analyzer Integration — Works alongside rust-analyzer via check.overrideCommand
Z3 SMT solver (installed automatically with platform-specific builds, or install manually)
Rust nightly toolchain (specified in rust-toolchain.toml)
Quick Start
Install the extension
Open a Rust project with verification annotations:
#[doc = "rust_fv::requires::a <= u32::MAX - b"]
#[doc = "rust_fv::ensures::result == a + b"]
pub fn add(a: u32, b: u32) -> u32 {
a + b
}
Run Rust FV: Run Verification from the command palette (or save the file)
See results in the Rust FV sidebar and inline diagnostics
Supported Annotations
Annotation
Purpose
requires
Precondition — must hold when function is called
ensures
Postcondition — must hold when function returns
invariant
Loop or struct invariant
decreases
Termination measure for recursive functions
pure
Pure function usable in specifications
ghost
Ghost code for verification only
trusted
Skip verification for this function
How It Works
rust-fv hooks into the Rust compiler (rustc) via rustc_driver::Callbacks, extracts MIR (Mid-level Intermediate Representation), translates it to SMT-LIB2, and verifies properties using the Z3 theorem prover. If Z3 finds a counterexample, you get a concrete input showing exactly how your specification can be violated.
