필사 모드: The Rust Standard Library Verification Campaign Found Zero Memory-Safety Bugs

• Introduction — The Results of a Verification Campaign Billed as the Largest Ever
• What the Campaign Set Out to Verify
• The Campaign's Structure — An Open Contest With Bounties
• The Numbers — How Far It Got Across 33,955 Functions
• What It Actually Found — Four Lines in Table 2
• How to Read the Null Result
• The Control Group — Same Tool, Different Codebases
  • try_fit — What 16.77 Million Fuzz Runs Couldn't Clear, in 20 Seconds
  • What Testing Can't See in Principle — Firecracker
  • Cedar — What Even a Formal Reference Model Didn't Catch
• The Door Contracts Opened — And the Test That Was Affirming a Bug
• When an LLM Writes the Spec — What Was Measured
• The Honest Limits — What These Proofs Don't Guarantee
• The Costs
• So When Should You Use It, and When Shouldn't You
• Closing
• References

Introduction — The Results of a Verification Campaign Billed as the Largest Ever

Formal-verification stories usually end the same way: "And so we found a critical bug nobody else had caught." Which makes the title and opening sentence of this paper's Section 4.4 feel unfamiliar.

The verification effort has not uncovered any previously unknown memory safety vulnerabilities in the standard library.

That's the sentence from Verifying the Rust Standard Library, posted to arXiv on June 16, 2026 and published at NASA Formal Methods Symposium 2026. The author list mixes AWS's Byron Cook with people from the Rust Foundation, UCL, KU Leuven, UCSD, Queen Mary University of London, and MIT. In the authors' own words, this is "the largest verification campaign reported for a software library" (their own self-assessment) — and its conclusion is "no newly discovered memory-safety vulnerabilities."

This isn't a failure story. It isn't a success story either. It's data that's far more useful than a press release for understanding what value formal verification actually delivers in practice. This post tries to read those numbers straight.

What the Campaign Set Out to Verify

Rust's ownership type system blocks data races and a large share of memory errors at compile time. The problem is that the standard library itself leans heavily on unsafe code. The soundness of the five operations the compiler doesn't check — raw pointer dereference, calling unsafe functions, mutable static access, unsafe trait implementation, union field access — ultimately rests on the developer's reasoning, and that reasoning is usually recorded only in natural-language SAFETY comments.

The paper's sense of scale: over the past three years, more than 74 soundness bugs have been reported under the I-unsound label, and historically 18 CVEs have been registered (both figures as of March 2026). With Rust now inside kernels, browser engines, and crypto libraries, the campaign's motivation is to back this foundation with machine-checked proofs.

One term needs pinning down here. What this campaign targets is the absence of undefined behavior (UB), not full correctness. Absence of UB is a sufficient condition for memory safety, but it does not guarantee functional correctness, liveness, or security properties.

The Campaign's Structure — An Open Contest With Bounties

The standard library is too large for one team to verify. So it was designed as an open contest run by the Rust Foundation.

The verification work is broken into units called challenges. Each challenge defines a concrete verification target, a list of assumptions, explicit success criteria, and a bounty paid on completion. Participants fork the repo and submit PRs, a technical review committee reviews them, and approved PRs get merged into the model-checking/verify-rust-std fork. As of the paper's cutoff (March 2026), 29 challenges had been published, drawing more than 450 PRs from 21+ external contributors across at least 4 institutions.

That figure checks out directly against the repo — doc/src/challenges/ holds exactly 29 files, from 0001-core-transmutation.md to 0029-boxed.md, and the repository is still active.

The contest is tool-agnostic. Any tool is accepted as long as it runs on the Rust standard library, integrates into CI, and provides a clear soundness guarantee (usually backed by a peer-reviewed paper). Four tools are currently supported.

• Kani — CBMC-based bounded model checking. The campaign's workhorse.
• ESBMC — also model checking.
• Flux — checks numeric ranges and safety preconditions via refinement types.
• VeriFast — separation logic. For the functions it covers, verifies the absence of all UB, including pointer-aliasing violations.

Verus, Creusot, KRust, and RAPx are under review. The paper's point is that this diversity isn't a matter of taste but a necessity — architecture-specific intrinsics, pointer-heavy code, concurrency primitives, and loops with complex invariants each demand a different reasoning technique. No single tool can digest every verification condition.

