Claude Proved Memory Safety Across 123 Libraries – Under Strict Assumptions

Claude Proved Memory Safety Across 123 Libraries – Under Strict Assumptions

On 22 October 2026, Anthropic published results the company itself describes as the first large-scale, AI-driven formal verification of production software at machine-code level.

Anthropic published results on 22 October 2026 that the company itself describes as the first large-scale, AI-driven formal verification of production software at machine-code level. Around 180 million lines of Rocq proofs were accepted by the proof checker – but the guarantees hold only under narrow assumptions, and several of the most concrete figures so far come from secondary sources quoting the release.

The company's Frontier Red Team – in collaboration with Theorem Labs, according to Crypto Briefing – had Claude produce machine-checked formal proofs that compiled programs exit normally without memory-safety errors or assertion failures, for all inputs under 64 MB. Around 180 million lines of proofs in the proof language Rocq were accepted by the proof checker, spread across 239 entry points in 123 open-source libraries from OSS-Fuzz (Anthropic; ChainCatcher).

The numbers are striking, but they require careful reading. The proofs hold under narrow assumptions: single-threaded, statically linked binaries with a fixed memory budget on a RISC-V processor running Linux, where the operating system's responses are modelled, not executed. Anthropic itself stresses that the result does not mean the libraries are free of vulnerabilities.

What Was Actually Proved

The core of the result is an existence guarantee: Anthropic writes that Claude proved that the programs in question "will always exit normally without triggering memory-safety errors or failed assertions, for any input under 64 MB and any modelled Linux response and memory layout" (Anthropic). The phrase "any input under 64 MB" is what separates this from testing: a fuzz test can try millions of inputs, a formal proof covers in principle all of them at once.

But the guarantee rests on four assumptions that deserve careful reading:

• RISC-V, not x86 or ARM. The proofs target compiled RISC-V instructions (Anthropic; ChainCatcher). The same library compiled for a different architecture is not covered.
• Single-threaded, statically linked binaries. Race conditions between threads, dynamically linked libraries, and complex startup configuration fall outside the scope.
• Fixed memory budget. The program is assumed to operate under a fixed memory cap.
• Modelled Linux. The operating system's responses and memory layout are modelled in the proofs. A model is not the actual kernel – if the model deviates from real Linux behaviour, the proof does not automatically carry over to the running software.

