That's literally the opposite of reality; the research and adoption have consistently produced code of extremely high quality, at great cost.

The problem has always been:

- It's extremely labour-intensive, and even small changes to the code can require an enormous amount of new proof work.

- The skills required to formally verify software are very different from the skills required to write it, and the set of people capable of doing so is much smaller.

- Code has to be written with verification in mind, against a specification that expresses invariants that can actually be verified, and that is coherent enough that you can derive useful high-level properties of the system from it.

You needed two teams — verification and development. Verification would always be behind the development team, while also having to feed requirements and design changes back to the developers. Everything slowed to a crawl.

AI changes this. A coherent, verifiable, useful specification isn't easy to write — but it's far easier to write than the software itself, and AI can do most of that work: both drafting the spec and proving that it's consistent and that the high-level properties you actually care about follow from it.

More importantly, a high-level spec is far easier to read and reason about than the reams of code required to actually implement something. Which means:

- AI does the grunt work of writing and proving the spec; humans only have to carefully review that high-level artifact.

- AI writes code it must also prove conforms to the spec, so humans can be assured it's correct without babysitting the AI.

- Changes are driven top-down: evolve the spec first, then have the AI fix the implementation and re-prove conformance.

Our (very, very large) company is rapidly going all-in on formal verification across projects we never would have dreamed of verifying before; the velocity hit and the man-hour cost were only worth paying for truly critical infrastructure.