I generally agree with your assessment. But frumplestlatz also says that literally their smartest engineers are not smart enough to do formal verification.

Agreed. Further, this has been true even ignoring formal verification. Who has been in the situation of making the choice to ship known-buggy code to make a release date or satisfy a customer demand for other functionality? All of us, I suspect, if we’re being honest. I certainly have.