The ironic thing is that LLMs are what will make formal methods feasible.

First: LLMs find so many bugs and security holes in software right now. So you pretty much have to prove your stuff correct, if you don't want to get hacked into.

Second: LLMs make it much easier to apply formal methods. Just ask Claude to prove your stuff in Lean or whatever, no PhD required anymore.