Prediction: AI will make formal verification go mainstream

Note

LLM proof-script generation + formal checkers create a virtuous cycle. Cites seL4 (8,700 lines C, 20 person-years, 200,000 lines Isabelle) as evidence that cost barrier is collapsing.