Anthropic says it has used Claude to write mathematical proofs that 239 entry points in 123 widely fuzzed open-source libraries cannot crash on any input up to 64 MB. The company’s Frontier Red Team published the work on 22 October, describing it as a collaboration with Theorem, a company whose stated aim is to “verify all software”. It calls the project, “to our knowledge”, the “first large-scale effort to use AI to apply formal verification to production software at the assembly code level”.
The proofs were a defensive exercise. Anthropic says the attempt to prove each library safe “discovered hundreds of bugs”, some of which “had eluded detection for years, despite trillions of test runs”. Claude patched them and then completed the proofs, the company says, all “over the span of a few weeks”.
Theorem is now offering the same pipeline to open-source projects free of charge, and a subset of the proofs is public on GitHub for anyone to check.
In brief
- What happened: Anthropic and Theorem say Claude produced machine-checked proofs that 239 OSS-Fuzz entry points never crash on inputs up to 64 MB, after finding and fixing hundreds of bugs.
- Why it matters: Formal proof rules out whole classes of crash for every input in scope, where fuzzing can only sample inputs.
- What’s unknown: The proofs cover RISC-V builds linked against musl, while most deployments run x86 or ARM with glibc, and several library entry points were left unproved.
The proofs cover compiled RISC-V binaries, not source code
The libraries all come from Google’s OSS-Fuzz programme. Anthropic turned their existing developer-written fuzz tests into formal specifications that Claude had to prove would always pass, including against crashes flagged by AddressSanitizer (ASan), a memory-error detector.
The proofs work on the compiled machine code rather than the source. Each library and its fuzz test are compiled to a RISC-V executable, which is translated into a mathematical model using Theorem’s semantics for RISC-V instructions and Linux processes. Claude writes the proof and the Rocq proof assistant’s kernel checks it.
The scale is large. Anthropic says the proofs “comprise about 180 million lines of Rocq, with a typical proof running to about 600,000 lines” for binaries with a median length of 18,000 RISC-V instructions. By comparison, the company notes that the seL4 operating system kernel took two person-years to build and 20 person-years to verify by hand.
The guarantee is conditional. Anthropic says the proofs assume “the program runs as a single-threaded static binary with a fixed memory budget on a RISC-V CPU using Linux OS”, and that the RISC-V and Linux models, the theorem statements and the Rocq checker all have to be trusted.
Proving the code turned up bugs fuzzers rarely reach
Fuzzers mutate small inputs, “typically capped at 1 MB”, Anthropic says, so some of the bugs Claude found sat well outside their range. One was a counter underflow in a decompressor that caused an out-of-bounds write, “but only on inputs of around 20 MB that had one rare, specific layout”. Another, in an image decoder, needed a 64 MB input and more than 2 GB of memory.
Claude also rediscovered CVE-2026-56132 in libexpat, the widely used XML parser. Anthropic says the bug “needed deeply nested input”. The NVD entry, published on 19 June, describes it as a heap-based buffer overflow in libexpat before version 2.8.2, rated 6.9 (medium), caused by mishandled memory reallocation “when there is data-structure sharing across parsers”. The fix is in libexpat pull request 1272.
Some findings never crashed at all. While proving one library memory-safe, Claude noticed that a feature restricting which files an application can load “isn’t always enforced”, the company says.
Anthropic also addressed an obvious shortcut: Claude could make any program provable by rewriting it so that it never crashes. To discourage this, the team says it “penalized any patch” and “logged and audited the patches”.
Anthropic says “formally verified” does not mean “bug-free”
Anthropic’s own limitations section is blunt. “‘Formally verified’ does not mean ‘bug-free,'” it says. A proof shows only that a program meets its specification, and the specification can be wrong.
The deployment gap is the largest caveat. “Our proofs are about single-threaded, static RISC-V binaries linked against musl libc. However, most people run these libraries on x86 or ARM and dynamically link them against glibc,” the company writes.
Coverage is partial too. “ASan doesn’t detect all memory safety bugs, and we didn’t verify all the entry points for each library,” Anthropic says, adding that callers could still misuse a library and corrupt memory themselves. Theorem’s repository README adds that a proof “does not say” a library is correct: wrong results and memory leaks are not excluded, and no proof in the release rules out a program that runs forever.
The public release is also a subset. Theorem’s repository lists proofs for 60 entry points in 25 libraries, against the 239 entry points in Anthropic’s headline figure. Anthropic says it is withholding proofs that “may reveal an unpatched bug”.
Theorem’s free scheme sends AI-written bug reports with no promise of review
Theorem’s OSS Verify scheme mirrors OSS-Fuzz. Maintainers enrol by pull request, supplying a build script that produces static riscv64 binaries, and qualifying projects pay nothing. The proof target is that “no input up to 64 MiB can cause a crash”, and individual proofs “can take multiple days”, Theorem says.
Bugs are disclosed privately to maintainers. Theorem states plainly: “Findings and patches are generated by AI models, and we don’t promise that a person reviews them before we send them. We set no disclosure deadline, and we don’t publish findings.”
That mirrors the approach Anthropic took with OSS Scanner, the free service that sends open-source projects unreviewed, model-written bug reports under its Cyber Mission. It also sits alongside the company’s Cyber Verification Program, which loosens Claude’s safeguards for vetted security teams. More defensive uses of AI are collected in TSN’s Tech for Good hub, and attacks the work aims to prevent are tracked in the ransomware and cyber attacks hub.
A proof moves the weak point from the code to the model of the machine
Fuzzing answers the question of which inputs have been tried. A proof answers a different one: under these assumptions, can any input in range cause a crash? For maintainers, that changes where scrutiny belongs. The code is no longer the main thing to trust; the trusted base is Theorem’s model of RISC-V and Linux, the specification derived from each fuzz test, and the Rocq checker. Anthropic’s own footnote adds the hardware, the operating system and the OCaml compiler to that list.
That is why the musl-on-RISC-V restriction matters more than it might first appear. The bugs found while proving are real bugs in shared source code, and their fixes help every platform. The guarantee itself, however, attaches to a build that few production systems run. Anthropic acknowledges this and says closing the gap needs system models closer to deployed machines. It reports one step in that direction: a proof for the Linux kernel’s zlib on x86 against the RFC 1950 compression specification.
Cost is the other constraint. Anthropic says proofs “can take hundreds of millions of tokens” and points to efficiency gains, including Opus 5.5 proving half of 36 test tasks “with about 40% fewer tokens than Opus 5” and a 17% saving when agents shared each other’s proofs. Its conclusion that verification “will soon be as practical as fuzzing is today” is a forecast, not a result. Theorem’s own roadmap for the Nix software ecosystem prices verifying all of it at about $6.4bn at today’s rates, a figure that depends on proving shared libraries once and reusing them everywhere.
The cheapest test of the claims is already open: the released proofs are MIT-licensed and can be re-checked by anyone with Rocq 9.2.0. Theorem puts the cost of proving OpenSSL, which sits beneath nearly 16,000 Nix packages, at about $220,000, or roughly $14 for each package that would reuse the proof.
Sources
- Anthropic: LLMs are making formal software verification feasible at a much larger scale, 22 October 2026
- Theorem: OSS Verify, free formal verification for open source
- GitHub: theorem-labs/oss-verify-proofs
- Theorem: Bootstrapping the Verified Software Stack, 29 September 2026
- NVD: CVE-2026-56132
- GitHub: libexpat pull request 1272
Related stories
- Anthropic Launches the Anthropic Cyber Mission: Critical-Infrastructure Programme and Free Open-Source Scanner
- Anthropic’s Cyber Verification Program: Three Tiers of Looser Guardrails for Vetted Defenders
Follow @tsnmediahub on X for breaking AI news as it happens.
Follow on X
