Anthropic is making a bold claim about one of the oldest promises in computer science. In research published on October 22, the company reports that Claude, working with tooling from the startup Theorem, produced formal proofs that a large batch of real open-source code cannot crash under the conditions its own developers test for. Formal verification has long been reserved for avionics, operating-system kernels and other code where years of specialist labour can be justified. Anthropic argues that language models now make it affordable for ordinary libraries.
The core experiment started from fuzz tests in Google's OSS-Fuzz program. A fuzzer throws huge numbers of mutated inputs at an entry point and flags any input that triggers a crash, including memory errors caught by AddressSanitizer. That search can never be exhaustive. Anthropic instead turned each harness into a mathematical statement: the compiled program never crashes for any input smaller than 64 MB. Claude then had to prove it in the Rocq proof assistant, using Theorem's formal models of RISC-V instructions and Linux process behaviour.
According to the post, Claude finished proofs for 239 entry points across 123 libraries over a few weeks. Together the proofs run to roughly 180 million lines of Rocq code, and a typical one stretches to about 600,000 lines for a binary of about 18,000 instructions. Nobody needs to read them, Anthropic says, because the Rocq kernel checks every step mechanically. What users must trust is narrower: the RISC-V and Linux models, the exact theorem statements and the checker itself. The guarantees also carry assumptions, among them that the program is a statically linked, single-threaded binary running within a set amount of memory.
The proof attempts doubled as a bug hunt. Whenever Claude hit a reachable crash, it patched the code and carried on, and Anthropic says the process surfaced hundreds of bugs. Examples include an out-of-bounds write in a bundled decompressor that appeared only with inputs near 20 MB, an image-decoder read error needing a 64 MB file and more than 2 GB of memory, and a fresh rediscovery of a known libexpat vulnerability. Fuzzers, which usually cap inputs around 1 MB, would rarely reach such cases.
Side projects pushed further. Claude wrote a formal specification of the zlib format defined in RFC 1950 and proved that the Linux kernel's zlib code meets it, this time on x86 binaries. It built a Rust interpreter for a large slice of Python, proved it against an academic model of CPython with the Verus tool, and matched CPython on 99.95% of 1.7 million random programs. An effort on a widely used PDF reader turned up as many security bugs in a week as are normally reported in a year, the company says.
Cost remains the obvious brake. Individual proofs can consume hundreds of millions of tokens. Anthropic reports that Claude Opus 5.5 needed roughly 40% fewer tokens than its predecessor, Opus 5, to solve half of a 36-task verification benchmark, and that agents sharing a workspace of reusable proofs cut token use by a further 17%. Theorem plans to offer the pipeline to other open-source projects and has published a roadmap that targets the Nix ecosystem, including glibc, OpenSSL and cURL.
Anthropic is releasing the new trusted models, complete proofs for harnesses that needed no patching and specifications for those it could not prove, while holding back anything that might expose unpatched flaws. It also stresses that a proof is only as good as its specification: if the model of the machine is wrong, verified code can still fail. Independent researchers have not yet had time to audit the release, so the scale figures remain the company's own account for now.