Module 5 — What a Proof Claims

A PASS is not correctness. Vacuous proofs, complete property suites, BMC versus mode prove, and writing properties that survive k-induction rather than a shallow bound.

Katas in this module (6)

• Kata 5.1 — Vacuous Pass
• Kata 5.2 — Complete Property Suite
• Kata 5.3 — No Scaffold
• Kata 5.4 — BMC vs Prove
• Kata 5.5 — Write for mode prove
• Kata 5.6 — No Scaffold — k-Induction

Part of Hardware Formal Verification on formal.org.