Module 8 — State Machines and State Graphs

Reachability via cover, observer FSMs inside properties, one-hot invariants, BMC depth as path length, cycle witnesses, and detecting stuck states.

Katas in this module (6)

• Kata 8.1 — Reachability via Cover
• Kata 8.2 — Observer FSM in a Property
• Kata 8.3 — One-Hot State Invariant
• Kata 8.4 — BMC Depth as Path Length
• Kata 8.5 — Cycle Witness via Sequence
• Kata 8.6 — Stuck State (Out-Degree Zero)

Part of Discrete Mathematics for Formal Verification on formal.org.