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