Claude wrote formal proofs for 123 open-source libraries

Anthropic says Claude has written machine-checked proofs that a large set of real open-source code cannot crash. The claim is bounded, and the post states the bounds itself. We read Anthropic’s research post in full, including its limitations section and footnotes. This article covers what was proved, what the results rest on, what the proofs do not cover and why it matters for AI-driven bug finding. We did not check the proofs or run the published artifacts.

What did Anthropic and Theorem do?

They had Claude prove properties about compiled programs, not source code. Working with Theorem, Anthropic says Claude proved that 239 fuzz-test entry points across 123 libraries in Google’s OSS-Fuzz project always exit normally, without memory-safety errors or failed assertions, for every input smaller than 64 MB. The proofs are about RISC-V machine code, are written in the Rocq proof assistant and use Theorem’s formal models of the RISC-V instruction set and Linux processes. Anthropic says the work took a few weeks, totals about 180 million lines of Rocq, with a typical proof of about 600,000 lines for binaries with a median of 18,000 instructions, and is, to its knowledge, the first large-scale effort to apply AI formal verification to production software at the assembly level.

How do fuzz tests become proofs?

Anthropic reuses a spec that already exists. A fuzz test is an entry point that takes input, and any input that crashes it is a bug. Anthropic turns “this fuzz test never crashes” into a formal statement about the compiled RISC-V code. If Claude proves it, fuzzing that entry point can find nothing more within the stated limits. Anthropic’s point is that this avoids the hard part of formal verification, writing a spec for what a program should do. When a proof fails, the failure points to a possible bug, so Claude patched the code and regenerated the spec, then proved the patched version. Anthropic says virtually none of that proof code needs manual review, since the Rocq checker verifies it against the spec.

What bugs did it find?

Anthropic says attempting the proofs surfaced hundreds of bugs, including ones a fuzzer would be unlikely to reach. Its examples:

• A counter underflow in a decompressor leading to an out-of-bounds write, only on inputs of about 20 MB with one rare layout.
• An out-of-bounds read in an image decoder that needed a 64 MB input and more than 2 GB of memory.
• An out-of-bounds read in another library that needed a specific sequence of calls across two handles to the same file.
• A rediscovery of CVE-2026-56132 in libexpat, which needed deeply nested input.
• A logic bug that never crashes: a feature meant to restrict which files an application can load was not always enforced.

Anthropic’s summary also says Claude found bugs that “had eluded detection for years, despite trillions of test runs”. That is Anthropic’s framing, and the post does not list how many of the hundreds were previously known or fixed upstream.

What else did Anthropic try?

Three smaller experiments, each reported as promising rather than finished:

• zlib: Claude wrote a formal spec of RFC 1950 and proved that the zlib in the Linux kernel, compiled for x86, implements it, using x86 semantics Claude generated. Anthropic repeated this for about six other libraries and found minor, unexploitable corner-case bugs that are being filed upstream.
• A Python interpreter in Rust: Claude wrote an interpreter for a large subset of Python and used the Verus tool to prove that it follows a published semantics of CPython. On 1.7 million random programs, behavior matched CPython in 99.95% of tests.
• A PDF reader: Anthropic says a verification attempt on a widely used PDF reader found as many security bugs in one week as are typically reported in a year, and that another widely used application had a logic bug latent for more than a decade. It does not name them.

What does it cost, and is it getting cheaper?

Expensive today, with a trend Anthropic describes as improving. It says proofs can take hundreds of millions of tokens. On 36 small verification tasks built from OSS-Fuzz code, it reports that Opus 5.5 proves half using about 40% fewer tokens than Opus 5, and a chart in the post shows Opus 5.5 completing more tasks than Opus 5 and Fable 5.1 at lower token budgets. When agents could copy each other’s proofs in a shared workspace they needed 17% fewer tokens than agents working alone, and Anthropic says most of a proof concerns code every program contains, so proofs overlap heavily.

What does it not prove?

Anthropic is explicit: “formally verified” does not mean “bug-free”. Its limitations section says:

• The real machine differs from the model. The proofs are about single-threaded static RISC-V binaries linked against musl, while most people run these libraries on x86 or ARM with glibc.
• The claim does not cover everything. AddressSanitizer does not detect all memory-safety bugs, not every entry point was verified, a whole library is not covered even if every entry point were (dead code, for one), and callers can still misuse a library and corrupt memory.
• Trust moves, it does not vanish. You must trust the formal models of RISC-V and Linux, the exact theorem statements, the Rocq checker and, per Anthropic’s footnote, the hardware, the OS and the OCaml compiler the checker relies on.
• Reward hacking is possible. Because Claude may patch code, it could make a theorem provable by rewriting a program into one that trivially never crashes. Anthropic says it penalized patches, rewarded proving how few inputs a patch changes, and logged and audited patches.
• Some proofs are withheld. Anthropic is not releasing proofs that may reveal an unpatched bug.

What is released?

Anthropic says it is publishing the trusted components not already public, Claude’s complete Rocq proofs for fuzz tests that needed no patching, and specs for fuzz tests it could not prove, and that Theorem offers to run the pipeline for other open-source projects and publishes a Claude skill for starting one. It links a proof subset, Theorem’s RISC-V and Linux semantics, Theorem’s service page and a full appendix. We did not open them.

What is still unknown?

• Independent verification. Anthropic invites it. We saw no outside check yet.
• How many of the hundreds of bugs were new, and how many are fixed upstream.
• Whether the approach carries over to x86, ARM, dynamically linked glibc and multithreaded code, which Anthropic names as the gaps to close.
• What the cost per library is outside the 36-task benchmark.

What to keep in mind

These are our observations:

• The claim is a narrow one, stated narrowly. “No crash on inputs under 64 MB under these assumptions” is much weaker than “secure”, and Anthropic says as much.
• The method fits the current moment. The same capability that finds bugs now also checks fixes. See our PHP report for AI-assisted research finding critical bugs in a mature codebase.
• The numbers are Anthropic’s own. The token savings, the bug counts and the 99.95% match rate come from the post and are not independently measured.
• The trusted base is small but real. Hardening Rocq and the machine models matters more once many proofs depend on them.

Editorial review: October 23, 2026 (AI). Prepared from Anthropic’s research post “LLMs are making formal software verification feasible at a much larger scale” (dated October 22, 2026 in the page metadata, which was modified again on October 23), read in full as page text including its limitations and footnotes. We did not read the appendix PDF, open the proofs, the Theorem repositories or the service page, run anything, or contact Anthropic or Theorem. Numbers are Anthropic’s own. The page may change after our reading.