Prediction: AI will make formal verification go mainstream
December 10, 2025
Much has been said about the effects that AI will have on software development, but there is an angle I haven’t seen talked about: I believe that AI will bring formal verification, which for decades has been a bit of a fringe pursuit, into the software engineering mainstream.
Source: Prediction: AI will make formal verification go mainstream — Martin Kleppmann’s blog
When I studied computer science at university in the 1980s, formal verification was a quite an area of research and interest.
What doesn’t really occur to most people is that computer science, in many ways, is a branch of mathematics. There are many mathematical approaches to programming and programming languages. There are famous theorems, like Turing’s work on the halting problem, there are questions about P vs NP.
None of this occurred to me, either, as a naive teenager who’d done some programming in Pascal and Forth and, of course, BASIC, and then I largely forgot about it for the last 30 or 40 years, but turns out verification is making a comeback.
Formal verification is different from things like debugging. It’s about proving mathematically the correctness of a piece of code against its specifications.
As Martin Kleppmann observes here, formal verification is really hard, time-intensive, and expensive and there are a handful of experts in the entire world. It’s very valuable for systems that essentially cannot fail, but years of work can go into verifying a few hundred lines of code.
But it turns out large language models might be really good at this work. And we might see a renaissance of formal verification of software.
