Fuzzing has always been the workhorse of software security. Developers write an entry point, let the fuzzer hammer it with enormous numbers of semi-random inputs, and declare victory when something crashes. The catch is that the input space is infinite, so no amount of hammering can be exhaustive: fuzzing can tell you "there is a bug here," but never "there is no bug here." Formal verification can give you the second sentence, but historically at a price measured in expert-years. The seL4 microkernel took two person-years to implement and roughly twenty person-years to verify, which is why the technique stayed confined to the most safety-critical code, like Airbus avionics.

Anthropic and Theorem bent that curve. Using Claude, they produced machine-checkable formal proofs at the RISC-V assembly level for real open-source libraries. To Anthropic's knowledge, this is the first large-scale effort to apply formal verification to production software at the assembly code level (original post).

From "running tests" to "proving a proposition"

The key move was not asking the model to rewrite the code. Instead, each library's existing fuzz test was automatically converted into a specification: this test never crashes on any input. The specification is defined over compiled RISC-V instructions, built on Theorem's formal semantics for the RISC-V instruction set and for Linux processes. Claude writes the proof; the Rocq kernel checks whether that proof actually satisfies the specification.

The result is that a developer only has to trust three artifacts: the formal models of RISC-V and of Linux processes, the exact theorem statements, and the Rocq proof checker itself.

239 entry points, 180 million lines of proof

On scale: over the span of a few weeks, Claude patched the bugs it found and then proved that there are no crashes on any input up to 64 MB for 239 entry points across 123 different OSS-Fuzz libraries. Those proofs come to roughly 180 million lines of Rocq, with a typical proof running about 600,000 lines to cover binaries whose median length is 18,000 RISC-V instructions. Unite.AI, citing the technical appendix, gives an even more striking figure: Claude wrote around one billion lines of Rocq during the effort, of which about 180 million passed the proof checker. A single entry point in cJSON — a 391-line parser — received a 630,000-line proof.

The bugs that fell out along the way

More interesting than the proof count is what the process turned up. Claude found a counter underflow in a copy of a decompressor that led to an out-of-bounds write, but only on inputs of around 20 MB with one rare, specific layout. An out-of-bounds read in an image decoder needed a 64 MB input and more than 2 GB of memory. In libexpat it rediscovered CVE-2026-56132. It also caught logic bugs that never crash at all, such as a restriction on which files an application may load that is not always enforced. During an effort to verify a widely used PDF reader, the team says it found as many security bugs in one week as are typically reported in a year.

Whether the cost can hold up

The biggest weakness of formal verification is cost: producing a proof can burn hundreds of millions of tokens. Anthropic's answer has two parts. First, newer models are cheaper — they shrank real OSS-Fuzz code into 36 small verification tasks, and Opus 5.5 completed half of them using about 40% fewer tokens than Opus 5. Second, proofs are reusable: when agents were allowed to copy one another's proofs in a shared workspace, token consumption dropped 17%, and some agents succeeded at tasks they had failed at working alone. That is the same logic by which the Lean community grew Mathlib to nearly 300,000 theorems with over 700 contributors.

Where the boundaries are

Anthropic states the caveat plainly: "formally verified" does not mean "bug-free." A proof checker cannot tell you whether your specification matches reality. These proofs cover single-threaded, statically linked RISC-V binaries against musl libc, whereas most people run these libraries on x86 or ARM, dynamically linked against glibc. AddressSanitizer itself does not detect every memory-safety bug, and not every entry point in every library was verified. There is also a reward-hacking hazard: in principle Claude could rewrite a program into something that trivially never crashes. The team's countermeasure was to penalize patches, to award extra credit for proving which inputs a patch changes, and to log and audit the patches.

So what

The part worth watching is not the numbers but the division of labor. The model is no longer only tasked with finding bugs; it is tasked with upgrading "find bugs" into "prove there are no bugs," while humans hold onto three trust anchors. If this path holds, the default shape of software security shifts from "we tested a lot" to "this part has been proved."