Claude proved 239 open-source entry points crash-free in machine code — what Anthropic's proofs do and don't cover

Anthropic's Frontier Red Team and the verification company Theorem say Claude has produced machine-checked proofs that 239 fuzz-test entry points in 123 OSS-Fuzz libraries cannot crash on any input up to 64 MB, and that the effort uncovered "hundreds of bugs" that years of fuzzing had missed. The result is real and the proofs are partly public, but the guarantee is narrower than the headline: it covers statically linked RISC-V binaries with the musl C library, errors a sanitizer can see, and only the entry points that were proved. Our assessment: this is the most credible sign yet that AI changes the economics of formal verification for defenders — and the most likely to be over-read as "these libraries are now bug-free".

The short version

Open-source libraries — image decoders, JSON parsers, compression code — sit underneath almost everything in IT. The standard way to harden them is fuzzing: Google's OSS-Fuzz runs developer-written "fuzz targets" that feed endless random inputs into a library and watch for crashes. Fuzzing is good at finding bugs, but it can never show that none remain.

Formal verification can: it produces a mathematical proof that a program behaves as specified for every possible input. It has historically been so expensive that only a handful of projects — the seL4 microkernel is the textbook case — have attempted it. Anthropic's post, published on October 22, 2026, argues that large language models now make it affordable at scale.

The method is simple to describe. Each existing fuzz test was turned into a statement — roughly, "this fuzz target will not crash for any input smaller than 64 MB" — about the compiled machine code, not the source. Claude then wrote proofs in the Rocq proof assistant, and Rocq's checker, not Claude, decided whether each proof was valid. Where a proof could not go through because the code really was broken, Claude patched the bug and proved the patched version.

The proofs are only as wide as their assumptions, and Anthropic states those openly: one CPU architecture (RISC-V), one minimal C library (musl), static linking, single-threaded execution, a fixed memory budget, and a model of Linux process behaviour.

Timeline

• October 22, 2026 — Anthropic publishes "LLMs are making formal software verification feasible at a much larger scale" on its research site, credited to the Frontier Red Team with 15 named authors, in partnership with Theorem (the page metadata shows a modification on October 23, 2026).
• With the post — Anthropic links Theorem's public repository theorem-labs/oss-verify-proofs (a subset of the proofs), the RISC-V/Linux semantics (rocq-linux-process-semantics) and a Claude skill for adding new projects; the repository page shows no release date.
• October 22–23, 2026 — Trade coverage (Interesting Engineering and others) repeats Anthropic's figures; we found no named independent expert reaction as of November 5, 2026.
• Undated, "over the span of a few weeks" — the period in which, according to Anthropic, the 123-library proofs were produced.

What we know

Scale. Anthropic says Claude "formally proved security properties in the compiled code of 123 open-source libraries" — 239 OSS-Fuzz entry points proven crash-free for inputs up to 64 MB, out of hundreds of projects attempted. The proofs total about 180 million lines of Rocq; a typical one is around 600,000 lines, for binaries with a median of 18,000 RISC-V instructions. (Anthropic)

What is trusted. According to Anthropic, the trusted base is the RISC-V and Linux process semantics, the theorem statements, the Rocq proof checker, plus the hardware and the OCaml compiler. Claude's own output is not trusted: a proof either checks or it does not.

Bugs. Anthropic writes that "the process of attempting to prove these specs discovered hundreds of bugs" and that "Claude successfully patched the bugs it found". The examples it gives are instructive because they are exactly what random testing struggles to reach: a counter underflow in a decompressor triggered only by inputs around 20 MB with one rare layout; an out-of-bounds read in an image decoder that needs a 64 MB input and more than 2 GB of memory; an out-of-bounds read that requires a particular sequence of calls on two handles to the same file; a rediscovery of libexpat's CVE-2026-56132 through deeply nested input; and a file-restriction feature that was not always enforced — a logic bug that never crashes. Anthropic gives no total count, no severity breakdown and, except for zlib, no statement on upstream reporting.

