On October 22, 2026, Anthropic's Frontier Red Team published "LLMs are making formal software verification feasible at a much larger scale", written with the verification startup Theorem. Its opening claim sets the motivation: "Most software is riddled with bugs, which AI can now easily find and exploit." The proposed answer is not more scanning but proofs.
What was proved
The team started from Google's OSS-Fuzz, where maintainers write fuzz entry points and any crash counts as a bug. It compiled each library and its fuzz test to a RISC-V executable, then combined that binary with Theorem's formal semantics for RISC-V and Linux processes to generate a specification: the fuzz test never crashes, for any input under 64 MB. Claude wrote the proofs and the Rocq kernel checked them. According to the post, "Over the span of a few weeks", Claude patched the bugs it found and proved that 239 entry points across 123 libraries never crash on any input up to 64 MB. The proofs total about 180 million lines of Rocq. A typical proof runs to about 600,000 lines, covering binaries with a median of 18,000 RISC-V instructions. Because AddressSanitizer is compiled in, "no crash" also rules out the memory errors it detects.
Nobody reviews 180 million lines by hand. The post says the only artifacts to trust are the RISC-V and Linux models, the exact theorem statements and the Rocq checker, plus, in a footnote, the hardware, OS and OCaml compiler Rocq runs on. The proofs assume a single-threaded static binary linked against musl, with a fixed memory budget, on RISC-V. Most deployments are x86 or ARM with glibc and dynamic linking.
Bugs found on the way
Failed proof attempts point at bugs, and the team let Claude fix them. Examples include a counter underflow in a decompressor that caused an out-of-bounds write only on inputs of around 20 MB with one rare layout, an image-decoder read that needed a 64 MB input and over 2 GB of memory, and a rediscovery of CVE-2026-56132 in libexpat. Fuzzers, which typically cap inputs at about 1 MB, would be unlikely to reach these. Letting the model patch code invites reward hacking, since a program rewritten to do nothing never crashes. The team says it penalized patches, gave extra credit for proving how few inputs a patch changed, and audited the patches.
Other experiments went further. Claude wrote a formal spec of RFC 1950 and proved that the Linux kernel's zlib binary implements it, using x86 semantics that Claude itself generated. A Python-subset interpreter in Rust was verified with Verus and matched CPython on 99.95% of 1.7 million random programs. 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."
Cost and reuse
The limitation the authors stress is cost: proofs "can take hundreds of millions of tokens to produce." On 36 small tasks built from OSS-Fuzz code, they report that Opus 5.5 proves half of them with about 40% fewer tokens than Opus 5. Letting agents copy each other's proofs from a shared workspace cut tokens by 17%. At OSS-Fuzz scale, the authors add, most of each proof covers C runtime and AddressSanitizer start-up code that every program shares, so teams copied and adapted each other's proofs. The release is a subset: the theorem-labs/oss-verify-proofs repository, created on October 22, holds complete proofs for fuzz tests that did not need patching, plus specifications for targets the team could not prove. Proofs that could reveal unpatched bugs are withheld. Theorem's OSS Verify programme offers the pipeline free to qualifying projects, with one caveat maintainers should read: "Findings and patches are generated by AI models, and we don't promise that a person reviews them before we send them."
What remains uncertain. All results come from the two collaborators, and no independent group has yet checked the trusted components. The authors themselves write: "Formally verified" does not mean "bug-free." ASan does not catch every memory-safety bug, not every entry point was covered, and on the x86 semantics they write that they "can not be sure our semantics themselves are perfect".
Analysis: The useful idea is that a fuzz harness is already a specification, so maintainers do not have to write a spec from scratch. For a security lead, a proof replaces the question of whether testing was sufficient with the question of whether the model of the machine is right, which is a smaller and more reviewable surface. The bottleneck shifts to two places: porting builds to static RISC-V, and absorbing AI-written patches that nobody has reviewed. The PHP Foundation's recent count of more than 100 invalid or duplicate reports suggests that triage, not proof generation, is where the strain will show next.
Anthropic and Theorem (October 22) report that Claude produced Rocq proofs, about 180 million lines in total, that 239 OSS-Fuzz entry points in 123 libraries never crash on any input under 64 MB when compiled as static RISC-V binaries, finding and patching bugs fuzzers would likely miss; the guarantee rests on the RISC-V and Linux models, the theorem statements and Rocq, costs hundreds of millions of tokens, and has not yet been independently checked.