Claude Writes 180 Million Lines of Proof for Real Code

Formal verification lets you mathematically prove that code is free of certain bugs, and it’s no longer just for aerospace budgets. In research published October 22, Anthropic’s Frontier Red Team worked with the verification startup Theorem and used Claude to prove that 239 fuzzing entry points across 123 open-source libraries can’t crash on any input up to 64 MB. While doing it, Claude also found hundreds of bugs that years of testing had missed.

Why this used to be impractical

Formal verification turns code into a mathematical model and then proves the code always follows a set of rules. It works, but it’s very expensive. Anthropic points to the seL4 operating system kernel, which took two person-years to build and 20 person-years to verify. That’s why the technique has mostly stayed in places like Airbus avionics.

What the researchers did

The hard part is usually the spec, which is the precise definition of what “correct” means. The team got around that by reusing tests developers had already written:

• They started with fuzz tests from Google’s OSS-Fuzz project. These tests crash whenever something goes wrong, including memory errors caught by AddressSanitizer.
• They compiled each library and its test to RISC-V machine code.
• Using Theorem’s models of RISC-V and Linux, they turned “this test never crashes for any input under 64 MB” into a formal spec.
• Claude wrote the proofs in Rocq, a proof assistant whose checker verifies every step.
• When Claude hit a real bug, it patched the code and then proved the patched version.

The Rocq checker validates the proofs automatically, so nobody has to read them. You only have to trust the RISC-V and Linux models, the theorem statements and the checker itself.

The numbers

Newer models make a real difference. On 36 small verification tasks, Opus 5.5 proved half of them using about 40% fewer tokens than Opus 5. When agents could share and copy each other’s proofs, they used another 17% fewer tokens.

Bugs fuzzers would never find

This is the part that stands out most. Fuzzers usually cap inputs at around 1 MB, so they miss bugs that only show up with large, unusual inputs. Claude found:

• An out-of-bounds write in a decompressor, triggered only by inputs of about 20 MB with a rare layout
• An out-of-bounds read in an image decoder that needed a 64 MB input and over 2 GB of memory
• CVE-2026-56132 in libexpat, found again independently
• A logic bug where a restriction on which files an app can load wasn’t always enforced

Side experiments went further. Claude proved that the zlib code in the Linux kernel matches its RFC 1950 spec, working directly on the x86 binary. It also built a Python interpreter in Rust, verified with Verus, that behaved the same as CPython on 99.95% of 1.7 million random programs. And a week spent trying to verify a widely used PDF reader turned up as many security bugs as usually get reported in a year.

Limitations Anthropic flags

The team is blunt about it:

“‘Formally verified’ does not mean ‘bug-free.'”

• The proofs cover single-threaded, static RISC-V binaries linked against musl. Most people run these libraries on x86 or ARM with glibc.
• AddressSanitizer doesn’t catch every memory bug, and the team didn’t verify every entry point.
• A single proof can still take hundreds of millions of tokens.
• Letting Claude patch code creates a reward-hacking risk. It could “fix” a program into one that trivially never crashes. The team penalized patches and audited every one.

What you can do with this

This matters because AI keeps getting better at finding exploitable bugs, and attackers have the same tools. Proofs change the defense from “we haven’t found a bug yet” to “this kind of bug can’t exist here.”

Some practical steps:

• If you maintain an open-source project, Theorem is offering to run the same pipeline on other open-source projects.
• Try Theorem’s published Claude skill on your own code.
• If you tried LLM-assisted verification with older models and gave up, Anthropic is explicitly asking you to try again.
• Start with your most critical dependencies. Proofs can be reused, so verifying a shared library once pays off everywhere it’s used.

Anthropic predicts verification will soon be “as practical as fuzzing is today.” Token cost is the real bottleneck now. If each model generation keeps cutting it by around 40%, verified dependencies could become a security requirement before most teams are ready. My advice is to pick one critical library you depend on and test this workflow now, while it’s still optional. The full writeup, the published proofs and a technical appendix are available from Anthropic.