Anthropic Says Claude Proved Security Properties Across 123 Libraries

Anthropic published research on October 22, 2026, reporting that Claude produced machine-checked formal proofs of security properties at the RISC-V assembly code level for 239 fuzz-test entry points across 123 open-source libraries, in a collaboration with Theorem.

According to Anthropic, Claude patched the bugs it found and then proved the programs will always exit normally without triggering memory-safety errors or failing assertions, for every input under 64 MB and every modeled Linux operating system response and memory layout. The proofs assume the program runs as a single-threaded static binary with a fixed memory budget on a RISC-V CPU using Linux. Anthropic said the proofs comprise about 180 million lines of Rocq, with a typical proof running about 600,000 lines to cover binaries with a median length of 18,000 RISC-V instructions. The company said that, to its knowledge, this is the first large-scale effort to use AI to apply formal verification to production software at the assembly code level.

A subset of the proofs, along with the RISC-V and operating-system semantics behind them, is being published on GitHub. Anthropic said it is also releasing the trusted components built for the project that are not already public, complete proofs for fuzz tests that required no patching, and specifications for fuzz tests it could not prove, while withholding proofs that could reveal an unpatched bug.

Turning Fuzz Tests Into Formal Proofs

The approach converts each library’s existing compilable fuzz test into a formal specification encoding one rule: the test never crashes for any input under 64 MB. The specification is defined over compiled RISC-V instructions using Theorem’s formal semantics of the RISC-V instruction set and Linux processes, and the Rocq proof checker verifies each finished proof against the specification. Anthropic says this leaves only three components developers need to trust: the formal models of RISC-V and Linux processes, the exact theorem statements, and the Rocq checker itself.

Anthropic said it applied this process to hundreds of projects in Google’s OSS-Fuzz initiative, which provides continuous fuzz testing for qualifying open-source projects and automatically instruments C and C++ programs with AddressSanitizer, a tool that crashes a program whenever memory is accessed improperly. An appendix dated October 22, 2026, spells out the full theorem proved: for all inputs under 64 MiB and all memory layouts, neither the ASan-instrumented binary nor the plain binary faults, aborts, or exhibits unmodeled behavior, and both produce identical read and write traces, exit behavior, and final file-system state.

The appendix states that Claude wrote around one billion lines of Rocq during the effort, of which about 180 million lines passed the proof checker; cJSON’s 391-line parser entry point received a 630,000-line proof, while fftw3, with 51,000 lines linked in, received a 480,000-line proof. Because Claude was permitted to patch code before completing a proof, Anthropic said it penalized patches, offered extra credit for proving which inputs a patch changed, and logged and audited patches to discourage reward hacking.

Bugs Discovered During Proof Attempts

Anthropic reports that attempting the proofs surfaced hundreds of bugs, many of them ones a fuzzer would be unlikely to find. While proving one library’s entry point, Claude found a counter underflow in a decompressor that caused an out-of-bounds write, but only on inputs of around 20 MB with one rare, specific layout. Other finds included an out-of-bounds read in an image decoder requiring a 64 MB input and more than 2 GB of memory, an out-of-bounds read requiring a particular sequence of calls across two handles to the same file, and a rediscovery of CVE-2026-56132 in libexpat, which required deeply nested input.

Claude also found logic bugs that never crash, including a restriction on which files an application can load that is not always enforced. Anthropic said verification attempts on several widely used critical applications uncovered a previously unknown logic bug that had been latent for more than a decade, and that during an effort to verify a widely used PDF reader, it found as many security bugs in one week as are typically reported in a year.

Additional Experiments and Efficiency Findings

Beyond OSS-Fuzz, Anthropic asked Claude to write a formal specification of RFC 1950, the technical document defining the zlib compression format, and then prove that the Linux kernel’s zlib implementation correctly implements it. Claude proved the x86-compiled binary directly, using Claude-generated formal semantics of the x86 instruction set, and Anthropic said it repeated the process for half a dozen other widely used libraries, finding minor, unexploitable corner-case bugs that are being filed upstream. The company also reported that generating the x86 semantics identified hundreds of mistakes in official reference documentation and a smaller number of bugs in the hardware itself, and that single-stepping through the semantics can boot an Ubuntu userspace on a Linux kernel.

In another experiment, Claude built an interpreter for a large subset of Python in Rust and proved, using the Verus verification tool, that it adheres to the CPython semantics outlined in an academic paper. The technical appendix states that all 17 tiers of the interpreter were proved, with the theorem holding that “Whenever the interpreter returns a result, that result is the one the formal semantics prescribes.” Anthropic said empirical testing over 1.7 million randomly generated Python programs found behavior identical to CPython in 99.95% of tests; of seven deliberately injected bugs, five survived random testing while all seven broke the proof.

To measure efficiency, Anthropic built 36 small verification tasks by shrinking real OSS-Fuzz entry points, producing programs of 283–2,491 instructions with inputs limited to 64 bytes and AddressSanitizer replaced by a “mini-ASan” runtime of about 100 instructions. Anthropic reports that Opus 5.5 proves half of the tasks with about 40% fewer tokens than Opus 5. Anthropic also reports that agents allowed to copy each other’s proofs in a shared workspace needed 17% fewer tokens than agents working alone, that some succeeded after previously failing solo, and that agents working alone failed to complete two of the proofs. The company said the same reuse effect appeared at scale during the OSS-Fuzz effort, where agent teams copied finished proofs and adapted them because much of each proof covers shared C runtime and AddressSanitizer initialization code.

Stated Limitations and the OSS Verify Program

Anthropic states that the proofs do not mean the libraries are bug-free: remaining bugs could lie within the trusted components or outside the proofs’ scope. The proofs cover single-threaded static RISC-V binaries linked against musl libc, while most users run these libraries on x86 or ARM and dynamically link against glibc, and AddressSanitizer does not detect all memory-safety bugs. The company said it expects these limitations to become tractable as models improve.

Theorem is offering the same pipeline to qualifying open-source projects for free through its OSS Verify program. Enrollment works by pull request that adds project.yaml, Dockerfile, and build.sh files to the program’s repository, and Theorem says it reviews projects along lines similar to OSS-Fuzz, prioritizing widely used critical infrastructure. According to Theorem, maintainers receive a Rocq proof, checked by the Rocq kernel, that each fuzz target does not crash on any input up to 64 MiB; bugs found during the proof effort are privately disclosed to maintainers by email with no disclosure deadline, and proofs can take multiple days to produce. Theorem’s roadmap targets verifying the entirety of the Nix ecosystem, including critical infrastructure such as glibc, OpenSSL, and cURL.