Claude Formally Verifies 123 Open-Source Libraries at the Binary Level

Formal verification means writing a mathematical proof that a program always obeys some rule, rather than testing it on many inputs and hoping. It has been too expensive for most software: Anthropic notes that the seL4 kernel took two person-years to build and 20 to verify. In this Frontier Red Team write-up, done with the company Theorem, Anthropic reports that Claude proved, over a few weeks, that 239 test entry points across 123 open-source libraries in Google's OSS-Fuzz project never crash on any input smaller than 64 MB.

The trick was to avoid writing new specifications by hand. OSS-Fuzz projects already ship fuzz tests, small entry points that crash when something goes wrong, and the C and C++ code is built with AddressSanitizer, which turns improper memory access into a crash. Anthropic converted the rule that a fuzz test never crashes into a theorem about the compiled RISC-V machine code, using Theorem's models of RISC-V instructions and Linux processes, and Claude wrote the proofs in the Rocq proof assistant. Because many fuzz tests assert things like compress-then-decompress returning the original data, proving no crash can also prove that behavior. The output is huge, about 180 million lines of Rocq with a typical proof around 600,000 lines, but Anthropic says almost none of it needs human review, because the Rocq checker confirms each proof mechanically. What a reader must trust is the RISC-V and Linux models, the exact theorem statements and the checker itself.

Getting there was also a bug hunt. When a proof failed, Claude patched the code and proved the patched version; Anthropic says this surfaced hundreds of bugs, including an out-of-bounds write that only appeared on inputs of about 20 MB with one rare layout, far beyond the roughly 1 MB inputs fuzzers usually try. Because letting the model patch code invites it to make the problem trivially provable, Anthropic says it penalized patches and audited them for that kind of shortcut.

The article is explicit that formally verified does not mean bug-free. The proofs cover single-threaded, static RISC-V binaries linked against musl, while most people run these libraries on x86 or ARM with glibc; AddressSanitizer misses some memory bugs; and not every entry point, let alone every function in each library, was proved. Cost is the other open question, since proofs can take hundreds of millions of tokens. Anthropic reports early signs that this falls: on a set of 36 small tasks, Opus 5.5 proved half of them with about 40% fewer tokens than Opus 5, and agents that could copy each other's proofs needed 17% fewer tokens than agents working alone. It is publishing the new trusted models, the complete proofs for fuzz tests that needed no patching, and the specifications for tests it could not prove, so others can check the work.