However, this looks like an unusual case. Based on the fact that they had such a dumb design for this system, that shouldn’t have passed muster in any aviation context no matter your software methodology, it’s probably not representative enough to draw a larger lesson about engineering. The larger lesson seems to be business and regulatory.
Regarding Japanese cars, Toyota went through a big thing with unintended acceleration that got quite a few people killed. Software was suspected, but the cause was ultimately determined to (mostly?) be a combination of drivers mixing up the accelerator and the brake (happens more often than you might think) and unsecured floor mats pushing the accelerator down. I bought a Toyota not too long after this and the dealer made a special point to show me how the floor mat attached to the floor and that I must be sure it was solidly connected.
Their software was audited and apparently it was really badly made. It was described as “spaghetti-like” and had global variable abuse, ignored errors, failed to restart unresponsive tasks, and had potential memory corruption problems. It’s quite possible that this really was the cause, and a jury even found this to be the cause in a civil trial over one of the crashes, but it was never definitely linked.
I think the point is which these disasters show, and some others in the past (was there not a recalled Japanese car with a software issue?) that a few million more for the right resources will save you a lot more down the line. Problem is that this is not really a statement we can prove for formal verification because we do not have enough to compare with; i have a very strong feeling it will make quite a significant difference; if not for the proofs themselves then for the sheer number of hours and time the proofwriters thought about it by the time of delivery.