Anthropic’s Frontier Red Team and the startup Theorem say they used Claude to produce roughly 180 million lines of machine-checked proof code about 123 open-source libraries, in a few weeks. According to The Decoder’s report on the work, the effort surfaced hundreds of bugs that conventional testing had missed. It matters because formal verification, long limited to a handful of safety-critical systems, may be getting cheap enough to apply broadly, though the proofs come with tight limits.
What was done
Rather than writing new software, Claude verified existing programs. As described by The Decoder, the model took test programs from Google’s OSS-Fuzz security project, translated crash tests into mathematical statements, analyzed the compiled machine code and generated proofs. The Rocq proof assistant then checks the proofs automatically, so a wrong proof is rejected whatever Claude believes. Anthropic calls the process fully autonomous, while noting that the tools and formal foundations were built by humans at Theorem.
Scale is the headline contrast. The Decoder notes that verifying the small seL4 operating-system kernel took specialists about 20 person-years, which is why the technique was reserved for cases like avionics.
Bugs found
During proof attempts Claude hit hundreds of bugs and was allowed to fix them. Many appear only under narrow conditions such as very large input files or specific access sequences, the researchers say. On a widely used PDF reader the team reportedly found as many security bugs in a week as the software typically has reported in a year, and in another application a logic error that had gone undetected for over a decade. Anthropic’s point is that even a failed proof is useful because the attempt exposes real flaws. These figures come from Anthropic and Theorem; we have not seen an independent review.
The limits
“Formally verified” does not mean “error-free.” Per The Decoder, the proofs hold only for a specific processor architecture, for single-threaded programs and for inputs under 64 MB, while real deployments differ. Compute is heavy: individual proofs consumed hundreds of millions of tokens, and Anthropic has not reported total project cost. Efficiency is improving, the report says: Opus 5.5 solves half of the proofs with about 40% fewer tokens than Opus 5.
Where Theorem says this is heading
In a September post, Theorem argues that model performance on software verification doubled every two months between May and September, and sketches verifying the Nix package ecosystem, including glibc, OpenSSL and curl. It estimates that 95% of the machine code in that ecosystem could be verified for about $134 million by the end of 2027, if models improve at verification much faster than they do overall. That is a projection with explicit conditions, not a result. Theorem’s approach works at the binary level, so bugs found are bugs in the code that actually runs.
Why it matters
AI-written code is a growing share of what ships, and review is a bottleneck. Proofs that a machine checks could shift trust from reading code to checking guarantees about it, on narrow properties such as memory safety. Our explainer on AI coding assistants covers how these tools are used today, and our guide to least-privilege API keys for coding agents shows the access controls that still matter whatever the proofs say.
What to watch next
- Publication of Anthropic’s full methods and the list of fixed bugs.
- Whether maintainers of the 123 libraries adopt the proofs and patches.
- Verification extended to multithreaded code and other processor architectures.
- Total compute cost disclosures.
- Theorem’s progress toward glibc, OpenSSL and curl.
Key takeaways
- About 180 million lines of proof code were generated for 123 libraries in a few weeks, per Anthropic.
- The Rocq proof checker validates every proof independently of the model.
- Hundreds of previously missed bugs were found along the way.
- Proofs cover limited conditions: one architecture, single-threaded code, inputs under 64 MB.
- Costs are high and the full project bill is undisclosed.
Frequently asked questions
What is formal verification?
Using mathematical proofs, checked by software, to show a program behaves according to a precise specification under stated conditions.
Does this mean the libraries are bug-free?
No. The proofs hold only under the conditions listed, and the specifications cover certain properties, not everything.
Who did the work?
Anthropic’s Frontier Red Team with Theorem, which built the tools and formal foundations.
