Anthropic and Theorem Partner: Claude First to Prove Zero Crashes in RISC-V Assembly Across 123 Libraries

On October 22, 2026, Anthropic and Theorem jointly released research in which Claude generated approximately 180 million lines of Rocq proof code for 123 real open-source libraries included in Google OSS-Fuzz, mathematically proving at the RISC-V assembly level that 239 entry points “do not crash under any input.”

The Facts

The research shows that under assumptions of single-threaded static binaries, a fixed memory budget, a RISC-V CPU, and a Linux OS, Claude proved that programs always exit normally without triggering memory safety errors or assertion failures, with an input cap of 64 MB. The process also found several hidden vulnerabilities that trillions of fuzzing runs had still not triggered. The research released part of the proof code and the RISC-V and OS semantics; Theorem also offers the same pipeline for other open-source projects and released a Claude skill to help developers get started.

Mechanism Breakdown

Formal verification first requires transforming code into a mathematical model and then proving that it always follows specified safety rules. If a proof fails, it points to a vulnerability that may violate the rules; after eliminating the cause, the process is repeated until a proof is obtained showing no rule-violating vulnerabilities. Traditionally, proof code far exceeds the original code in volume and requires highly specialized skills; for example, the seL4 kernel implementation took only 2 person-years, while verification consumed 20 person-years. This time, Claude autonomously generated proofs, pushing the process toward a mass-producible automated pipeline.

Industry Impact

This move extends formal verification from mission-critical applications only (such as Airbus avionics code) to more real open-source libraries. The potential to reuse and modify proofs is expected to amortize verification costs for subsequent codebases. Theorem’s pipeline service and skills release provide developers with a direct entry point. As model capabilities improve, formal verification is expected to become a routine part of secure software development.

Strategic Assessment

(Analysis, not fact) This work tests the model’s long-horizon reasoning, code understanding, and logical proof capabilities, mirroring existing quantitative evaluations of code execution and complex reasoning. Beyond lab scores, AI’s real engineering reliability is emerging in a verifiable way. If models continue to improve, lower proof costs will accelerate the standardization of security assurance, but fully eliminating all possible vulnerabilities still requires further exploration.