Anthropic uses Claude to write formal proofs for 123 open-source libraries

Anthropic says large language models can now write formal mathematical proofs that a program contains no bugs of a certain kind, at a scale that was previously impossible. In a project with the startup Theorem, the company used its Claude models to prove security properties for 123 open-source software libraries, working directly on the compiled assembly code rather than the original source.

Formal verification translates a program into a mathematical model and proves it always follows a defined set of rules. Historically that work has taken years: building the seL4 operating system kernel took two person-years, but verifying it took 20, according to Anthropic. Because of that cost, the technique has mostly stayed limited to mission-critical systems such as Airbus avionics software.

Anthropic and Theorem instead used existing fuzz tests, automated checks that feed huge numbers of random inputs into a program to find crashes, and turned them into formal specifications. A spec built this way states that a given entry point will never crash on inputs smaller than 64 megabytes. Over several weeks, Claude proved that claim for 239 entry points across the 123 libraries, assuming each program runs as a single-threaded, fixed-memory binary compiled for RISC-V chips under Linux. Anthropic says the resulting proofs add up to about 180 million lines of code in the Rocq proof language, with a typical proof running to roughly 600,000 lines to cover a binary with a median length of 18,000 RISC-V assembly instructions.

Bugs that fuzzing missed

While writing the proofs, Claude also found and fixed bugs in the libraries that fuzz testing, despite trillions of runs, had not caught, according to Anthropic. The company says a separate proof checker called the Rocq kernel verifies that each proof actually satisfies its stated specification, so developers do not need to read the proof code by hand. What they do need to trust, Anthropic says, are the formal models of RISC-V chip behavior and Linux processes, plus the exact wording of what was proved.

Anthropic is careful to note the limits of the claim. The proofs cover crashes and memory-safety failures, not every kind of bug, and they apply only under the stated assumptions about how the program runs. A library judged free of crashes under this method could still contain bugs outside that scope, or flaws hidden in the trusted RISC-V, Linux, or Rocq models themselves.

Anthropic is publishing a subset of the proofs, along with the RISC-V and operating system models used to build them, so outside researchers can check the work. Theorem is offering to run the same verification pipeline on other open-source projects and is releasing a Claude skill meant to help developers start verifying their own code.

What happens next depends on how the approach holds up outside this initial batch of libraries. Anthropic says the cost of writing proofs should keep falling as models improve, and that proofs built for one codebase should become easier to reuse or adapt for others. Independent review of the published proofs, and of the trusted RISC-V and Linux models underneath them, will show whether the guarantees hold.