Module 2 — Abstraction: Black-Boxing & Data Abstraction

Over-approximate sub-module behaviors with assume constraints and suppress irrelevant data. Reduce the verification state space while preserving all safety properties of the full design.

Katas in this module (3)

• Kata 2.1 — Black-Box the Multiplier, Prove the Comparator
• Kata 2.2 — When Black-Boxing Goes Wrong
• Kata 2.3 — Data Abstraction: A Counter Becomes Three States

Part of Industrial Practice: Scaling Formal Verification on formal.org.