Other case studies. Anthropic says Claude wrote a specification for zlib from RFC 1950 and proved the Linux kernel's zlib correct at the x86 binary level, then repeated similar work for about six other libraries, finding "minor" corner-case bugs that are "in the process of being filed upstream". It also describes a Rust Python interpreter verified with Verus that matched CPython's behaviour on 99.95% of 1.7 million random programs, and a week of work on "a widely used PDF reader" (unnamed) in which "we found as many security bugs in one week as are typically reported in a year", including "a previously unknown logic bug that had been latent for more than a decade".

Gaming the proof. Anthropic flags an obvious failure mode: "Claude could make any theorem provable by rewriting the program into one that trivially never crashes." Its counter-measures were to penalise any patch, reward minimal changes, and log and audit every patch.

Cost. Anthropic calls cost the main limitation — proofs can take "hundreds of millions of tokens" — but publishes no compute or dollar figures. In a smaller experiment on 36 OSS-Fuzz tasks (three attempts, 5 million-token budget each), it reports that "Opus 5.5 proves half of them with about 40% fewer tokens than Opus 5", and that a shared proof workspace cut tokens by 17%, with 30 of 34 completed proofs cheaper when sharing and two completed only in the shared setting. Anthropic does not name the model used for the main 123-library run.

What is public. Theorem's repository, which we read on October 28, 2026 and re-checked on November 5, 2026 (no change to the figures below), describes itself as "Theorem statements about OSS-Fuzz fuzz targets as compiled RISC-V binaries, and machine-checked Rocq proofs of them". It lists proofs for 25 libraries and 60 entry points — among them OpenSSL, mbedTLS, zstd, bzip2, libpcap and simdjson — and a status table of 20,164 statements across 427 projects, of which 138 are marked proved and 19,797 open. Anyone can re-check a proof in a pinned Docker image; the tooling rejects any axiom not on an allowed list.

Technical analysis

Why proving the binary matters. Most verification work proves properties of source code and then trusts the compiler. Here the statement is about the RISC-V machine code that actually runs, so compiler optimisations, undefined-behaviour surprises and linker effects are inside the proof rather than outside it. That is a meaningful step up from source-level analysis — and it is also why the result does not transfer for free to x86 or ARM builds.

Turning tests into specs is the clever part. Writing specifications is usually the expensive, expert-only half of verification. Reusing OSS-Fuzz harnesses side-steps that: each harness already encodes a developer's idea of "this entry point should never misbehave on arbitrary bytes". The property proved is therefore modest but universal — no sanitizer-detectable error for any input below 64 MB — and it is exactly the class of bug (out-of-bounds reads and writes, underflows, failed assertions) that dominates memory-safety CVEs in C and C++ libraries.

Why this found what fuzzing missed. Fuzzers sample; proofs must account for every path. A bug that needs a 20 MB input with one rare layout, or two handles on one file used in a specific order, is a needle that random mutation rarely hits, but it blocks a proof outright. Our assessment: the bug-finding is a by-product of the proof attempt, and it is the part defenders can use immediately.

The AI angle. Nothing in the method is new to verification researchers; what is new is the labour. 180 million lines of proof in a few weeks is a volume no human team could produce. The security-relevant design choice is that the model is kept outside the trusted base: Claude generates, Rocq checks. That makes the approach robust to hallucination in a way that LLM-based code review is not. The remaining trust in Claude sits in two places Anthropic acknowledges — the patches (hence the audit for "trivially never crashes" rewrites) and any specification Claude wrote itself, such as the zlib spec from RFC 1950.

Read the theorem, not the headline. Theorem's README is blunter than the blog. The proofs cover agreement between plain and sanitizer builds, "not library correctness"; wrong results and memory leaks are not excluded; and "no proof in this release proves a halts statement", so none rule out a run that never ends — a hang is still a denial of service. Anthropic's own limitations list adds that ASan does not catch every memory error, that dead code and unproved entry points are not covered, and that callers can still misuse a library. Our assessment: "crash-free for this fuzz target on RISC-V/musl" is the accurate summary; "memory-safe library" is not.

