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.

翻译：Rust 的类型系统能防止多种内存错误，但其标准库高度依赖不安全代码，这些代码的正确性目前主要通过测试（包括在 Miri 下的动态检查）来验证，缺乏静态验证。我们呈现了据我们所知针对软件库所报道的最大规模验证活动：一项开放、众包式的努力，将互补的验证工具集成到一个从 Rust 标准库分叉的验证仓库的持续集成中。我们分析了该活动的有效性，讨论了机器检查证明对于部分未定义行为（例如越界访问、空指针和野指针解引用、以及使用未初始化内存）的实际价值，并将剩余的障碍框定为形式化方法领域的开放挑战。