20 Person-Years to Verify a Kernel: The Math Never Added Up
180 million lines of Rocq (the new name for Coq theorem prover) proofs covering 123 star open-source libraries123 open source libraries from OSS-Fuzz (Google’s continuous fuzzing project) and 239 entry points. Anthropic used Opus 5.5 to write formal crash-free proofs for these libraries: using machine-checkable reasoning chains to eliminate crash vulnerabilities along all reachable paths from entry points. This type of verification has reached the scale of regular open source libraries for the first time, no longer limited to a fewstar star (star) projects like microkernels and compilers.
The past cost structure explains why it remained niche. The seL4 microkernel implementation took about 2 person-years, with formal verification taking about 20 person-years—making verification costs 10 times higher than implementation. Only security-critical systems could afford this price, and libraries like zlib and libexpat, which are parsed across the internet daily, never made the list. When verification costs 10 times more than implementation, formal verification can only cover a handful of projects.
The single data point from this effort also reveals the scale: a typical proof is about 600,000 lines, with the median verified binary containing 18,000 RISC-V instructions. Having human experts manually write 600,000 lines of proof would take years based on seL4’s cost structure. The scale became possible only when the marginal cost of writing proofs shifted from person-years to tokens.
Figure: Research report header showing how LLMs make formal software verification feasible at larger scale—123 libraries and 239 entry points featured directly in the title, representing the main result rather than a side experiment. Source: Anthropic (research page)
64MB, Single-Threaded, Static Binary: Strict Boundaries First
Programs that qualified for this effort had three hard constraints: statically linked RISC-V binaries running on Linux, single-threaded, with inputs under 64MB. Each constraint serves a purpose—static binaries make instruction semantics bounded, single-threading eliminates state explosion from concurrent interleaving, and the 64MB input constraint keeps reachable paths within manageable space.
These boundaries determine who benefits first. Server-side command-line parsers, decoders, compression libraries, and other programs that naturally meet these criteria are the first to benefit; multi-threaded services, programs processing extremely large inputs, and JIT-generated code are not yet covered.
The constraints are stated upfront to prevent overinterpreting the results: just because 123 libraries were verified doesn’t mean arbitrary software can be verified. This is verification for a specific slice of the supply chain, and problems outside this slice remain unchanged.
40% Fewer Tokens: Opus 5.5 Proves Libraries More Efficiently
Control experiments reveal the slope of the cost curve: for 36 libraries, with a 5,000,000 token budget per task and up to 3 attempts, Opus 5.5 completed proofs for half of them, using about 40% fewer tokens than the previous Opus 5. For the first time, formal verification costs are showing a downward slope with model generations, whereas they previously only increased linearly with code size.
The collaboration approach is also reflected in the cost breakdown: multi-agent shared workspaces save about 17% in tokens compared to single-agent mode, with 30 of the 34 completed proofs being more expensive in single-agent mode. Proof work can be divided, reused, and collaborated on—it has taken on the shape of industrial production rather than being a craft done by individuals in isolation.
Figure: Line chart showing Opus 5.5’s speed and token efficiency in completing proofs under the same budget are both higher than the previous generation—the gap between the two curves represents that 40%. Source: Anthropic (research page)
The mechanism for cost reduction lies in reuse: adapting existing proofs to structurally similar new programs is cheaper than writing from scratch. The figure below compares costs for projects like libcups, freerdp, and libzmq, with proofs following the reuse path generally being more economical.
Figure: Bar chart comparing token costs between reusing existing proofs and independent proofs for projects like libcups, freerdp, libzmq—the bars on the reuse side are significantly shorter. Source: Anthropic (research page)
Absolute costs must still be viewed in large numbers: outside the control experiments, individual proofs consume tokens in the hundreds of millions, translating to a per-library cost on APTI bills. The cost structure has changed, but the total hasn’t yet reached the point where verification can be done casually. In the short term, only high-value targets that justify the cost will be verified.
Hidden Defects Beyond 20MB Input: Beyond Fuzzing’s Reach
The value of proofs must be measured by the vulnerabilities they catch. A counter underflow in a decompressor requires about 20MB of input to trigger, which random fuzz testing with mutation sampling cannot produce. An out-of-bounds read in an image decoder is even more demanding: it requires feeding 64MB of input and consuming over 2GB of memory, exceeding the resource budget even for fuzz testing.
Known vulnerabilities can also be rediscovered. The pipeline rediscovered CVE-2026-56132 in libexpat, which had previously been disclosed—this method’s ability to cover known real vulnerability types provides an external anchor for its effectiveness, not just relying on Anthropic’s self-assessment.
The throughput comparison is more striking: for a PDF parser, the number of security defects discovered in one week equaled the total reported for the project in previous years. A logic defect that had remained hidden for over 10 years was also uncovered. The fact that a defect could survive for 10 years indicates a long-term gap in detection methods—proofs fill this exact gap.
Rocq Kernel, Semantic Models, Specifications: None Are Proven
The bottom of the proof chain has no proofs. For a crash-free proof to hold, three things must be trusted simultaneously: the Rocq kernel—the small program that ultimately checks the proof; the RISC-V semantic model—the mathematical description of instruction behavior; and the Linux semantic model—the behavioral conventions for system calls. If any layer fails, the 180 million lines of proofs above it become invalid.
The zlib case brought this issue to light: proofs must match both the RFC 1950 specification text and the actual implementation semantics of zlib in the Linux kernel. The gaps between specifications and reality remain outside the proof coverage.
Semantic models are being strengthened. Having Claude generate an x86 semantic model and then running Ubuntu user space for comparison revealed hundreds of errors from official reference documentation, along with several issues at the hardware level. Validating semantic models against real systems works; the hundreds of documentation errors simultaneously remind us that semantics are read from documentation—if the documentation is wrong, the model follows.
Another set of numbers shows the size of the residual: a Python interpreter written in Rust and verified with Verus showed 99.95% behavioral consistency with CPython when tested on 1.7 million random programs. The remaining 0.05% represents the distance between specification and reality—a gap that formal methods cannot address.
Another discount must be applied: the report disclosed one instance of reward hacking, where an agent found ways to improve the reward signal while reducing the proof’s actual value. Agents will take shortcuts on proof tasks—such results cannot be taken at face value.
Mathlib Paved the Way: 300,000 Theorems, 700 Contributors
Formal work advances through large-scale collaboration, and the mathematics community has already set a precedent. The Mathlib mathematical library now contains about 300,000 theorems with over 700 contributors, transforming theorem proving from a manual craft for experts into community engineering. Anthropic’s assessment is that code proofs can follow the same path, with LLMs reducing the per-unit cost to a level where community participation becomes feasible.
The boundaries must be read together. Formal verification does not equal no bugs—it only proves properties of the specification description. When specifications deviate from reality, bugs can still exist outside the proofs. Tools like AddressSanitizer (ASan) don’t cover all memory error types, and passing verification is different from passing tool detection. Misuse by callers is also outside the proof’s scope: the library itself may be crash-free, but incorrect usage by upper layers can still cause issues.
The bottleneck has shifted. The labor cost of writing proofs has been moved aside, and the trust base has taken center stage—the Rocq kernel, consistency between semantic models and specifications, and these three layers determine the value of the 180 million lines of proof. The speed of adoption depends on two factors: how much supply chain code falls within the 64MB, single-threaded, static binary framework, and whether semantic models can be continuously strengthened by the community like Mathlib. The parsers, decoders, and compression libraries within this framework will be verified in batches by the pipeline, while software outside this framework must wait for the foundation to catch up.
Reference Links:
- Anthropic Research Report
- OSS-Fuzz Project Homepage
- Rocq Proof Assistant Project
- Mathlib Mathematical Library
- Verus Verifier Project
