Formal software verification—mathematically proving that code is free of bugs—has historically been impractical for most projects. According to Anthropic research, it took 20 person-years to formally verify the seL4 operating system kernel, despite only two person-years spent implementing it. But frontier large language models are now changing this calculus.
Anthropric and collaborator Theorem demonstrated that Claude can produce formal proofs autonomously across real-world software. The team proved security properties at the assembly code level (RISC-V) in over 100 open-source libraries—described as the first large-scale effort to use AI for formal verification on production software at the assembly level.
The approach converted existing test suites into formal specifications. Developers typically write fuzz tests—automated tools that generate random inputs to find crashes—but these offer no guarantee of covering all possible code paths. By proving that a program will always exit normally without crashing, memory-safety errors, or failed assertions for every input less than 64 MB under specified conditions, Claude eliminated the need for continued fuzzing of those entry points.
The team used over 300 developer-authored entry points from Google’s OSS-Fuzz initiative, which provides continuous fuzz testing for qualifying open-source projects. While proving these properties, Claude also discovered bugs that had eluded detection despite trillions of test runs. The research showed that frontier models can now handle the inherent complexity of reasoning across tens of thousands of assembly instructions—a task historically considered intractable because resulting proofs tend to be many times larger than the original code.
Anthropric notes that formal verification remains far from a complete solution. The proofs applied specifically to single-threaded static binaries with fixed memory budgets on RISC-V CPUs running Linux. The team is publishing a subset of proofs and RISC-V semantics for public verification and reuse. Theorem is also offering to run the same pipeline for other open-source projects and publishing a Claude skill to help developers verify their own code.
As model capabilities improve and more code is formalized, the cost of writing proofs is expected to decrease further. Anthropic encourages developers to explore formal verification with LLMs, particularly those who found it impractical with less capable models.
Key facts
- Claude proved security properties across 123 open-source libraries at the RISC-V assembly code level
- The proofs guaranteed programs would never crash under certain conditions, despite trillions of previous test runs
- Formal verification historically required decades of expert effort; the seL4 kernel took 20 person-years to verify
- The specifications covered single-threaded static binaries with inputs under 64 MB on RISC-V CPUs running Linux
- Anthropic is publishing proofs and RISC-V semantics for public verification and reuse