Definition
Formal verification is Formal verification is the use of mathematical proof, checked by software, to show that a program or system always meets a precise specification, such as never crashing on any valid input.
Formal verification means proving, with mathematics, that a piece of software does what its specification says. Ordinary testing shows that a program worked on the cases you tried. A proof shows it works on every case the specification covers.
The proof is not a paper argument. It is written in a language a proof checker (software such as Rocq, Lean or Isabelle) can verify step by step. If the checker accepts it, the result holds, as long as the specification and the checker's assumptions are right.
You start with two things: the code (or a model of it) and a specification, a precise statement of what it must do. A specification might say "this function never reads outside its buffer" or "this decompressor never crashes on any input under 64 MB." Then you build a proof that the code satisfies the statement, and the proof checker confirms every step.
The hard part is effort. Real proofs can run to hundreds of thousands of lines, and writing them has historically needed rare experts working for months or years. That is why formal verification has mostly been used where failure is very costly, such as operating system kernels, compilers, cryptography and aerospace.
Verified does not mean bug-free. A proof is only as good as its specification. If the specification misses something, the code can satisfy it and still do the wrong thing. Proofs also rest on assumptions about the hardware, the operating system and the compiler. If those assumptions do not match reality, the guarantee weakens.
Writing proofs is the sort of long, checkable, trial-and-error task that AI models can grind through, because a proof checker gives an unambiguous yes or no on every attempt. That makes it a natural target for AI systems, and research groups have begun using models to produce proofs at scales that were impractical by hand.
A checker also guards against a weakness of AI-written code: a model cannot talk the checker into accepting a bad proof, though it can still reward hack by weakening the specification, so the specification needs human review.
Fuzzing and ordinary tests sample inputs and look for failures. Formal verification reasons about all inputs at once. The two work well together: fuzzing is cheap and finds bugs fast, and verification can close the gap by showing a class of bug cannot occur. Evals play a similar role for AI models, but they too only sample.
No. It proves the code meets its specification under stated assumptions, so a flaw in the specification or the assumptions can still leave bugs.
Testing checks sample inputs and can miss rare cases. Formal verification proves a property for every input the specification covers.
Anthropic and Theorem say Claude wrote machine-checked proofs that 239 fuzz entry points across 123 open-source libraries never crash on inputs under 64 MB, finding hundreds of bugs on the way. AI is finally doing the slow, boring half of security.