flâneur

Prediction: AI will make formal verification go mainstream — Martin Kleppmann’s blog

martin.kleppmann.com · 1,246 words · saved by 1 readers

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. Proof assistants and proof-oriented programming languages such as Rocq, Isabelle, Lean, F*, and Agda have been around for a long time. They make it possible to write a formal specification that some piece of code is supposed to satisfy, and then mathematically prove that the code always satisfies that spec (even on weird edge cases that you didn’t think of testing). These tools have been used to develop some large formally verified software systems, such as an operating system kernel, a C compiler, and a cryptographic protocol stack. At present, formal verification is mostly used by research projects, and it is uncommon for industrial software engineers to use formal methods (even those working on classic high-ass

Prediction: AI will make formal verification go mainstream - Martin Kleppmann's blog Skip to content Martin Kleppmann Student Projects About/Contact Supporters Prediction: AI will make formal verification go mainstream Published by Martin Kleppmann on 08 Dec 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. Proof assistants and proof-oriented programming languages

related reading