Anthropic says Claude has done something that once took human experts years: it has written machine-checked mathematical proofs that real production software cannot crash. In research published on October 22, Anthropic’s Frontier Red Team and the startup Theorem report that Claude proved security properties at the assembly code level for 239 entry points across 123 open-source libraries drawn from Google’s OSS-Fuzz project, generating roughly 180 million lines of proof in the Rocq proof assistant.
Anthropic calls the project, to its knowledge, “the first large-scale effort to use AI to apply formal verification to production software at the assembly code level.” Along the way, Claude also found and patched hundreds of bugs — flaws that had escaped years of fuzz testing, including a rediscovery of CVE-2026-56132 in libexpat. The proofs, along with Theorem’s RISC-V and Linux operating-system semantics, are being released publicly so anyone can check them.
From fuzz tests to machine-checked proofs
The team started from Google’s OSS-Fuzz project, which provides continuous fuzz testing for open-source software. In fuzz testing, developers write an entry point into their code, and a testing engine throws enormous numbers of semi-random inputs at it, hoping one causes a crash. Fuzzing can never try every input, so it offers no guarantee that a bug won’t be found later.
Claude turned each fuzz test into a formal specification: the statement that the test “won’t crash for any input less than 64 MB,” defined over the compiled RISC-V machine code of the library. It then wrote a proof of that statement, which the Rocq proof checker verifies mechanically. A typical proof runs to about 600,000 lines of Rocq for binaries with a median length of 18,000 RISC-V instructions.
The bugs hiding where fuzzers never looked
The proof process surfaced hundreds of bugs that fuzzing was unlikely to ever find, because fuzzers mutate small inputs — typically capped at 1 MB — and lean on code coverage to guide them. Claude’s bugs lived outside those assumptions. In one library it found a counter underflow in a decompressor that led to an out-of-bounds write, but only on inputs of around 20 MB with one rare, specific layout. An image decoder contained an out-of-bounds read that required a 64 MB input and over 2 GB of memory. Another library needed a particular sequence of calls across two handles to the same file.
Claude also found logic bugs that never crash at all: while proving one library memory-safe, it noticed that a feature for restricting which files an application can load isn’t always enforced. In a widely used PDF reader, the team says it surfaced as many security bugs in one week as are typically reported in a year.
The project also ran side experiments beyond memory safety. The team proved that the zlib implementation in the Linux kernel conforms to the RFC 1950 specification at the x86 binary level, and built a Rust interpreter covering a large subset of Python with 99.95% behavioral consistency against CPython across more than 1.7 million randomly generated programs.
What the proofs do not promise
Anthropic is careful about what “formally verified” means here: it does not mean bug-free. The proofs assume the program runs as a single-threaded static binary with a fixed memory budget on a RISC-V CPU under Linux — while most people run these libraries on x86 or ARM and dynamically link them against glibc. ASan, the sanitizer used to instrument the code, doesn’t detect all memory-safety bugs, and the team didn’t verify every entry point for each library.
Proving is also expensive: some proofs take hundreds of millions of tokens. But Anthropic’s conclusion is that the economics have flipped — formal verification “will soon be as practical as fuzzing is today for almost all production software,” and the cost of writing proofs falls as models get more capable.
Why it matters
For Anthropic, this research does double duty. The company is already using Claude’s security research as evidence for its own safety story, and proving properties of the open-source libraries that underpin nearly all software would give AI labs, cloud providers and enterprises a new tool for securing supply chains. If AI agents are increasingly able to find and exploit vulnerabilities in production code, the only defense with a mathematical guarantee is proof — and this project argues proof can now be generated at machine scale.
It also moves Claude deeper into the developer-tooling arena. Theorem is offering to run the same pipeline for other open-source projects and has published a Claude skill to help developers get started verifying their own code — a natural extension of the coding-agent business where Claude Code already competes.
Background
Formal verification has historically been the province of the most safety-critical code — the seL4 operating-system kernel took two person-years to build and 20 to verify. Anthropic’s Frontier Red Team has been publishing applied security research through 2026, and recently opened its models to outside red-teamers as part of its argument that AI progress and AI safety can be developed together.
Source: Anthropic — LLMs are making formal software verification feasible at a much larger scale ; AI Weekly
0 Comments