The Numbers — How Far It Got Across 33,955 Functions

As of the nightly-2025-10-08 toolchain snapshot, the three crates core, alloc, and std together contain 33,955 functions.

The first 16 months were hand-written proofs: 725 Kani harnesses (694 of them with function contracts), 50+ VeriFast proofs. Then around October 2025 the growth rate of new contracts flattens out. The paper's diagnosis is unsentimental — manual proof engineering alone hits a fundamental scalability wall; it can't reach tens of thousands of functions.

So they built Autoharness: a compiler pass inside Kani that enumerates every function in a crate, judges its eligibility, and synthesizes at the MIR level a proof harness that calls each qualifying function with fully non-deterministic inputs. It never touches the source — which is why it can live in CI.

A harness resembles a unit test, but instead of a concrete input it calls the function with a symbolic value standing in for every possible input at once. Once the model checker exhaustively explores every reachable execution path, it stops being a test and becomes a formal-verification problem.

Total functions               33,955
├─ Autoharness harnesses      16,748
│   ├─ Verified                11,970
│   └─ Failed                   4,778   (missing model / timeout / unsupported)
└─ Skipped                     17,207
    ├─ Generic type params      9,635  (56%)
    ├─ No Arbitrary impl        3,826  (22%)
    ├─ Kani-internal functions  3,246  (19%)
    └─ Other                      500  (3%)

Breaking the 11,970 passing functions down by category:

A caveat the paper attaches to itself matters here: not all 11,970 passing results carry the same evidentiary weight.

Add the 694 hand-written contract proofs and the number of functions verified against a formal function contract comes to 989 (295 automatic + 694 manual) — the strongest guarantee the campaign provides. That's 989 out of 33,955, roughly 2.9%.

At the opposite end sit 622 unsafe functions that passed without a contract. The paper's reading: either (a) these functions are trivially safe with respect to the UB classes Kani checks, and their unsafe marking exists for a property — like aliasing — that Kani doesn't yet check, or (b) Kani's UB coverage is simply incomplete for what that function actually does. Telling the two apart requires a human. The paper calls these 622 not proofs, but "candidates surfaced by automated triage."

The middle is the sturdiest. The 10,194 passing safe functions (85% of what Autoharness passed) carry no ambiguity — Kani symbolically executes every callee, including transitively-reached unsafe code, and confirms that no path triggers UB for any bit-valid input.

What It Actually Found — Four Lines in Table 2

So here is the entire set of issues this whole effort turned up — Table 2.

Four lines. And three of them are not code bugs but problems with specifications and documentation — a missing safety annotation, a wrong SAFETY comment, documentation that misdescribed a function's behavior.

The paper honestly frames this as a side benefit: the act of writing a formal specification itself forces a precise expression of safety requirements that natural-language comments alone never produce. This effect actually left a mark on the Rust language itself — the language team adopted contracts as an experimental language feature, and the Rust project adopted attaching safety contracts to the standard library as an official goal.

But there's a twist on the one line that is an actual code bug — "Incorrect SIMD shift result." Section 7 of the paper says so directly: Challenge 15 was completed via random testing of an executable model for 565 SIMD intrinsics, not via formal proof. Seeds were logged for reproducibility and it turned up two upstream bugs, but in the authors' own words this should be read as "validation with high confidence, not formal verification."

To sum it up: the code bug that the largest verification campaign ever run against the standard library actually found — random testing found it, not formal verification.

How to Read the Null Result

Start with the paper's own interpretation.

This null result is itself informative: it speaks to the effectiveness of Rust's existing testing infrastructure and Miri-based dynamic analysis at catching memory safety bugs before they reach production.

In other words, read it not as "formal verification is useless" but as a signal that "the Rust standard library's existing tests are already exceptionally good." Miri has already found dozens of bugs in the standard library and is integrated into CI. There simply wasn't much left to find.

And it redefines the campaign's value.

Testing can demonstrate the absence of bugs on exercised inputs; verification certifies their absence on all inputs within scope.

Testing can demonstrate the absence of bugs for the inputs it exercised; verification proves absence for every input in scope. So the campaign's real output isn't a bug list — it's a set of machine-checked proofs that live in CI. On every PR, the full tool suite runs across every active proof, and any violation is caught immediately. It's a regression backstop.

