FM Before, During, and After AI

Last week I visited Dominik, Lucas, and their colleagues and students at the University of Manchester. I used the visit to put together my thinking on what applying Formal Methods in cloud and software has actually been like for me, and how I see that changing now that AI is here to stay.

With AI, it can feel like Formal Methods suddenly got cheap. And in a way it did. Building the models, writing the harnesses, generating invariants and proofs, work that used to take person-months now takes person-days. The floor dropped under our feet. But what AI made cheap is the labour, not the judgment or the human ideas: what to verify, whether an abstraction is faithful, whether we are asking the right questions at all. These all stay.

The floor dropped and the practical ceiling is rising, expanding the reach of Formal Methods in industry to the higher and harder problems. But the other ceiling, the one made of hard theoretical limits, won’t budge.

The slides from my talk are below. They carry the full story: before, during, and after AI. Curious to hear other people’s thoughts on this. Especially where you think I’m wrong.