What Is Formal Verification in AI?

Formal verification in AI means proving, mechanically, that a statement holds for every possible input, rather than checking it against a sample of inputs. A test suite tells you the code worked on the cases you thought of. A formal proof tells you no counterexample exists at all. The difference matters because AI systems now produce both the code and, increasingly, the proofs about it.

The distinction is old. What changed in 2026 is that a model produced a proof large enough that no human team had managed it first.

What formal verification actually proves

A proof assistant such as Lean is a programming language whose type checker doubles as a referee. You state a claim, you supply a chain of reasoning, and the checker either accepts every step or rejects the whole thing. There is no partial credit and no persuasive writing. A proof that compiles is correct relative to the axioms it assumes.

That last clause is the whole game. Formal verification never proves something is true in the world. It proves that a conclusion follows from stated assumptions. If you assume the wrong thing about your database, a verified program will faithfully do the wrong thing.

Three properties follow:

• It is exhaustive. The claim covers all inputs, including the ones nobody imagined.

• It is checkable by machine, cheaply, forever. Rechecking a proof costs seconds.

• It is expensive to produce. Writing the proof is usually far harder than writing the code.

That last point is why formal verification has stayed confined to compilers, cryptographic protocols, aerospace control, and chip design. The cost only pays for itself when failure is catastrophic.

The Fermat's Last Theorem proof, and what it showed

On 4 September 2026 Anthropic published an account of Claude formalizing Fermat's Last Theorem in Lean. Working largely autonomously across 11 days, the system produced an end to end machine-checked proof following a simplified version of the Wiles argument. The result runs to roughly 13 million lines of Lean, more than five times the size of Mathlib, the community library it builds on, and proves about 29,500 intermediate theorems along the way. Lean accepted it using only its three standard axioms.

Anthropic is candid about the caveats. The proof is, in their words, likely much longer than it needs to be, and roughly 7 percent of the non-boilerplate lines came from failed early attempts. Kevin Buzzard, who has led the multi-year Imperial College effort to formalize the same theorem, wrote about being beaten to it.

Here is the part worth internalizing. Nobody has to trust Claude for this result to count. Lean checked it. The trust sits in a small, well-studied kernel that has been scrutinized for years, not in the model that produced the argument. That is a fundamentally different situation from asking a model whether its own answer is right, which is the setup that produces confidently wrong answers.

Why this does not verify your app

The reason formal methods stayed niche is not that nobody wanted them. It is that most software has no formal specification to verify against.

To prove a checkout flow correct, you first have to write down what correct means, in maths, precisely enough for a machine: every currency rounding rule, every partial refund, every race between two clicks. That specification is usually longer and harder than the code, and if it is wrong, you have proved nothing useful.

So the realistic split looks like this:

For the code an AI agent writes for you, the honest tools remain types, property-based tests, and reviewing AI-generated code before you ship it. None of them prove absence of bugs. They shrink the space where bugs hide.

The shift worth watching

The interesting claim is not that AI can prove theorems. It is that proof search has become a task where you can spend more compute and reliably get more result, and where the output is verified by something other than the model. That combination is rare.

Most model output has no oracle. When a model writes marketing copy or a migration script, there is no checker that returns true or false, which is why running evals on model output is difficult and always partial. Formal proof is the opposite: the oracle is free, exact, and instant. Any task with that shape, and there are more than people assume, is a task where models can grind away without a human validating every step.

Areas where this may land first: verified cryptographic implementations, protocol conformance, compiler optimization passes, and hardware verification. All of them share the property that the specification already exists in machine-checkable form.

FAQ

Is formal verification the same as testing?

No. Testing checks specific inputs and can only ever find bugs, never prove their absence. Formal verification proves a property holds for all inputs, but only for the property you managed to state.

Can AI formally verify the code it writes?

For narrow, well-specified components, increasingly yes. For a typical application, the blocker is not the proving. It is that writing a correct formal specification of what your app should do is harder than writing the app, and nobody has automated that.

Does a verified proof mean the model understood the maths?

It means the proof is correct, which is a separate question from understanding. Lean validates the artefact, not the process that produced it. That is precisely why the result is trustworthy without trusting the model. It also says nothing about how large language models actually work internally.

Should I care about this if I build small apps?

Not directly, and not yet. The useful takeaway is the pattern: output that a cheap, independent checker can validate is output you can let a model iterate on freely. Look for that shape in your own workflow, in type checkers, linters, schema validation, and test suites, and give the model as much room as the checker can cover.