The difference is that code with bugs can still compile, but proofs that are unsound won't check. Now granted, you can still prove the wrong thing or _not_ prov

The difference is that code with bugs can still compile, but proofs that are unsound won't check. Now granted, you can still prove the wrong thing or _not_ prove the thing that is supposed to make your system robust is taking place, so it's still very much a human endeavor with all that entails. I think a dedicated red team going after a system for 6 months and not finding anything is a pretty good "unit test", personally. It's _evidence_ of effectiveness, not _proof_.