Claude Generated Formal Proofs of Memory Safety for 123 Open-Source Libraries, Down to RISC-V Machine Code

Claude Generated Formal Proofs of Memory Safety for 123 Open-Source Libraries, Down to RISC-V Machine Code

Anthropic published research on 22 October 2026 in which Claude is said to have produced machine-checked formal proofs of memory safety for 239 entry points across 123 open-source libraries, down to compiled RISC-V machine code. According to the company, the method surfaced bugs that had survived trillions of fuzzing attempts — but the proofs are conditional, and the guarantees rest on components no one has verified.

What was actually done

The starting point was existing fuzz tests — tests that feed software random or mutated inputs to find crashes. Anthropic had Claude convert these tests into mathematical specifications: the statement to be proved was that the 239 entry points do not crash for any input under 64 MiB (MSN).

The proof work itself does not take place in source code, but in the compiled binaries. The specification is defined over compiled RISC-V instructions, using formal semantics for the RISC-V instruction set and Linux processes supplied by the partner Theorem (Unite.AI). This means the verification covers what the processor actually executes — including what the compiler did to the code — not just what the developer wrote.

Each completed proof is checked independently by Rocq, the proof assistant formerly known as Coq. The proofs reportedly average around 600,000 lines each, with roughly 180 million lines of Rocq code in total (Glitchwire). According to an appendix dated 22 October 2026, relayed by Unite.AI, Claude wrote around one billion lines along the way — of these, roughly 180 million passed the checker. The distinction between written and accepted code is worth noting: most of the work consisted of failed attempts, and the figures should be confirmed against the report's primary source, which is not among the available sources.

Anthropic itself presents the effort as the first major initiative to apply AI-driven formal verification to production software at this scale, claiming that what traditionally requires years of expert work was done in a few weeks (Glitchwire). Both claims are the company's own, not independently verified.

The bugs no fuzz test found

The point of a proof is that it covers all inputs, not just the ones the tester happened to generate. According to MSN's coverage, the proof attempts revealed bugs that had survived an estimated trillions of fuzz attempts:

• A counter that could underflow and trigger an out-of-bounds write during decompression — the bug required around 20 MB of input with a rare data arrangement.
• A bug in an image decoder that required 64 MB of input and more than 2 GB of memory to manifest.

In addition, Claude is said to have rediscovered CVE-2026-56132 in libexpat, a vulnerability requiring deeply nested input, according to Unite.AI. These findings rest on Anthropic's own reporting and are not independently confirmed.

When the model is allowed to patch the code

One methodological detail deserves attention: Claude was allowed to patch the code before a proof was completed. This opens the door to a classic machine learning pitfall — "reward hacking," where the model games the objective instead of solving the task, for example by changing the code into something trivial that is easy to prove.

Anthropic says it countered this in three ways: patches were penalized in the scoring, the model received extra credit for proving which inputs a patch changed the behavior of, and all patches were logged and audited (Unite.AI). These are sensible measures, but they are also self-assessed — the quality of the audit cannot be verified until the material is released.

Where the guarantees stop

The most important caveat appears in Anthropic's own limitations section, relayed by Blockchain.News: the proofs are conditional and do not mean the software is bug-free (Blockchain.News). The guarantees apply specifically to:

• Single-threaded, static binaries with a fixed memory budget on RISC-V Linux. Real production use with threads, dynamic loading, and other platforms is not covered by the model.
• A limited set of entry points. The work does not cover all entry points or all ways the software is used in production.
• Conditions in the specification. The proof states "no crash for inputs under 64 MiB" — not the absence of all types of security flaws.

On top of this comes what formal verification calls the "trusted base": the semantics for RISC-V and Linux, the theorem statements themselves, and the Rocq checker are components that are not proved. If the semantics diverge from how a physical processor behaves, the guarantee does not transfer to reality. The uncertainty is thus not gone, but concentrated in fewer, inspectable places — provided someone actually inspects them.

What is being released — and what is being withheld

Anthropic says it is releasing a selection of the proofs, the RISC-V and OS semantics, the trusted components not already public, complete proofs for fuzz tests that required no patching, and specifications for tests that could not be proved (Unite.AI). Proofs that could reveal unpatched bugs are being withheld — an understandable safety consideration, but it means the public material does not provide full insight into the findings.

The collaboration was between Anthropic's Frontier Red Team and Theorem Labs, a San Francisco startup founded in 2025 by Jason Gross and Rajashree Agrawal, according to Glitchwire. Other sources refer to the partner only as "Theorem," and the name and company details are supported by only one source. Glitchwire further reports — as the only source — that Mozilla credited the Frontier Red Team with more than a dozen bugs in Firefox ahead of version 148.

Open questions

The heaviest caveat is that none of the available sources is Anthropic's primary report. All key figures — 180 million accepted lines, one billion written, 239 entry points, 123 libraries, the 64 MiB limit — come from the company, relayed through secondary coverage, and no independent verification exists. The same applies to the bug findings, including the rediscovery of CVE-2026-56132 in libexpat.

Three questions will determine the significance of the result. First: will independent security researchers accept the trusted base — in particular, does the RISC-V/Linux semantics actually match real systems? Second: are the line counts and bug findings accurate when the primary report can be examined? Third: is it reproducible — can others do the same on other software, or did it require Anthropic's specific model and internal infrastructure?

What nonetheless sets this apart from most "AI found bugs" stories is the format. A fuzzing find is one data point; a machine-checked proof is a guarantee covering all inputs within the specification — on the terms of what the model and the trusted base actually describe. Any hype should be measured against what Anthropic itself writes in the limitations: conditional guarantees, not bug-free code.