Summary as given in the post:
1. formal verification is about to become vastly cheaper;
2. AI-generated code needs formal verification so that we can skip human review and still be sure that it works;
3. the precision of formal verification counteracts the imprecise and probabilistic nature of LLMs.
These three things taken together mean formal verification is likely to go mainstream in the foreseeable future. I suspect that soon the limiting factor will not be the technology, but the culture change required for people to realise that formal methods have become viable in practice.
Summary as given in the post: 1. formal verification is about to become vastly cheaper; 2. AI-generated code needs formal verification so that we can skip human review and still be sure that it works; 3. the precision of formal verification counteracts the imprecise and probabilistic nature of LLMs. These three things taken together mean formal verification is likely to go mainstream in the foreseeable future. I suspect that soon the limiting factor will not be the technology, but the culture change required for people to realise that formal methods have become viable in practice.