A property can fail for four reasons and only one of them is a design bug: the cycle is wrong, the trigger never fires, the rule is too weak to see its mutant, or the design is actually broken. This topic is the triage routine for all four: read the trace backwards to the attempt, prove the trigger is reachable, mutate the rule, and run the checklist that catches the rest.

Suggested order: top to bottom. Trace reading first, because every later lesson starts from a failing run; then the two ways a pass can lie, vacuity and weakness; then the checklist that folds all of it into review practice. The coverage section of the course continues the cover story, and the engines section continues the induction failures. For writing the properties in the first place, see the property-development section.