Verifying the Rust Standard Library
Talkat RustConf 2026 · on Thursday, 2026-09-10· at 10:20· Room 511 | Palais des Congrès de Montréal, Palais des Congrès de Montréal·
summary
Project verifies 12,000+ functions verified in the Rust standard library, integrates eight verification tools (Kani, Verus, Prusti, …) into CI, and solves correctness challenges such as functional correctness of LinkedList, safety of NonZero, and SIMD intrinsics. Ten challenges are completed, 19 remain open, and 68 contributors have earned $250,000 in awards so far. AI assists specification drafting and proof search, while proofs must rerun on every stdlib change to keep guarantees current.
AI-written summary · about
related talks
33mVerifying the Rust Standard Library
19mA Hybrid Approach to Semi-automated Rust Verification
21mA Tour of Empirical Verification in Rust
22mRust as a Foundation for a Safe and Sustainable Future
31mValidating Rust for industry: Certification meets formal analysis
24mThe road to compiling the standard library with gccrs
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
58mRust for The Curious C++ Developers