I hope the threat of LLMs making much of our existing software dramatically easier to hack will finally push the software community toward formally verifying security-critical software.

Ironically, LLMs are also dramatically lowering the cost of doing exactly that.

Formal verification isn't a panacea, of course. You can prove the wrong specification correct. But for the small, security-critical foundations that everything else depends on, I think the economics are becoming much more compelling.