The offensive mirror. Anthropic frames the work against a world in which "AI can now easily find and exploit" bugs and chain benign ones into critical exploits. The same capability that writes a 600,000-line proof can locate the place where a proof fails — which is a precise pointer to a bug. Anthropic says it is withholding proofs that could reveal unpatched bugs, which implicitly concedes this. It fits a broader pattern we have tracked: Google found that half of the vulnerabilities AI discovers allow code execution, and Microsoft's AI bug-hunting lab says finding bugs is no longer the hard part. Proofs are one of the few AI outputs that push the balance back toward the defender, because they establish absence rather than presence.

What remains unclear

• Which model, and at what cost. The main run is attributed only to "Claude". There are no compute, dollar or wall-clock figures beyond "a few weeks" and "hundreds of millions of tokens".
• How many bugs, how severe, and who was told. "Hundreds" has no denominator, no severity scale and, apart from the zlib items and the rediscovered libexpat CVE, no list of reports or CVEs. Maintainers' views on the patches are not quoted.
• Public versus claimed. The repository lists 60 entry points in 25 libraries against Anthropic's 239 in 123. Anthropic calls the release a subset and says unpatched-bug proofs are withheld; the repo reports "0 withheld" yet marks 32 projects as "held" without explaining the category. We could not reconcile these from the public pages, which were unchanged as of November 5, 2026.
• The PDF reader. It is unnamed, and "a year's worth of bugs in a week" is not quantified.
• Portability. Anthropic presents x86 and ARM, glibc and dynamic linking as gaps, but gives no timeline for closing them. The zlib result shows x86 is possible for hand-picked cases.
• Independent review. We found no named outside verification expert assessing the work as of November 5, 2026.

Lessons and what to do

For security teams

• Treat "formally verified" claims from any vendor as a claim about a theorem. Ask: which property, which binary, which architecture, which libc, which entry points, and does it prove termination?
• The libraries in Theorem's repository include components you probably ship (OpenSSL, mbedTLS, zstd, bzip2, libpcap). A proof for a RISC-V/musl build does not cover your distribution's x86 glibc package — keep patching on normal cadence and watch upstream advisories for fixes coming out of this work.
• Expect a wave of upstream fixes from AI-driven verification and bug-finding. Track them like any other patch stream rather than as noise.

For AI builders and maintainers

• Fuzz harnesses just became more valuable: each one is a ready-made specification. Projects with good OSS-Fuzz coverage are the ones this approach can reach first.
• Copy the trust architecture, not just the model: let the model generate and an independent checker decide. Log and review every code change the model makes to "make the proof pass".
• Decide in advance how you will handle proofs that reveal unpatched bugs — they are vulnerability disclosures in another form.

For leadership

• Proof generation is moving from research cost to engineering cost. It is reasonable to ask suppliers of security-critical components whether machine-checked guarantees are on their roadmap — and what exactly those guarantees cover.
• Do not let a proof replace testing, sanitizers or patch management. Anthropic itself says "'Formally verified' does not mean 'bug-free.'"

Sources

• Anthropic, "LLMs are making formal software verification feasible at a much larger scale", October 22, 2026: https://www.anthropic.com/research/formal-verification
• Theorem, oss-verify-proofs repository (README and status table, read October 28 and November 5, 2026): https://github.com/theorem-labs/oss-verify-proofs
• Theorem, rocq-linux-process-semantics: https://github.com/theorem-labs/rocq-linux-process-semantics
• Theorem, Claude skill for adding projects: https://github.com/theorem-labs/oss-verify/blob/main/.claude/skills/add-project/SKILL.md

Coverage:

• Interesting Engineering, October 22, 2026: https://interestingengineering.com/ai-robotics/claude-formal-verification-software-security