We should look at formal verification like everything else: in terms of statistical effectiveness. It's not really important whether or not there are _no_ bugs.

We should look at formal verification like everything else: in terms of statistical effectiveness. It's not really important whether or not there are _no_ bugs. What's important is how many bugs there are for each unit of "effort." For example, if this were hypothetically the only bug that was ever found, then that would be a pretty damn good argument that formal verification is effective. Because the bug rate of other non-verified operating systems is much higher.