This won't happen to any large extent for the simple reason that in 95% of the software that people write, deciding what constitutes "correctness" (aka business

This won't happen to any large extent for the simple reason that in 95% of the software that people write, deciding what constitutes "correctness" (aka business requirements) is the bulk of the work. Further, those requirements change continually. Even if they could be frozen at a certain point, specifying them formally would be a massive undertaking, and the correct formal specification of those requirements would itself be a source of errors. How do you know when the formal specification means exactly what you really meant it to? As an example, I heard a story about an ambulance dispatch system that was built using formal verification. One of the things the developers wanted to prove about the system was that after an emergency call, an ambulance would always be dispatched within a certain amount of time. This seemed like an easy requirement to formalize: "For any dispatched ambulance A, the time of dispatch minus the time of call must be less than T". Unfortunately, after the system was deployed, it turned out that occasionally an ambulance would simply never show up in response to a call. This seemed impossible until the developers realized that the proof still held, it was simply vacuously true in this case. The fix is obvious in hindsight: The requirement should start with "For any emergency call...". But the point is that it is possible to make mistakes in requirements, just as it is possible to make mistakes in implementation. Formal proof is no silver bullet for software.