Table of Contents
Anthropic and Theorem have used Claude to produce machine-checked proofs of no-crash properties for 239 testing entry points across 123 open-source libraries, applying formal verification directly to compiled software rather than its source code.
The research converts existing fuzz tests into mathematical specifications, then has Claude write proofs that the resulting RISC-V binaries cannot crash on covered inputs. During the work, Claude also found and patched hundreds of bugs, including failures requiring unusually large inputs that conventional fuzzing was unlikely to discover.
Anthropic announced the results after a few weeks of work with Theorem. The company calls it the first large-scale AI effort to formally verify production software at the assembly-code level. The result concerns specific executable paths and security properties, not a blanket certification of every function in the 123 libraries.
Turning Fuzz Tests Into Mathematical Claims
Fuzzing repeatedly feeds generated or mutated inputs into a program to look for failures. Developers supply an entry point, such as a function that parses an image or decompresses data, and a testing engine searches for inputs that make it crash. The search can run for years without exhausting all possible inputs.
Formal verification changes the task from finding a failing example to proving that no covered example can fail. A specification defines the property to be established; a proof checker determines whether the mathematical argument satisfies it.
For this experiment, the researchers reused tests from Google's OSS-Fuzz project. Those tests already encode properties that maintainers care about, including assertions that crash when a requirement is violated. AddressSanitizer adds runtime checks that also turn detected memory errors into crashes.
Theorem's formal models describe RISC-V instructions and Linux process behavior. Compiling each library and its fuzz test into a RISC-V executable lets the pipeline generate a specification about the instructions the binary will execute. Claude then writes a proof, and the Rocq proof kernel checks it.
The main experiment targeted inputs below 64 MB, across modeled Linux responses and memory layouts. Its assumptions include single-threaded, statically linked RISC-V binaries, a fixed memory budget, and musl libc. The resulting proofs totaled about 180 million lines of Rocq. A typical proof ran to roughly 600,000 lines, while the median binary contained about 18,000 RISC-V instructions.
Rocq checks the proof, so that volume does not require manual code review. Developers still need to trust the theorem statements, the processor and operating-system models, and the proof checker. The guarantees apply to the covered binaries and behavior, rather than automatically carrying over to an x86 or ARM build with different linking or runtime assumptions.
Proof Attempts Exposed Hard-to-Reach Bugs
When Claude encountered a bug that prevented a proof, it could patch the program, regenerate the specification, and continue. Anthropic penalized patches, rewarded narrowly scoped behavioral changes, and logged and audited modifications to discourage shortcuts that would satisfy the theorem by removing useful functionality.
One decompressor contained a counter underflow that could cause an out-of-bounds write, but triggering it required an input of about 20 MB with a rare layout. An image decoder had an out-of-bounds read requiring a 64 MB input and more than 2 GB of memory. Another failure depended on a particular sequence of operations across two handles to the same file.
Claude also rediscovered CVE-2026-56132 in libexpat, involving deeply nested input, and noticed a logic error in a feature intended to restrict which files an application could load. That restriction was not always enforced, even though the failure did not cause a crash.
The proofs could establish higher-level behavior when tests expressed it as an assertion. An LZO compression test checks that compressing and then decompressing data recovers the original input. Proving that test cannot crash establishes the roundtrip property within its scope.
In the cpp-httplib work, ruling out a stack overflow required Claude to prove that libc++'s red-black tree rebalancing keeps tree depth logarithmically bounded. This connects a low-level no-crash goal to the correctness of a data structure used by the program.
Coverage still follows the test harness. Code an entry point cannot reach is outside its proof, and sanitizer checks do not detect every memory error. These are properties of the specification being proved, so choosing useful tests remains part of the verification work.
Extending Verification Beyond Crash Detection
Anthropic also tested whether Claude could verify software against an independently written format specification. Claude formalized RFC 1950, which defines the zlib compression format, and proved that the Linux kernel's zlib implementation matched it at the x86 binary level, using model-generated and extensively tested x86 semantics.
The team repeated that approach for half a dozen other widely used libraries. Anthropic reports minor, unexploitable corner-case bugs that are being filed upstream.
In a separate experiment, Claude built an interpreter for a large subset of Python in Rust and used Verus, a Rust verification tool, to prove adherence to specified CPython semantics. Empirical testing on more than 1.7 million randomly generated Python programs produced behavior identical to CPython in 99.95% of cases; Anthropic attributed the remaining differences to known corner cases.
Verification attempts on other widely used applications also uncovered a logic bug that had persisted for more than a decade. In work on a PDF reader, Anthropic says the team found as many security bugs in one week as the application typically has reported in a year.
The work complements Anthropic's Cyber Mission and opt-in OSS Scanner, which use AI to identify vulnerabilities. Here, the additional output is a checkable proof of a defined property after any necessary repairs.