That claim is honest, but read coldly it also means this: this campaign's ROI is in the future. It didn't find bugs that were already there — it aims to stop bugs that haven't arrived yet, and that value hasn't been measured yet.

The Control Group — Same Tool, Different Codebases

If the story stopped here, the takeaway would be "formal verification isn't much use on well-tested code." But two weeks later, on July 1, 2026, much of the same team posted Kani: A Model Checker for Rust (still a preprint). Table 2 of that paper is exactly the control group.

Kani found 11 bugs across four production Rust codebases that testing and fuzzing had missed.

Same tool, opposite result. The difference isn't the tool — it's the existing test maturity of the target code.

try_fit — What 16.77 Million Fuzz Runs Couldn't Clear, in 20 Seconds

This is the most striking case. s2n-quic is Amazon's implementation of IETF QUIC, and the try_fit function decides how many bytes of data to pack into a QUIC Stream frame given the packet's remaining capacity. It's a subtle calculation, because the frame length's variable-length integer encoding grows right at capacity boundaries.

s2n-quic uses the Bolero property-testing framework. A single #[cfg_attr(kani, kani::proof)] attribute lets the same harness run both as a fuzz test and as a Kani proof. That makes the following comparison possible: a differential Bolero harness comparing the implementation against a reference model ran under libfuzzer for over 10 minutes — 16,777,216 executions — and found no failure. Kani found a failing assertion in 20 seconds.

The failure sat near the boundary between the 1-byte and 2-byte encodings. The paper's diagnosis is the crux of it — this is a sparse input space that coverage-guided fuzzing has no gradient pointing toward, while Kani's symbolic execution goes straight there.

The second s2n-quic case shows the opposite side of complementarity. The decode_packet_number bug was found independently by Kani in 2.8 seconds and by fuzzing within a minute. Even when both find it, Kani gives more actionable information — it points to the failure of a named property rather than an unidentified crash, and its concrete-playback feature generates a concrete counterexample the developer can replay as an ordinary Rust test.

What Testing Can't See in Principle — Firecracker

Firecracker is the VMM behind AWS Lambda and Fargate. It uses Kani on two security-critical components.

The I/O rate limiter is a token bucket. The property of interest is that "a microVM cannot exceed its configured I/O bandwidth in any given one-second window." But this is inherently time-dependent — the number of tokens replenished depends on exactly when auto_replenish is called relative to the system clock, which makes exhaustive testing impossible.

Kani's solution is to swap libc::clock_gettime for a non-deterministic stub that returns a monotonically non-decreasing Instant — turning the time dimension itself into a symbolic variable. The resulting harness found several bugs in the rate limiter, the most important being a rounding error that let a guest, under adversarially-timed calls, exceed its I/O budget by up to 0.01%.

One thing needs saying honestly: 0.01% is, in practical terms, a tiny overage. Dressing it up as a "critical vulnerability" would be a lie. What's interesting isn't the magnitude but the kind — this error depends on exactly when, at sub-millisecond resolution against the system clock, a replenish call fires, a condition testing cannot deterministically control and fuzzing can't target either without an explicit time model.

The second component is VirtIO device emulation. Memory shared between host and guest is an adversarial attack surface — an untrusted guest can write arbitrary values into shared descriptors and ring buffers. Kani modeled this scenario with non-deterministic guest memory to verify compliance with VirtIO spec Section 2.6.7.2, and additionally found a bug where a guest could place a VirtIO queue component's start address in the MMIO gap and panic Firecracker during boot.

Cedar — What Even a Formal Reference Model Didn't Catch

Cedar is an open-source authorization policy language and engine. What makes this case special is that Cedar was already running differential testing against a formal reference model — and the bug still survived into production code.

contains_at_least_two checks whether a specific substring occurs at least twice in a string. Passing a multi-byte character as the search term could slice an &str at a non-character boundary, causing a runtime panic. Every existing test stayed silent. Kani's symbolic execution produced a counterexample, and the fix was merged as cedar PR 1037 (July 2024).

Note the date. The Kani paper is from 2026, but the individual cases span different years — the Cedar fix is from 2024. The paper is reporting these cases together in 2026; it doesn't mean all 11 bugs were found in 2026.

The Door Contracts Opened — And the Test That Was Affirming a Bug

