Anthropic's Frontier Red Team published research on October 22 in which Claude wrote formal proofs for 239 entry points across 123 open-source libraries: as long as the input is smaller than 64 MB, none of these programs will crash. The proofs sit directly on compiled RISC-V executables, and the team worked with Theorem, a company that builds formal-methods tooling. Anthropic says this is the first time AI has done formal verification at scale on production software at the assembly level.
All of the libraries come from Google's OSS-Fuzz project, the long-running set of foundational components kept on that fuzzing platform. Compression, image decoding and HTTP parsing are all in the mix. The whole effort took a few weeks.
Turning fuzz tests into theorems
The approach has three steps. First, the team rewrote each library's existing fuzz test suite as a formal specification, which says that this piece of test code does not crash on any input. The specification is built on the RISC-V instruction semantics and Linux process semantics models provided by Theorem.
Second, Claude writes the proof, and the Rocq proof checker verifies it line by line.
"Claude writes the proof; the Rocq kernel checks it against the specification."
The third step handles proofs that will not go through. A stuck proof often means the code really does contain a defect. In that case Claude edits the code itself, the specification is regenerated, and the proof continues. The team acknowledges that this step invites reward hacking, where the model might alter the program arbitrarily just to make the proof pass. So they added a penalty for patches, required proofs to cover the range of inputs a patch affects, and logged every patch for human audit.
A typical proof runs about 600,000 lines. What ultimately has to be trusted comes down to the RISC-V and Linux semantics models, the theorem statements themselves and the Rocq checker.
Bugs uncovered along the way
Hundreds of bugs were found and fixed during the proof work, some of them hard to hit with fuzzing. The write-up gives several examples: a counter underflow in a decompressor that triggers only on a specific input of around 20 MB; an out-of-bounds read in an image decoder that needs 64 MB of input plus more than 2 GB of memory; and another out-of-bounds read that requires two handles to operate on the same file in a particular order. CVE-2026-56132 in libexpat was also independently rediscovered.
The cpp-httplib proof had an extra hurdle: recursion during std::set destruction could overflow the stack. To rule that out, the team proved at the machine-code level that the balancing algorithm of the libc++ red-black tree keeps tree depth logarithmic.
The same research also includes a few side experiments. Claude wrote a Python subset in Rust and used Verus to prove it conforms to CPython semantics; across 1.7 million random programs, its behavior matched CPython 99.95% of the time. It also generated its own set of x86 instruction semantics, capable of single-step execution that boots an Ubuntu userspace, and in the process turned up hundreds of errors in the official reference documentation.
Comparing with seL4
Formal verification is nothing new in industry; the hard part has always been labor. The seL4 microkernel is the usual example: roughly 10,000 lines of C, with the proof effort commonly cited as around twenty person-years. The CompCert compiler followed a similar path, polished over many years by a small team. What these projects share is few targets, long timelines and heavy reliance on experts.
Anthropic's run covered 123 libraries in a few weeks. Roughly speaking, the cost structure per unit of work has taken a different shape, with humans stepping back from writing proofs to defining specifications and reviewing patches. The cost has shifted to tokens: the write-up says a full proof can consume hundreds of millions of tokens. On the 36 small tasks, each task got a single agent three attempts with a 5-million-token budget per attempt; once agents were allowed to reuse each other's proofs, the tokens needed dropped by a further 17%.
The strength of the guarantees also differs. seL4 proved functional correctness, while this work proves only "does not crash," a much narrower scope.
The gaps beyond the proofs
The limitations Anthropic lists are quite specific. The proofs cover single-threaded, statically linked RISC-V binaries using musl libc, whereas most users actually run builds on x86 or ARM that link glibc dynamically. AddressSanitizer cannot catch every memory-safety error, some entry points are not covered, and memory corruption caused by a caller misusing a library is likewise outside the scope of the proofs.
"Formally verified" does not mean "bug-free."
The gap between the specification and the real machine is where this approach is most likely to go wrong. Rocq and the semantics models themselves also need hardening, which the write-up calls "no small task." The team's view is that formal verification will become a routine part of secure software development; as for when these proofs might reach mainstream deployment environments such as x86 and glibc, the write-up gives no timeline.
Sources: Anthropic Frontier Red Team research article, CocoLoop; Anthropic research page, used to check the library count, entry-point count, proof line count and token comparison basis.