Verifying the Rust Standard Library
For Rust developers and the formal-methods community, this work demonstrates a practical, crowdsourced approach to verifying a widely-used library's unsafe code, though it is incremental in nature.
The paper presents the largest verification campaign for a software library, integrating complementary verification tools into the continuous integration of a forked Rust standard library to statically verify unsafe code, and analyzes its effectiveness in preventing undefined behaviors.
Rust's type system prevents many classes of memory errors, yet its standard library relies heavily on unsafe code whose correctness is validated through testing, including dynamic checks under Miri, but lacks static verification. We present what is, to the best of our knowledge, the largest verification campaign reported for a software library: an open, crowdsourced effort that integrates complementary verification tools into the continuous integration of a verification repository forked from the Rust standard library. We analyze the campaign's effectiveness, discuss the practical value of machine-checked proofs for a subset of undefined behaviors (e.g., out-of-bounds access, null and dangling pointer dereferences, and use of uninitialized memory), and frame the remaining obstacles as open challenges for the formal-methods community.