Formal Verification in the Age of AI

For decades, research in formal verification has been guided by a simple mental model that I recently coined the formal verification triangle.

The triangle captures a trade-off between three desirable properties:

• Automation – the verification tool runs largely without human guidance
• Scalability – the technique works on large real systems
• Precision – the method can prove interesting properties, such as functional correctness

Historically, verification techniques could reliably achieve two of the three, but not all three simultaneously.

Static analysis scales to millions of lines of code but sacrifices precision. Model checking provides precise answers but struggles with large systems. Interactive theorem proving can scale and remain precise — but only through substantial human effort.

The triangle was never a theorem, but it described the practical limits of verification engineering remarkably well.

Until now.

What the Triangle Really Measured

All verification tools automate some work. The real question has always been what kind of labour can be delegated to machines.

Decision procedures — SAT solving, SMT solving, abstract interpretation — allowed machines to automate certain kinds of reasoning:

• constraint solving
• fixpoint computation
• symbolic execution
• bounded state exploration

But other tasks stubbornly remained human:

• inventing lemmas
• structuring proofs
• discovering complex invariants
• reorganising proof developments
• repairing proofs after changes

Interactive theorem proving mechanised these forms of reasoning: proofs could be constructed and checked within a proof assistant, but the reasoning itself largely remained manual.

The price was labour.

The landmark verification of functional correctness for the ~9k line C implementation of the seL4 verified microkernel required roughly:

• ~200k lines of Isabelle/HOL proofs
• completed in ~20 person-years of work

The triangle therefore reflected a constraint on which kinds of reasoning could realistically be automated.

A Striking Comparison

Recent progress in AI-assisted theorem proving and formalisation suggests that this constraint may be shifting.

An AI system recently produced a formal proof of the sphere-packing results in dimensions 8 and 24 consisting of roughly 200k lines of proof in about two weeks.

While the similarity in proof size to the seL4 result is striking, the two efforts are hardly identical. The seL4 project required building a complete system model and proof architecture for a real operating system. Mathematical formalisation builds on extensive libraries and, in the case of the sphere packing result, a large body of human-written existing theory.

But the comparison is still illuminating.

For decades, verification engineers implicitly assumed that a proof development of that scale implied years of human effort. Very roughly speaking, during the seL4 project we would often talk about 10,000 lines of proof being about a year’s worth of effort.

That assumption may no longer hold.

If the cost of producing and maintaining proofs drops by even an order of magnitude, the implications for verified systems are profound. As others have noted, verification could move from heroic one-off projects to something closer to routine engineering practice.

The Verification Feedback Loop

What seems to make recent systems effective is not simply that AI can generate proofs.

It is that they operate inside a verification feedback loop with two key ingredients:

1. A correctness oracle
2. Rich feedback that enables repair

Interactive theorem provers provide both.

The proof kernel acts as the oracle: it checks whether a proof step is valid. The proof state provides detailed feedback: unproved goals, missing assumptions, failed tactics, etc.

This creates a powerful loop:

propose → check → feedback → repair → repeat

The trusted kernel guarantees correctness, while the AI performs exploratory reasoning.

The Role of Traditional Verification Techniques

This shift does not make traditional automated verification techniques, such as static analysis and model checking, obsolete.

Instead, it may highlight a different role for them.

Static analysis and model checking are already excellent sources of structured feedback:

• model checkers produce counterexample traces
• static analysers infer candidate invariants and abstractions
• abstract interpretation provides over-approximations of system behaviour

These signals can guide exploration in an AI-driven verification loop.

For example:

• a model checker might produce a counterexample trace that forces an AI agent to strengthen an invariant
• a static analyser might suggest invariants that the agent attempts to prove in a theorem prover
• abstract interpretation might provide approximations that guide proof search

Rather than replacing these techniques, AI may turn them into components of a feedback-rich verification ecosystem.

It would also be a mistake to assume that the future of verification simply looks like automatically writing interactive proofs. That is the most obvious extrapolation of today’s tools, but it may not be the most interesting one.

A Call to Rethink Verification

The formal verification triangle assumed that automation meant decision procedures: push a button and get a yes/no answer.

AI suggests a broader notion of automation.

Automation can also mean delegating reasoning labour to agents whose output is continuously checked by a trusted oracle and refined through feedback.

Once that kind of delegation becomes possible, the design space of verification systems changes dramatically.

In ten years, we may not be verifying software inside a single proof assistant. Instead we may see entirely new verification architectures built around the propose–check–feedback–repair loop, combining theorem provers, model checkers, static analysers, and other tools in ways we have not yet explored.

The formal verification triangle did not describe a fundamental law of verification.

It described the limits of a particular generation of automation technology.

Those limits are starting to move.

The challenge now is to rethink verification in a world where previously undelegable reasoning labour can be delegated to machines.