Even then it doesn't matter if your software is "correct" if you don't understand/have not captured all the requirements. You could write a formally verified M

Even then it doesn't matter if your software is "correct" if you don't understand/have not captured all the requirements. You could write a formally verified MCAS system in Coq or whatever that still kills people because you didn't consider the case of sensor failure (because that wasn't in the requirements). Or because you didn't consider the case of double sensor failure or a combination of extremely rare hardware failures (that wasn't in the requirements either!). Your code is mathematically perfect, yes! But it was built with the incorrect assumption that the hardware is perfect as well! I'll take a robust set of tests written by someone thinking outside of the box in terms of what could fail, how it will be used in operation, etc. over a piece of software "guaranteed unsinkable" because it is formally verified.