Prediction: AI will make formal verification go mainstream

Summary

Kleppmann argues that AI will transform formal verification from a niche academic pursuit into mainstream software engineering. Formal verification—mathematically proving code correctness—has traditionally been prohibitively expensive, requiring “23 lines of proof and half a person-day for every single line of implementation.”

However, LLM-based coding assistants are becoming skilled at writing proof scripts, which could dramatically reduce costs. This shift matters because AI-generated code needs formal verification rather than human review for reliability. As automation handles proof generation, the focus will shift to specifying what properties code should satisfy—a more manageable challenge.

My thoughts

Fascinating prediction from the author of “Designing Data-Intensive Applications”, one of my favorite book. The economics argument is compelling: if AI makes proof-writing cheap, formal verification becomes viable. The cultural shift will be the harder part. But looking forward to it!