When Proofs Lie: Avoiding False Positives
The ways a formal environment can report "proven" while a real bug survives — over-constraints, vacuity, reset mistakes, wrong configurations, shallow bounds — and the habits that catch them.
What you will learn
- Define a false positive and explain why it is more dangerous than a false negative.
- Recognise over-constraining assumptions and vacuous assertions.
- Spot reset and clock setup mistakes that silently disable checking.
- Apply a false-positive checklist before every signoff.
Lessons
- 9.1Spurious passes vs spurious failuresWhy "proven" deserves more scrutiny than "failed".
- 9.2Over-constraining assumptionsAssumptions that remove the very behaviour where the bug lives.
- 9.3Vacuity and unreachable coversImplications that can never trigger.
- 9.4Reset and clock mistakesHow a wrong polarity can make every assertion pass.
- 9.5Wrong configuration, wrong files, shallow boundsProving something other than what you ship.
- 9.6A false-positive checklistRun through this before calling anything signed off.
- ✎Chapter quiz (4 questions)