I think as long as we don't integrate formal verification into the programs themselves, it's not going to become mainstream. Especially now you got two different pieces you need to maintain and keep in sync (whether using LLMs or not).

Strong type systems are providing partial validation which is helping quite a lot IMO. The better we can model the state - the more constraints we can define in the model, the closer we'd be getting to writing "self-proven" code. I would assume formal proofs do way more than just ensuring validity of the model, but the similar approaches can be integrated to mainstream programs as well I believe.