Although I will admit that formal verification is looking better now than it ever did, and it's probably easier to generate proofs for those few simple safety-critical systems which benefit from it, I'm still bearish about it for the mainstream case.

I agree with "Even if fully automatic verification were within reach, it would be detrimental". Formal verification proofs make the same trade-off as overly fine-grained unit tests; they lock-down the current implementation and thus significantly reduce operational agility; because, if you make a modification to the code, you may have to re-generate the entire proof again. Proofs thus lock down sub-optimal abstractions and implementations. For many kinds of software, requirement changes are a daily occurrence and proofs would get in the way of making the required changes.

Even with complete, zero-cost automation of proof-generation, with no prompting or user-intervention (which would require the AI to have internalized a complete, perfect world-model), there would still be an incentive problem; when engineers see a lot of proofs and/or fine-grained unit tests, they are often reluctant to make the necessary refactoring to meet new requirements. Existing (counter-productive, flawed) abstractions become part of the lingo of the team and it becomes literally impossible to move off of them; yet they create a lasting barrier for new team members and when implementing new features.

The biggest problem though is that many modern software issues are flaws in the requirements (the spec itself), not in the implementation. The requirements are often produced by business people who often have a vague idea about what they want; requirements usually contain subtle contradictions or conflicts which have to be resolved.

Having worked on projects with clean, well architected code, requirements issues are by far the most common issue. On my last project, I kept coming back to my business/product co-founder with questions like: "You said that this checkbox should be on this page; but for a different onboarding flow, you said that it should be impossible for that specific user role to see/select this checkbox and the backend processing relies on this fact for reasons X, Y and Z..." or "You said to apply a filter to the collection and keep narrowing down the set as the user moves through the stages in the flow, but now you want to add a step which expands the set again with data from a different source; so now we can't just update the filter against a single collection; we need to make a separate table to hold the data from different sources; that will require some refactoring and it adds overhead since now we have to keep a lot of data per-user and we need to account for malicious spam-scenarios, etc... We can't just hold all the state in the URL (for bookmark) anymore... Users can't just share filters with each other anymore to restore the same app state across account boundaries."

In my last project, most of the work was trying to figure out what my co-founder wanted and it turns out that the idea he had in his head about the system was not logically consistent across all of its parts; a fact we only discovered after months of implementation. Also, he did not understand some of the technical limitations in terms of what kinds of data a free public API would give us access to; and that turned out to have been fundamentally incompatible with business objectives and the target market. His refusal to pivot to a premium market (where the user may have been able and willing to pay to cover the additional downstream API costs) marked the end of the project. The project was logically impossible from the start given the hard constraints of what platform to rely on, what our costs would be and what the target audience was. If we need formal verification, it would have to be for the requirements themselves, evaluated against the technical constraints. We don't need formal verification of the code.

Correct code is a mostly solved problem if you break down the typical software system into its sub-parts and identify the right platforms (e.g. CRUD, edge functions, data ingestion, data processing...) Correct requirements are a far bigger problem.