I have used statistical analysis and formal methods in production code. Mainly Astree, https://www.absint.com/astree/index.htm https://www.absint.com/astree/ind

I have used statistical analysis and formal methods in production code. Mainly Astree, https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm When you have bought the tools to verify code in some safety critical project and know how to use it, it's easier to use it in less critical software too. You will soon hit the wall where formal correctness loses to time constraints and new features. You end up verifying only the code that is used repeatedly in multiple projects and does not change. Formal verification is not substitute for testing and code review. You can verify that the code is correct but you don't know if you have the correct code. The answer is: Because correctness of programs produces only limited value for normal use cases. It's more important to add more features than it is to produce solid code. If you don't have code reviews where all new code and changes are being read and analyzed by others (increasing the cost of the software 5-10 times) your interest in correct code is limited.