> The bugs will only disappear until the model that was used to security test the generated code becomes obsoleted.

I think you're ignoring the distinct possibility that even if the code is not formally verified, LLMs could simply stop writing bugs, or this kind of bugs. No matter how smart an attacker AI, it cannot exploit bugs that are simply not there.

But hell, even formally verified ones can only verify back to the spec. There are plenty of examples of bugs in formally verified software.

I place a higher likelihood on LLMs winning (producing fewer bugs than formally verified) over the long run. Mostly because verified software can, IIUC, only verify back to the spec. Whereas LLMs can go "uh, your spec itself has a bug, you really want me to codify that?".