RustBelt and IrisFoundational separation-logic verification of Rust's safe / unsafe core, and its 2024-2026 RefinedRust successor.
VerusMicrosoft Research's SMT-backed Rust verifier, the leading tool for verified systems software at scale in 2025-2026.
CreusotA deductive verifier for safe Rust that compiles to Why3 and discharges to off-the-shelf SMT solvers.
KaniAWS's bit-precise bounded model checker for Rust, deployed in CI on Firecracker and the standard library.
AeneasRust verification by functional translation: compile Rust to a pure lambda calculus, verify there.
CompCert and the Verified-Compiler ToolchainThe production-grade formally verified C compiler, the CompCertO / Owlang line, and why it matters for JIT verification.
CakeML and the Verified-JIT LineThe bootstrapping verified ML compiler, its 2024 PLDI agenda, and the FM-JIT verified-JIT effort that builds on it.
Formal Models of the Rust Borrow CheckerStacked Borrows, the 2025 Tree Borrows replacement, and the trajectory of NLL / two-phase formalisation.
Separation Logic for Managed (GC'd) HeapsIris-based separation logics with space credits, tracing GC, and the 2025 IrisFit + Nextgen-Modality lines.
Capability-Machine Formalism and Endorsement RelationsCerise, the CHERI-C Coq memory model, and capability-safety logical relations as the formal model behind handle-based runtimes.