What is formal verification? How it differs from testing and fuzzing, and what a proof does not promise

In short

Formal verification proves, with mathematics checked by a program, that a piece of software meets a precise written rule for every possible input, not just the ones someone tried. Testing and fuzzing look for bugs by running the code; verification shows a class of bugs cannot exist, within the assumptions of the model it uses. It is not a promise that software is "bug-free": the proof is only as good as the rule you wrote and the model of the machine you proved it against. It has been expensive for decades, and this week's Anthropic and Theorem result is the latest claim that language models are changing that cost.

Three ways of asking "does this code work?"

Testing runs the program on chosen inputs and checks the answers. A test suite proves one thing: for those inputs, the code gave the expected result. It says nothing about the inputs nobody thought of.

Fuzzing automates the choosing. A fuzzer feeds a program large numbers of mutated inputs and watches for crashes or sanitizer errors. Google's OSS-Fuzz runs this continuously for many open-source projects. A fuzz test is a small function: take some bytes, call the library, and treat any crash as a bug. In Anthropic's description, fuzzers typically stay near 1 MB inputs, which is why some bugs, such as ones that only appear with a 20 MB input in a rare layout, are unlikely to be found that way.

Formal verification does not run the program on samples. It turns the program, and a statement of what it must satisfy, into mathematical objects, and a proof shows that the statement holds for all inputs in a stated range. Anthropic's study proved that selected programs never crash, trigger no memory-safety error and fail no assertion for any input under 64 MB. A fuzzer, however long it runs, only ever covers a sample of that space.

What a proof actually contains

Three ingredients, and each is a place where things can go wrong.

1. The program, in some form the prover understands. It can be source code, but in Anthropic's study it was the compiled machine code, as RISC-V instructions. Proving things about the binary means the compiler is no longer something you have to trust.
2. A model of the machine: what each instruction does, and how the operating system responds to system calls. Theorem built a formal model of RISC-V and of a Linux process for this purpose. The authors say Claude also generated models of other instruction sets, such as x86, and that the work revealed hundreds of errors in official reference documentation.
3. The specification: the rule being proved. "Never crashes" is one. "Decompressing what you compressed gives back the original" is another. "Matches this RFC" is a third; Claude wrote a specification of RFC 1950, the zlib format, and proved that the Linux kernel's zlib code meets it.

The proof itself is written in a proof assistant, a program in which every step must be justified. Anthropic's study used Rocq (a long-established proof assistant, formerly known as Coq). The key idea is that a small checker re-verifies every step. You do not need to trust whoever (or whatever) wrote the proof, only the checker.

A toy example: why "for all inputs" matters

Take a function that returns the absolute value of an integer. Tests with 5, -5 and 0 pass. A reader sees nothing wrong. But in a typical 32-bit signed integer, the most negative value, -2,147,483,648, has no positive counterpart, so negating it overflows. This is a well-known property of two's-complement arithmetic. A test suite finds it only if someone thinks to try that exact value. A proof attempt of "the result is never negative" fails on that case and shows the counterexample. The failed proof is the useful output: it tells you where the code and the rule disagree.

This is the pattern Anthropic describes at scale. Failed proofs pointed at likely bugs, and the authors report hundreds of them, among them an underflow in a decompressor leading to an out-of-bounds write and a rediscovery of CVE-2026-56132 in libexpat.

Why it was rare, and why it might not be

Verification has been rare because of cost. The post cites the seL4 microkernel: about two person-years to implement, about 20 person-years to verify. Most of that time went on writing proofs by hand. Its main uses have been in places where failure is very expensive, such as the Airbus avionics code the post mentions.

The new claim is that models can now write the proofs, because the checker removes the risk of a wrong one. Anthropic reports 239 entry points in 123 libraries proved in a few weeks, with typical proofs around 600,000 lines of Rocq. Some of the economics are as notable as the headline: agents that could copy each other's proofs used 17% fewer tokens than agents working alone, and teams reused finished proofs between programs, because much of each proof covers shared setup code. That is how verification could become cheaper per library as the pool of proved code grows, in the way the authors compare to the Lean library Mathlib, which has nearly 300,000 theorems from over 700 contributors.

What a proof does not tell you

"Formally verified" is a precise statement, and the precision is the point. Read it as: this property holds, under this model, assuming these things about the machine. The things to check:

• Is the property the one you care about? A proof that a parser never crashes says nothing about whether it parses correctly. One of Anthropic's example bugs, a file-restriction feature that was not always enforced, never crashes at all and would pass a no-crash proof.
• Does the model match reality? The study's proofs cover single-threaded static RISC-V binaries linked against musl libc. Most real deployments use x86 or ARM and often dynamically linked glibc, and the authors say closing that gap needs accurate models of those systems.
• Is everything covered? Not every entry point was verified. The sanitizer used as the crash oracle does not catch every memory-safety bug, and callers can still misuse a library.
• What is trusted? The semantic models, the exact theorem statement, the proof checker, and underneath them the hardware, the operating system and the compiler the checker itself runs on.
• Could the prover cheat? The authors warn that a model could make a theorem easier to prove by rewriting the program so that it never crashes. They penalised patches, gave extra credit for proving which inputs a patch changes, and audited the patch logs.

The public repository illustrates the distance between demonstration and coverage: it lists 20,164 statements across 427 OSS-Fuzz projects, and counts 138 proved and 19,797 open, while its README notes that its Linux process model is "best effort and not complete".

A short glossary

• Entry point: a function a program or library exposes to the outside, such as the function a fuzz test calls with raw bytes. Anthropic's count of 239 is in entry points.
• Specification: the written rule the code must satisfy, stated precisely enough that a machine can check a proof of it.
• Theorem statement: the specification combined with the program and the machine model into one claim that a proof assistant can accept or reject.
• Proof assistant / proof checker: the program, here Rocq, that accepts a proof only if every step follows from the previous ones. The checker, not the author, is what you trust.
• Sanitizer: a compiler feature (AddressSanitizer, UndefinedBehaviorSanitizer) that makes a program stop when it touches memory it should not. In the study, "never crashes" means "never trips the sanitizer".
• Semantics (of an instruction set): the formal description of what each machine instruction does. Errors here undermine every proof built on top, which is why the authors flag it as part of the trust base.
• Reward hacking: a model achieving a goal by exploiting the way it is scored, for example by changing the program instead of proving it.

How to use this knowledge

If you build software, you do not need to write a proof to benefit. Three habits follow from the ideas above:

1. State the property. Even for ordinary tests, writing "for all inputs, X holds" is a stronger design exercise than listing examples. Property-based testing tools take that statement and generate inputs for it.
2. Fuzz what parses untrusted input. The fuzz test is also, as Anthropic's pipeline shows, the starting point for a proof, so it is never wasted work.
3. Read the claim, not the label. When a vendor says "formally verified", ask what property, against which model, covering which code. A good answer names all three.

Where to go next

Read the Anthropic post for the full study and its limits, and browse the proofs repository to see what a statement and a machine-checked proof look like. The Rocq standard library page is a starting point for the proof assistant itself. For the security side, our article on how Anthropic used Claude to cut OpenSSH's pre-login attack surface shows the same models used offensively and defensively.

Sources

• Anthropic Frontier Red Team with Theorem: LLMs are making formal software verification feasible at a much larger scale (primary source)
• theorem-labs/oss-verify-proofs on GitHub
• Rocq standard library package page
• audiotale.net: Claude proves 239 open-source entry points crash-free
• audiotale.net: Anthropic used Claude to cut OpenSSH's pre-login attack surface