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?".
That just doesn't seem like a reasonable possibility to me, given what we're seeing from and learning about these models. They have no capacity to be aware and adhere to an overarching vision, which is why they inevitably corrode architectural coherence over time [1]. The only reason these agents are able to still create usable code is because harnesses take advantage of model's ability to find bugs, giving us the famous loop, adding duct tape on top of duct tape, ratcheting up the complexity, until the adversarial model isn't able to find any more issues. Thus, the bugs are pushed out into higher complexity dimensions, temporarily invisible until a stronger model comes along which can detect them.
[1] see for example the "Decoherence Trap" article discussed here yesterday: https://maevyn.codes/decoherence
> There are plenty of examples of bugs in formally verified software.
Of course. Which is why humans will always need to be involved in the software creation process. We have to specify what we want. It's true that we ourselves often don't know what we want, in fact this is a big part of what software development is about: requirements gathering and continuously recondisering and reworking them. But it would be beyond naive to imagine that software might one day know better than us humans what it is we actually want, no?
My experience over the last couple of years with this type of prompt is that eventually you run out of bugs to find (meaning you reach "I see what you mean, but I disagree").
And those fixes don't cause messes.
And a new model may find something new, but not even remotely the volume seen the first time. This indicates to me that the supply of bugs is finite, and after this period of house cleaning, it should go down.
But anyway, a mess (decoherence) doesn't necessarily mean an exploitable mess.
Reading that good article, I find myself thinking that we did not need LLMs to get decoherence in complex software or systems. At least LLMs don't have personal fiefdoms, egos, and company politics adding to encouraging decoherence.
One thing to keep in mind is the logic of technological evolution and market competition will ensure that we always push the complexity of our systems to the edge of what is possible using current tools.
I don't deny that coding agents can be (and are) very useful for software engineering, as you say they have a lot going for them, and I'm pretty sure that once the dust has settled, they will be seen as an intrinsic part of the process, but I also am convinced that skilled humans will still very much be needed to direct and supervise them.
But even if new code gets bugs, we run a bug finding pass on the delta. So the vulnporalypse will end.
And in my prompts I've seen LLMs find complex interaction bugs that a human would basically never find (and the bug was added by a human).
You say polluted by vibe coding. But in terms of bugs, especially in the last like 6 months, you could argue that humans are the polluters.
E.g. while I've seen "ai deleted our database", but if what you're saying is true, we should be seeing "AI added this buffer overflow". But we don't, because humans are the polluters of that.
Yes, there have been "ai coded up client side password checking", but I've not seen that recently. Only like 6 generations and three years ago.
At some point it's like telling the cab driver to just follow Google maps directions. Like... sorry, cabbie (Black Cabs in London with their "the Knowledge" is what I'm thinking), your memorization, while impressive, is worse than the app.
The painter, while impressively skilled, is a worse documentarian than the camera.
And that point is probably behind us. At least for typing. And it's climbing up in abstractions.