Within these boundaries, the proofs are machine-checked: the Rocq kernel has verified that every inference follows from the previous ones, from axioms down to machine instructions. That means the proofs themselves cannot contain logical errors that the checker has missed. It does not mean that the specifications – the claims about what should be proved – match what the user actually wants. Anthropic points to this itself: the proof checker cannot confirm that the specifications correspond to reality (as reported in ChainCatcher's coverage of the release). A proof is only as strong as the specification it proves.

How It Was Done: From Fuzz Tests to Formal Specifications

The technical entry point was Google OSS-Fuzz, Google's service that continuously fuzz-tests open-source libraries. OSS-Fuzz projects come with compilable fuzz tests – small programs that call the library's entry points with generated inputs. The team converted these tests into formal specifications: instead of running the test on selected inputs, they formulated the test as a mathematical statement about all possible inputs (ChainCatcher).

Claude was then tasked with proving the properties at machine-code level. This is a significant choice: proofs at source-code level require trusting that the compiler does what it is supposed to. By targeting the compiled RISC-V instructions, that step is eliminated – the guarantee applies to what actually runs on the processor, not to what was written in the C code.

The process was not clean from the first attempt. ChainCatcher writes that Claude proved the properties for 239 entry points in 123 libraries "after patching identified issues" – meaning the work uncovered bugs in the libraries themselves that had to be fixed before the proofs could be completed (ChainCatcher). The whole effort reportedly happened "within weeks", according to the same source.

The Scale in Numbers – and What Rests on Secondary Sources

The figures fall into two layers: what appears in Anthropic's own publication, and what is so far known through coverage of the release and its appendix.

From Anthropic's own publication (Anthropic):

• 123 open-source libraries.
• An input limit of 64 MB.
• The assumptions of a single-threaded, statically linked binary with a fixed memory budget on RISC-V running Linux.
• The seL4 comparison: it took two person-years to implement the seL4 kernel, but 20 person-years to formally verify it. According to Anthropic, formal verification has therefore been practical only in mission-critical systems, such as Airbus's flight-critical code.

From secondary sources quoting the release and its appendix (ChainCatcher; Unite.AI):

• 239 entry points across 123 libraries.
• Around 180 million lines of Rocq accepted by the proof checker.
• Around 1 billion lines of Rocq written in total – meaning roughly 18% of the model's proof attempts survived checking.
• cJSON: one entry point in a 391-line parser required a 630,000-line proof. fftw3, with 51,000 lines of code linked in, required 480,000 proof lines.

The cJSON ratio is the most illustrative figure in the material: the proof was more than 1,600 times longer than the code it proved. This points to why formal verification has historically been out of reach for ordinary software – not because the claims are difficult, but because the workload of proof construction is enormous. Measured against Anthropic's seL4 figures, 180 million accepted lines represent a task that would traditionally be counted in tens of person-years.

An important caveat about sourcing: the details on 239 entry points, 180 million lines, the bug count, and the interpreter project are drawn here from ChainCatcher's and Unite.AI's rendering of the release, not verified directly against the full primary text. If the secondary sources have summarised correctly, the picture is as described.

The Bugs Uncovered Along the Way

The proof effort also functioned as an unusually aggressive bug hunter. According to Unite.AI, which cites the release's appendix, hundreds of bugs surfaced along the way, including a rediscovery of CVE-2026-56132 in libexpat (Unite.AI).

It is worth noting what kind of finding this is: not a brand-new discovery from scratch, but an independent rediscovery of an already registered vulnerability – found through mathematical reasoning over compiled code, not by running the program. This is how good formal verification works as a bug hunter: it finds inputs that trigger undefined behaviour without anyone having executed them.

The severity of these bugs, including the underflow error in the decompression code and the PDF-reader error mentioned in the coverage, rests on Anthropic's own reporting. There is no independent security assessment in the source material, and this article is not one either. Coverage of CVE-2026-56132 should therefore be read as "Anthropic reports", not as an established fact about severity.

Additional Results: zlib and a Python Interpreter

The project included two tasks beyond the memory-safety proofs, known through Unite.AI's coverage of the release (Unite.AI):

A formal specification of RFC 1950. Anthropic asked Claude to write a formal specification of RFC 1950, the document defining the zlib compression format, and then prove that the Linux kernel's zlib implementation satisfies it – at x86 machine-code level. This is a different kind of guarantee than memory safety: not "the program doesn't crash", but "the program does what the specification says". Such functional correctness proofs have historically been even more expensive than safety proofs, and carrying one out at machine-code level for an implementation in the Linux kernel is, in that sense, arguably more pioneering than the headline result itself.

A Rust-implemented Python interpreter. The team built a Python interpreter in Rust and showed that it matches CPython on 99.95% of more than 1.7 million randomly generated programs. Note the difference in character: this is extensive differential testing with randomly generated programs, not formal proofs. 99.95% is impressive, but 0.05% of 1.7 million is around 850 divergences – and a divergence in an interpreter can range from a cosmetic difference to a security-relevant behavioural difference. The source does not state the severity of the divergences.

What Remains Unproved

Anthropic's own caveats are clear and deserve to be repeated as clearly as the result:

1. The libraries are not vulnerability-free. The company explicitly writes that the result does not mean the libraries are free of vulnerabilities – remaining issues may lie in components outside the trusted computing base or outside the proofs' scope (ChainCatcher). "Trusted computing base" is the key phrase: formal proofs always rest on a foundation of axioms and assumptions that are not themselves proved. The compiler, the machine model, the OS model, and the specifications are not part of what has been verified here.
2. The specification–reality gap. The proof checker cannot confirm that the specifications correspond to reality. A proof that "the program exits normally under these assumptions" is maximally valuable only if the assumptions cover how the software is actually run in production.
3. The "first" claim is Anthropic's own. The company characterises this as the first known large-scale, AI-driven formal verification of production software at machine-code level. That is a pioneering claim that cannot be verified without a systematic review of prior work in the field, and can therefore only be attributed to the company.
4. The partner's role is unclear. Crypto Briefing writes that the work comes from the Frontier Red Team "in collaboration with a company called Theorem Labs" (Crypto Briefing); Unite.AI refers to the collaboration as "Theorem". According to Crypto Briefing, the author list reportedly includes security researchers such as Keane Lucas, Chris Rohlf, Nicholas Carlini, and Nickolai Zeldovich. The exact division of roles between the companies has not been independently verified.

What It Means: The Economics of Verification

The real story is not 123 libraries. It is the seL4 figure: 20 person-years of verification against two person-years of implementation is the ratio that, according to Anthropic, has kept formal verification out of all software that does not control mission-critical systems. If Anthropic is right that Claude could produce comparable Rocq-checked proofs "within weeks", the cost curve for the entire discipline changes – at least for software that can be compiled into single-threaded static binaries on RISC-V.

Three factors temper that conclusion for now:

• The case rests on the company's own evaluation. This is Anthropic showcasing its own model's capabilities, not an independent replication. The appendix figures have not been third-party audited in the source material.
• The assumptions limit transferability. The result says little directly about typical production environments: multi-threaded programs, dynamically loaded code, other instruction-set environments, or interactions with a real kernel rather than a model.
• Reusability is unresolved. The sources do not establish how much of the methodology is project-specific, and how much can be repeated on new libraries without manual specification work.

If the numbers hold up under independent scrutiny, this is nonetheless a significant event: proofs of memory safety at machine-code level for hundreds of entry points in widely used open-source software, produced autonomously by a language model and checked by a proof checker. It is the kind of result that has historically required multi-year academic projects. Knowing exactly what has been proved – and what has not – is the prerequisite for judging whether this is a breakthrough in the economics of formal verification, or an impressive demonstration with a narrower scope than the headlines suggest.