This seemed like a high possibility, but since our adoption of LLMs in software so far has mostly been to throw out best practices, I am skeptical that it will lead us to expanded verification.

It's like Bezos talking about how we're going to have 3 day work weeks while he makes his employees piss in a bottle.

Automated proofs do sound very neat but I think they'll be constrained to a vanishingly small set of already paranoid domains like cryptography, aerospace, etc. Everywhere else is going to spend the dividends on shipping more unvetted code faster, we're just trading discipline for velocity.

Piss bottles are easily explained by rent though. You get more productive, so the landlord ups the rent, and you have to produce more for the people owning the scarce land (your landlord, the grocery store's landlord, the farmer, etc).

Software doesn't have this scarcity dynamic. People will use LLMs to build better sounder foundations (as rust is 'better' than c) and code quality will improve as we migrate to them. You won't get screwed on your rust++ license though to the point you have to piss in bottles.