How the Rust Standard Library Verification Contest Scaled Past Manual Proof Engineering
This article was written with support from Rahul Kumar (Senior Applied Scientist Manager, AWS) & Felipe Monteiro (Senior Applied Scientist, AWS)
When the Rust Foundation and AWS launched the verification contest for the Rust standard library back in November 2024, none of us knew exactly how far a crowdsourced, multi-tool effort could take it. The standard library is enormous – roughly 34,000 functions across core, alloc, and std – and it ships a new release every six weeks. Proving the absence of undefined behavior across a codebase like that was never going to be something any single team, company, or tool may have the resources to do alone.
With the project’s next public update coming at RustConf 2026 in Montréal this September, we wanted to share where the program stands today, drawn from the comprehensive paper my co-authors and I presented as part of Rahul Kumar’s keynote at NFM 2026.
How the contest works
The contest works by breaking verification down into discrete challenges, each with a concrete target, explicit success criteria, and a financial reward. Anyone can take one on. So far, that’s brought in more than 450 pull requests from at least 21 external contributors across four institutions. This is proof that this kind of work doesn’t have to live only inside a single company’s verification team.
The contest has also stayed tool-agnostic from the start. Four verification tools are now integrated into continuous integration (Kani, ESBMC, VeriFast, and Flux, contributed and maintained by teams at AWS, KU Leuven, and UC San Diego among others) and four more (Verus, Creusot, KRust, and RAPx) are currently under review for inclusion. No single tool can reason about everything the standard library throws at it: bounded model checking is a great fit for straightforward, non-heap-heavy code, while pointer-intensive data structures need the kind of unbounded, separation-logic reasoning that VeriFast provides.
Where manual proof engineering hit its ceiling
For the first year of the program, verification was almost entirely hand-written: contributors produced 725 manual Kani harnesses (694 of them backed by formal function contracts) plus more than 50 VeriFast proofs. That work was genuinely valuable and is what convinced the Rust language team to accept contracts as an experimental language feature, and it’s what led the Rust Project to adopt a formal goal of instrumenting the standard library with safety contracts. But the growth in manually written contracts plateaued around October 2025, covering only a small fraction of the library. Manual proof engineering, on its own, was never going to reach tens of thousands of functions.
Autoharness: an order of magnitude jump
That plateau is what motivated Autoharness, a tool the AWS Kani team built to automatically generate proof harnesses at the MIR level, no source changes required. Instead of hand-writing a harness for each function, Autoharness enumerates every eligible function in a crate and calls it with fully symbolic inputs, turning the call into a formal verification problem that Kani’s backend can exhaustively check.
The results speak for themselves. Autoharness produced 16,748 proof harnesses, including 4,645 for unsafe functions and 1,126 for safe abstractions that wrap unsafe code internally. Of those, 11,970 were successfully verified against Kani’s supported classes of undefined behavior: out-of-bounds access, null and dangling pointer dereferences, use of uninitialized memory, and arithmetic overflow in unsafe contexts. That’s an order of magnitude beyond what fifteen months of manual effort produced.
Not every one of those 11,970 carries the same weight, and the paper is careful about that rather than rounding it up. The strongest guarantees (989 functions in total, combining automatic and manual harnesses) are those verified against full formal contracts with explicit preconditions and postconditions. The remaining verified functions still provide real assurance (particularly the ~10,200 safe functions, where Kani symbolically executes through every callee including any unsafe code reached transitively), but some of the verified unsafe functions pass only because they were exercised on unconstrained, bit-valid inputs with no stated precondition — a useful triage signal, not yet a complete safety proof.
A different kind of proof: LinkedList
Alongside the model-checking numbers, the program also produced a proof that reasons differently: a VeriFast verification of LinkedList, one of the most pointer-heavy modules in the library, contributed through the contest by researchers working with VeriFast. It directly verifies 19 functions and, through them, implies the soundness of 5 more. Every operation in LinkedList manipulates raw pointers and manages heap allocation by hand, so this proof (built on separation logic rather than bounded model checking) establishes something bounded model checking alone can’t: that the verified functions won’t exhibit undefined behavior for any well-typed caller, not just the ones the harness happened to explore.
What the contest found (and what it means)
Encouragingly, the effort hasn’t turned up any previously unknown memory-safety vulnerabilities. We take that as a genuine, if quiet, endorsement of the testing and Miri-based dynamic analysis the standard library already relies on. What the program has surfaced is a set of specification and documentation issues: an incorrect SIMD shift result, missing unsafe annotations, incorrect SAFETY comments, and a documentation error in panic behavior; all now fixed upstream. Writing a formal specification, it turns out, forces a precision that a natural-language comment doesn’t always deliver.
What’s still ahead
There’s still a long way to go. Large swaths of high-impact code are only partially covered. Generic functions remain the single biggest gap: Autoharness currently has to skip over 9,600 of them because Rust monomorphizes generics at compile time, and automatic instantiation-based checking doesn’t scale well there. Concurrency is another open front. The challenges targeting atomic types and Arc haven’t yet been solved, and reasoning soundly about lock-free data structures under a relaxed memory model remains genuinely hard.
Why this matters
Rust now underpins operating system kernels, browser engines, cryptographic libraries, and safety-critical embedded systems. The standard library is the foundation nearly every one of those projects builds on. This program won’t get us to a fully verified standard library overnight, but the community it’s assembled, from AWS engineers, to academic tool authors, to the Rust Project, to independent contributors, has already produced a working model for how a library at this scale can be made more trustworthy over time, in the open.
If you want the full picture, including the complete breakdown by function category, the compilation performance work that made running thousands of proofs in CI practical, and the open technical challenges posed to the formal-methods community, Felipe Monteiro will be giving a full program update at RustConf 2026 in Montréal (September 8-11). Come join the session and say hello!
