This is also my take on this. IMHO, LLMs + theorem provers have the potential to make formal methods cheap enough to use more widely.

And we should give more credit to the theorem prover part of the equation, which comes in part from old AI symbolic efforts.