Anthropic and Theorem use Claude to prove crash-freedom in 123 open-source libraries

Anthropic said on Oct. 22 that, working with Theorem, it used Claude to write formal proofs at the RISC-V assembly level for 123 open-source libraries.1

Anthropic said formal verification has historically required years of expert effort, and that LLMs can now produce such proofs at large scale; as an example it cited the seL4 kernel, which took two person-years to implement and 20 person-years to verify.1 To define what "correct" means for the open-source libraries it sought to prove, Anthropic said it automatically converted their preexisting compilable test suites into a spec encoding the rule "this test suite always passes," using a general model of executing RISC-V-compiled binaries on Linux; for this project it started with fuzz tests, and the resulting spec says the fuzz test will not crash for any input less than 64 MB.1

Claude proved the programs always exit normally, with no memory-safety errors or failing assertions, for every input under 64 MB and every modeled Linux response and memory layout, according to Anthropic.1

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.1

Over a few weeks, Claude patched the bugs it found and proved no crashes on any input up to 64 MB for 239 entry points across 123 OSS-Fuzz libraries, and Anthropic said it found bugs that had eluded detection for years despite trillions of test runs.1

According to Anthropic's appendix, Claude wrote about one billion lines of Rocq proofs, of which about 180 million were part of proofs that passed the checker; a finished proof runs to about 600,000 lines, and checking one can take 30 minutes to several hours of CPU time.2