Anthropic says Claude makes formal verification feasible at scale

Anthropic says Claude has helped prove security properties in more than 100 open-source software libraries, showing how large language models could make formal verification practical beyond a handful of mission-critical systems. The company’s collaboration with formal-methods specialist Theorem used Claude to generate mathematical proofs at assembly-code level, while independent tools checked whether those proofs held. ¹²

The project focused on 123 real-world libraries and used existing test suites as the starting point for formal specifications. Anthropic says Claude generated proofs for programs compiled to RISC-V and demonstrated that they would avoid memory-safety errors, failed assertions or abnormal exits under defined assumptions. Those assumptions matter: the work models single-threaded static binaries, a fixed memory budget and inputs smaller than 64 MB on a RISC-V processor running Linux. ¹

That is not the same as proving that a library is universally bug-free on every computer. Instead, it is a mathematically checked guarantee about particular behaviours in a carefully described environment. Anthropic is explicit that the result is a step towards broader verification, not a complete answer to software security. ¹

The process also surfaced bugs that conventional testing had missed. The Decoder reports that Claude produced roughly 180 million lines of proof code in a few weeks and helped identify hundreds of bugs, including problems that appeared only with unusual input sizes or particular sequences of operations. The proofs were checked by Rocq, an independent proof assistant, rather than accepted merely because Claude claimed they were correct. ²

Why formal verification matters

Software testing runs a selection of inputs and watches what happens. Formal verification starts with a specification and attempts to prove that every input within the stated model satisfies it. That can provide much stronger confidence, but traditionally it has required specialist teams and enormous effort. Anthropic cites the seL4 microkernel, which took about 20 person-years to verify despite being much smaller than the software stacks used by most organisations. ¹

Claude changes the economics by taking on the repetitive proof-writing work. Theorem’s research argues that reusable proofs for shared libraries could eventually support a much larger verified software stack, including dependencies used by critical infrastructure. That remains a roadmap rather than a finished product, but the underlying idea is straightforward: prove an important component once, then let software built on it reuse the result. ³

There are limits beyond the model assumptions. Formal verification can only prove the specification that humans chose, and the specification may not capture every real-world requirement. Developers must also trust the hardware, operating system, compiler and proof checker supporting the process. Anthropic notes that the work leaves room for reward-hacking risks, where an AI could make a theorem easy to prove by changing the programme in an unacceptable way, so patches and proofs still need auditing. ¹

Our opinion

This is one of the more credible uses of AI in software engineering because it puts the model inside a chain of checks rather than treating fluent code generation as evidence of correctness. A proof assistant can reject a bad proof, and the narrow assumptions make it possible to say exactly what has — and has not — been demonstrated.

The danger is the headline version of the result. “AI proves code correct” sounds universal, while the actual achievement is conditional: Claude helped generate proofs for defined properties, architectures and input limits. That is still valuable. If the method scales without hiding its assumptions, it could turn formal verification from an elite safety technique into a routine layer for important libraries. The proof is not that AI has solved software reliability; it is that AI may finally make stronger guarantees affordable enough to use more often. ¹²