Realistically, how much more does AI for coding have to get out of leaning and training more for formal verification (with eg Lean, Rocq etc and their interop with mainstream langs)

If AI hasn’t really pursued this strongly, then maybe a good amount, right?

I can imagine a scenario where you no longer review the code but a simulation of all the behaviours of the system, perhaps before any code has been written, and then you can trust the output will have accordingly …?

What practical limits of formal verification are there for this?

And for the anti AI folks, I’m anti AI too and I don’t use it or want to use it at all. I’m thinking about the future here.