Hifitime is a high-precision time-management library used on Firefly's Blue Ghost Mission 1 lunar landing mission. This is the Kani paper's contract case study.

Kani contracts write function preconditions, postconditions, and loop invariants as Rust boolean expressions. Why this matters: it lifts bounded model checking to an unbounded guarantee — instead of exhaustively unrolling a loop, it verifies that the invariant is inductive and uses that to abstract the loop away. In the paper's terms, stage 1 proves an operation doesn't crash, and stage 2 proves the operation computes correctly.

As a side effect of establishing functional properties, Kani found 6 previously unknown bugs — properties a mere panic-freedom harness couldn't even express. The two most significant ones violated the Rust standard library's own requirements.

• Epoch's PartialEq/Ord mismatch. Duration::PartialEq deliberately treats values of opposite sign as equal (since it represents an interval length independent of direction). But while Epoch::PartialEq delegated to this implementation, Epoch::Ord used a sign-distinguishing lexicographic comparison. The Rust standard library requires that if a == b, then a.cmp(b) must be Ordering::Equal. This invariant was broken for every pair of epochs with opposite signs.
• Duration's PartialEq/Ord mismatch (zero-crossing). Same root cause. Two Durations could satisfy a == b and a < b simultaneously.

Why the Epoch bug slipped past testing compresses this whole post's point into one sentence — no test ever compared an epoch against its sign-flipped counterpart, because it's a conceptually strange operation to perform on a "point in time." Kani's symbolic execution, exploring every possible pair of Epochs, generated this input automatically.

And the most painful detail. When a contract caught a sign error in total_nanoseconds() (using subtraction instead of addition for periods exceeding a century in the negative direction), the fix was a single character in the source. But one existing integration test was asserting that buggy behavior as correct, and it had to be fixed along with the implementation. The paper's diagnosis is sharp — because the test oracle had been written by looking at the implementation's output, it encoded the same error right along with it. The postcondition, by contrast, was derived from the Duration type's encoding invariant, which let it check the implementation and the test independently of each other.

This trap checks out outside the paper too. Issue 475 in the Hifitime repo is an error-classification bug in try_truncated_nanoseconds found during Kani verification work (PR 474, merged April 2026), and the issue body reads: "updated the Kani harness to match the current (incorrect) behavior so the proof would pass; the actual implementation still needs a separate fix." Fit the spec to the implementation, and verification passes while the bug stays. Even with a verification tool in hand, where the human gets the spec from is still everything.

When an LLM Writes the Spec — What Was Measured

Hifitime's stage-2 spec was developed with an AI coding assistant that had shell access. The workflow was a tight loop — the assistant proposed a contract annotation, wrote it into the source, ran cargo kani, observed the result (success/failure/timeout/compile error), and refined the spec. The human researcher directed which functions to target, supplied domain context, and reviewed the plausibility of the proposed contracts.

The fact that Kani's specification language is an extension of Rust works in its favor here. Because contracts are Rust boolean expressions and harnesses are Rust functions, the assistant leans on its existing Rust knowledge rather than learning a separate formal language.

What the paper emphasizes is structure, not outcome.

Crucially, the specifications do not need to be trusted: Kani verifies every contract against the implementation.

The point is that the spec doesn't need to be trusted. In fact, 3 AI-generated contracts failed verification, and Kani caught all three.

1. An unmanageable postcondition that called the function under verification from within its own ensures clause — the SAT formula doubled and the solver timed out. (The assistant simplified it into a direct arithmetic expression.)
2. An overly broad symbolic input (kani::any::<Epoch>()) that pulled the TimeScale::ET variant — and with it sin() — into the SAT formula, causing a timeout. (Restricted to TimeScale::TAI.)
3. A const fn incompatibility — Kani's macro expansion generated non-const code, causing a compile error. (Switched to a standalone proof harness.)

Sorted by category: one spec-design error, one harness-design error, one Kani-native limitation. All three were diagnosed and fixed by the assistant, in the same session, from Kani's output alone.

