Formal verification: How a proof checker shows that software cannot crash

Formal verification is a way to prove, with mathematics checked by a computer, that a program always obeys a stated rule. Testing tries many inputs and looks for failures. A formal proof covers every possible input at once, within the rule it was given.

The idea is old, but AI is making it cheaper. Anthropic recently used Claude to apply it to 123 open-source libraries, as our news story reported.

Why testing alone leaves gaps

Picture a bridge. Engineers can drive a thousand trucks across it and see that it holds. That tells them about those trucks. A structural calculation tells them about every truck up to a stated weight.

Software works the same way. A fuzzer, a tool that feeds a program huge numbers of random inputs, can run for months and find nothing. Yet one rare input can still crash the program.

Anthropic gives examples from its own work. A decompressor bug was triggered only by inputs of around 20 MB with a rare memory layout. An image decoder bug needed a 64 MB input and over 2 GB of memory. Anthropic says some of these bugs had gone unnoticed for years despite heavy fuzzing.

Three ingredients: A rule, a proof and a checker

Every formal verification has three parts.

• A specification. This is the rule, written in precise mathematical language. An example is “the program never crashes on any input under 64 MB.”
• A proof. This is a long chain of logical steps showing the program meets the rule.
• A proof checker. This is a small program that verifies each step mechanically.

The checker is what makes the approach trustworthy. Nobody has to read a proof of hundreds of thousands of lines. The checker either accepts it or rejects it. According to Anthropic, a reader only has to trust the exact theorem statements, the formal models of the machine, and the checker.

The checker Anthropic used is Rocq, formerly called Coq. Its project site describes it as an interactive theorem prover. People write proofs step by step with commands called tactics, and a small trusted kernel checks the result.

Where the idea came from and what it has proved before

Two projects show what verification looks like at full scale.

The first is seL4, a small operating system kernel. A team led by Gerwin Klein published a 2009 paper at the SOSP systems conference (full name: Symposium on Operating Systems Principles). It reported a machine-checked proof that the kernel’s C code matches its abstract specification. The authors describe it as the first such proof for a complete, general-purpose operating system kernel. The kernel has about 8,700 lines of C and 600 lines of assembly, and the proof used a tool called Isabelle/HOL. The seL4 project page says later work extended the proofs to security properties and to the compiled machine code on some platforms.

The second is CompCert, a compiler that translates C into machine code. Its documentation, credited to Xavier Leroy, says the generated code is semantically equivalent to the source program. This was proved in Coq. CompCert handles a large subset of C, not the whole language.

Both projects took expert teams a great deal of effort. Anthropic frames the scale against seL4, which it says took about 2 person-years to implement and about 20 person-years to verify.

What changed when a language model started writing the proofs

The main cost of verification has been human labor. Proofs are long and fussy, and experts write them by hand. That is a good fit for a model, because the checker catches any mistake. A wrong proof is simply rejected, so the model cannot talk its way past it.

Anthropic’s Frontier Red Team, working with a company called Theorem, had Claude do this for 239 entry points in 123 libraries from Google’s OSS-Fuzz project. Each library’s existing fuzz test became the specification. The proofs are defined over compiled RISC-V instructions, not source code. Anthropic says this removes the compiler from the list of things to trust.

The scale is large. Anthropic reports that Claude wrote roughly a billion lines of Rocq and that about 180 million passed the checker. A typical proof runs about 600,000 lines. Anthropic says the work took a few weeks and that proofs can still take hundreds of millions of tokens.

Claude fixed the bugs it found first and then proved the patched programs exit normally. Anthropic says the attempts surfaced hundreds of bugs. It also reports rediscovering CVE-2026-56132 in libexpat. Some further claims, such as a decade-old logic bug in widely used applications, cannot yet be checked by outsiders.

Why a proof is not the same as bug-free

A proof only covers the rule it was given. Anthropic puts it plainly: “‘Formally verified’ does not mean ‘bug-free.'” It adds that a proof checker cannot tell you whether the specification matches reality.

The limits of the Anthropic work show what this means in practice:

• The proofs assume a single-threaded static binary, a fixed memory budget, a RISC-V CPU, Linux and the musl C library. Many real deployments use x86 or ARM and the glibc library.
• The rule is “does not crash.” That is narrower than full memory safety, because the AddressSanitizer tool used for it does not catch every memory-safety bug.
• Not every entry point was verified, and a caller can still misuse a library.
• The formal models of RISC-V and Linux are themselves things to trust.

The seL4 project page lists similar boundaries. Its proofs rest on assumptions about hardware, and modeling some hardware details is still described there as unsolved.

What to watch as the proofs get cheaper

The first thing to watch is cost. Anthropic reports that Opus 5.5 proved half of 36 small verification tasks using about 40% fewer tokens than Opus 5. If the price keeps falling, verifying everyday libraries becomes realistic.

The second is access. Theorem’s OSS Verify program offers its pipeline free to qualifying open-source projects, and Anthropic released a subset of the proofs and semantics on GitHub. It is withholding proofs that could reveal unpatched bugs.

The third is the specifications. Machine-written proofs shift the hard question from “is the proof right?” to “is the rule the right one?” Better models of real hardware and operating systems, and reviewable specifications, will matter as much as faster provers.