Spurious passes vs spurious failures
Formal tools are mathematically rigorous — about the question you asked. When the question is subtly wrong, the answer can be rigorously useless. Two kinds of error exist:
| False negative | False positive | |
|---|---|---|
| What you see | Assertion fails | Assertion proven |
| Reality | No real bug (bad assumption or property) | A real bug exists, or nothing was really checked |
| Cost | Debug time | A bug escapes — possibly to silicon |
| How you notice | You have to debug it anyway | Only if you go looking |
Failures announce themselves. Passes do not. That asymmetry is why experienced formal engineers treat a proof as a claim to be audited, not as a result. The rest of this chapter is a tour of the most common ways passes go wrong, each with a small example you can reproduce.