This is a rare honest angle among LLM-proof-automation stories — the boast isn't "the AI writes good specs," it's "the verifier filters out the AI's spec mistakes." The point is that Kani caught what human review might have missed (in the paper's own words, "all caught by Kani, not human review").

Meanwhile, the LLM experiments on the standard-library-campaign side are far more cautious. They tried LLM-based contract synthesis that translates natural-language SAFETY comments into function contracts, but the paper calls this "preliminary," notes that generated contracts require manual review before merging, and leaves a systematic evaluation of precision and recall for future work. There's no citable number for this yet.

The Honest Limits — What These Proofs Don't Guarantee

Section 7 of the NFM paper is titled "Limitations and threats to validity," and it's written with a density you rarely see in formal-verification marketing copy. It's worth carrying over directly.

Bounded reasoning. Kani is, by default, bounded model checking — it unrolls loops up to a set limit. If the limit is insufficient, an unwinding assertion fails and the proof is reported as a failure, so it doesn't fail silently. But it does not verify termination, because Kani doesn't yet support loop-variant (decreases) clauses.

Partial property coverage. Kani checks only a subset of the UB the Rust reference enumerates. What it does not check is a substantial list.

• Violations of the pointer-aliasing model (Stacked Borrows / Tree Borrows)
• Data races
• Incorrect inline assembly
• Some forms of provenance-related UB
• Preservation of type-safety invariants across unsafe boundaries (e.g., that a Vec's length never exceeds its capacity)

In the paper's own words — a function that passes every current check can still exhibit UB under a more complete model.

Gaps between spec and model. Rust still has no ratified formal specification. Core pieces like the aliasing model have competing proposals, and if the spec changes down the line, proofs that were sound under today's assumptions could become invalid. Verification of functions that call intrinsics or foreign functions depends on the fidelity of the model provided for those operations, and an inaccurate model can produce an unsound verification result.

Toolchain soundness. Every result depends on the correctness of the tools themselves — Kani's MIR-to-GOTO translation, CBMC, the SAT/SMT solvers invoked, VeriFast's symbolic execution engine. The paper says it directly: none of these tools is itself formally verified. Their reliability rests on extensive testing and fuzzing, and years of production use.

Concurrency is a blank spot altogether. Of the 29 challenges, two target concurrency APIs — Challenge 7 (atomic types) and Challenge 27 (Arc). Neither has a single approved solution, even though a data race in unsafe Rust is immediate UB. The hard part is specifying and verifying lock-free data structures under a relaxed memory model.

What's left. Over ten thousand functions were verified, but the standard library is far from fully verified. Many high-impact APIs — BTreeMap internals, atomic types, String, iterators, vectors, deques, reference-counted types — have been covered only partially or not at all.

The Kani paper also acknowledges bias in its own case studies — the evaluated projects aren't a random sample but places that self-selected into adopting Kani, so favorable cases may be overrepresented. It notes that the Cedar experiment, a deliberate evaluation of a project that wasn't already using Kani, partially mitigates this.

The Costs

Proof maintenance. The verification repo is a fork of upstream rust-lang/rust and has to be synced periodically. And Rust ships a new release every six weeks. The paper's conclusion is that for this to be sustainable, contracts and proofs need to move upstream so that proof maintenance becomes part of the standard development workflow. Right now, it isn't.

Compile time. As harnesses proliferated, compilation became a bottleneck. They built a dedicated compiler-benchmarking tool and added parallelization, caching, heuristic code-generation ordering, and function stubbing, getting a 3.97x speedup on standard-library compilation (author-measured, against a naive sequential pipeline).

CI time. Per Table 1 of the Kani paper.

Most finish within 25 minutes. The paper's claim is that this is a budget you can fit into a PR workflow, and the table makes that plausible. But it also shows the harness count and the time aren't linear — rust-sel4, with 1 harness, takes 4 minutes, while zerocopy, with 10, takes 3. The difficulty of individual proofs dominates over the harness count.

Human and organizational costs. Section 5.1 of the paper is the most candid part. It admits that the initial plan focused on technical milestones and badly underestimated the time needed for community consensus and institutional coordination. Integrating contracts into the Rust compiler needed broad buy-in from the language team, library maintainers, and tool authors, and even technically simple changes stalled if stakeholders weren't brought in early. Collaborating with outside institutions required legal agreements that took months. Attracting outside contributors also took more than bounties alone — it needed a spread of difficulty levels, clear documentation, and working examples.

Per-tool overhead. PR 238, which proved LinkedList with VeriFast (Challenge 5, merged August 2025), illustrates this cost well. It directly verifies 19 functions and implies the soundness of 5 more, but VeriFast requires lightly modifying the source to insert ghost commands (e.g., turning a for loop into a loop, Option::map into its first-order equivalent). So the CI pipeline runs in three stages — VeriFast checks the annotated code, a refinement checker mechanically verifies that every behavior of the original is also a behavior of the annotated version, and a diff confirms the original matches upstream. It's a clear picture of the engineering burden deductive verification adds over model checking — and also the price of the deeper guarantee (absence of all UB) it buys.

So When Should You Use It, and When Shouldn't You

Overlay the two papers and a fairly clear decision rule emerges.

When it earns its keep

• A property exists that existing tests can't reach in principle. Time-dependent code (Firecracker's rate limiter), shared-memory boundaries facing adversarial input (VirtIO), sparse input regions like encoding boundaries (try_fit). Wherever fuzzing has no gradient is exactly where symbolic execution belongs.
• The code is narrow and the state space is well-defined. The common thread among the short-CI projects in Table 1.
• The property can be written as a spec. Where an invariant that can be derived independently of the implementation exists — Eq/Ord consistency, encode-decode round-tripping — a contract does real work. The Hifitime case shows this.
• The goal is stopping regressions. Even on already well-tested code, a machine-checked proof that lives in CI catches future regressions. This is where the standard-library campaign actually lives.
• Property testing already exists. As with s2n-quic's use of Bolero, one attribute turns the same harness into a proof. The marginal cost is close to zero.

When it's overkill or not there yet

• The code is already verified at Miri-grade rigor. The standard-library result is exactly this case. Go in expecting new bugs and you'll be disappointed.
• Generics are central to the code. 56% of the functions Autoharness skipped are generic. Because Rust monomorphizes at compile time, it can't synthesize inputs for uninstantiated type parameters.
• Concurrency is the core issue. The fact that Challenges 7 and 27 have no approved solutions tells you the current maturity level. Lock-free data structures under a relaxed memory model remain an open problem.
• Aliasing or data races are the primary risk. Kani doesn't look at these. This territory is still Miri's.
• You're about to copy the spec from the implementation. As Issue 475 and the Hifitime bug above show, a spec written by looking at the implementation encodes the implementation's bugs right along with it. Verification passes and the bug stays. Without a spec derivable independently, verification is an expensive tautology.

Boiled down to one sentence: the value of formal verification is proportional not to how powerful the tool is, but to how much territory your existing tests can't reach.

Closing

This is why these two papers need to be read together. Read only one, and you get the wrong conclusion.

Read only the NFM paper and you get: "The largest verification campaign ever found zero bugs — formal verification is overhyped." Read only the Kani paper and you get: "It found in 20 seconds what 16.77 million fuzz runs missed — why isn't everyone using this already?" Both are results from the same tool, the same team.

The real conclusion sits between them. No bugs surfaced in the standard library not because the tool is weak, but because the target had already been hardened by years of Miri and testing; bugs surfaced in s2n-quic and Hifitime not because the tool is magic, but because those codebases had corners testing couldn't reach in principle. Formal verification isn't a strict upgrade over testing — it's a differently-shaped net that complements it.

And, finally, the biggest asset this campaign leaves behind may not be the 11,970 proofs. Contracts became an experimental Rust language feature, and attaching safety contracts to the standard library became an official project goal. Things that used to exist only as natural-language SAFETY comments have started moving into a machine-readable form — this quiet shift happening behind the null result is probably the part that outlasts everything else.

References

• Verifying the Rust Standard Library (Cook et al., NASA Formal Methods Symposium 2026, arXiv 2606.17374) — the campaign's results paper. DOI 10.1007/978-3-032-28079-4_19
• Kani: A Model Checker for Rust (arXiv 2607.01504, preprint July 1, 2026) — the tool paper. Industrial-codebase case studies and 11 bugs
• model-checking/verify-rust-std — the verification repository — the 29 challenges are visible directly under doc/src/challenges/
• verify-rust-std PR 238 — VeriFast's LinkedList proof (Challenge 5)
• Kani Rust Verifier — tool repository
• cedar PR 1037 — fix for the latent bug in contains_at_least_two
• hifitime issue 475 — found during Kani verification, a case of fitting the harness to the buggy behavior
• List of undefined behavior Kani checks — for confirming what it does not check