LLMs are making formal software verification feasible at a much larger scale
A · Strong evidence Anthropic's Frontier Red Team, with Theorem, reports machine-checked proofs over compiled binaries at a new scale and publishes a subset of proofs and trusted components for checking; held below S because it is a lab self-report with costs undisclosed and only part of the proofs released.
Summary based on the full text·Original: about 18 minutes to read
In short
A 22 October 2026 post by Anthropic's Frontier Red Team (authors include Nicholas Carlini and Nickolai Zeldovich) with the firm Theorem. Over a few weeks Claude turned existing fuzz tests into formal specifications and proved, at the level of compiled RISC-V binaries, that 239 entry points in 123 OSS-Fuzz libraries never crash for any input under 64 MB, patching the bugs it found along the way. The Rocq proof checker verifies the proofs, so humans need to trust only the machine and OS models, the theorem statements and the checker.
Key numbers
- 239OSS-Fuzz entry points proved never to crash for inputs under 64 MB
- 123open-source libraries covered by those proofs
- about 180 million lines of Rocqtotal proof size, typically about 600,000 lines per proof
- 17%fewer tokens needed when agents could copy each other's proofs in a shared workspace
- about 40%fewer tokens for Opus 5.5 than Opus 5 to prove half of 36 small verification tasks
As reported by the source.
English·Web page·opens anthropic.com
What it reports
- Approach: compile library plus fuzz test to RISC-V; combine with Theorem's RISC-V and Linux process semantics and a no-crash property to yield a spec; Claude writes the proof; Rocq checks it.
- Scale: about 180 million lines of Rocq, a typical proof about 600,000 lines, binaries with a median 18,000 RISC-V instructions.
- Bugs found that fuzzers were unlikely to reach: a counter underflow causing an out-of-bounds write on about 20 MB inputs with a rare layout; an out-of-bounds read needing a 64 MB input and over 2 GB of memory; a rediscovery of CVE-2026-56132 in libexpat; a non-crashing logic bug where a file-loading restriction was not always enforced.
- Other studies: Linux kernel zlib proved to implement a Claude-written spec of RFC 1950 at the x86 binary level; a Rust Python interpreter proved against CPython semantics matched CPython on 99.95% of over 1.7 million random programs; a PDF reader effort found as many security bugs in a week as are typically reported in a year.
- Cost trend: proofs can take hundreds of millions of tokens; Opus 5.5 proves half of 36 tasks with about 40% fewer tokens than Opus 5; shared workspaces cut tokens 17%.
- Reward-hacking guard: patches were penalised and audited so Claude could not make proofs trivial by rewriting programs.
- Released: trusted components, complete proofs for fuzz tests that needed no patching, and specs for those not proved. Theorem offers to run the pipeline for other projects.
How they got it
Autonomous agent runs on hundreds of OSS-Fuzz projects, with proofs checked mechanically. Context comparison: seL4 took two person-years to build and 20 person-years to verify.
Limits
- Proofs assume single-threaded static RISC-V binaries linked against musl libc; most deployments use x86 or ARM with glibc.
- AddressSanitizer does not catch all memory-safety bugs; not all entry points per library were verified; caller misuse is out of scope.
- Total compute and money cost are not disclosed beyond "hundreds of millions of tokens".
- Lab self-report promoting its own models; proofs that might reveal unpatched bugs are withheld.
Why it matters for companies
If the cost curve holds, proof that a dependency cannot crash on a defined input class becomes something a security team can buy or commission, not only a research artefact. For companies that consume open source, the practical near-term value is the bug yield: attempting proofs found flaws that years of fuzzing missed. Procurement and security teams should start asking which critical dependencies have machine-checked guarantees, and under what assumptions, since "verified" holds only for the modelled machine.
Summary based on the full text. Read the original for the full argument and data.Read the original on anthropic.com