Verifying the Rust Standard Library
summary
Amazon and the Rust Foundation run a verification contest that aims to formally prove the Rust standard library’s unsafe code cannot cause undefined behavior, maintaining a fork where 25 challenges live and 5 resolved so far; proofs must run in CI and merge into the fork, with reviewers on a technical committee and three approved tools plus two under review. Carnegie Mellon students used Connie to verify examples, and tool adopters may earn a $25,000 reward for acceptance.
AI-written summary · about
chapters (6)
- 0:00Safety and unsafe in Rust
- 1:27Verifying standard library
- 4:34Contest and project logistics
- 8:32Case study on verification
- 18:15Future goals and community
- 23:19Q&A session
related talks
10mVerifying the Rust Standard Library
19mA Hybrid Approach to Semi-automated Rust Verification
21mA Tour of Empirical Verification in Rust
31mValidating Rust for industry: Certification meets formal analysis
22mRust as a Foundation for a Safe and Sustainable Future
58mRust for The Curious C++ Developers
46mPanel: Rust in Safety Critical
56mRust for Foundation Software