AI will make formal verification go mainstream
New blog post
Hi! You’re getting this email because you subscribed to my blog posts at martin.kleppmann.com.
I just published a short post in which I argue that AI will make formal verification go mainstream. There are three reasons why I think this:
A future where LLMs can write proofs of correctness fully automatically, without human input, seems within reach. That will make formalisation vastly cheaper than it has been for the last few decades.
If you generate code using AI, but then have to carefully review it by hand, you don’t save much time overall. But if the AI proves that the code is correct, you can confidently use it without having to even look at it.
LLMs are great at making up plausible-sounding nonsense, but automated proof checkers won’t be fooled by this, which makes it much safer to use LLMs in this context.
For comments, please find me on Bluesky!