| 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. |