A failing trace is not a verdict; it is a question with four possible answers. It can be a design bug, a missing assumption, an abstraction artefact, or a step that starts where no reset can reach. Each answer has a different fix, and guessing the class wastes the debug. This topic fixes the order: triage first, minimise and replay second, and name the trace kind before touching anything.
Lesson | After it you can... |
|---|---|
Classify any failure in a fixed order and prescribe the fix plus its regression. | |
Shorten a trace and replay it where the team can see it. | |
Tell the three failing traces apart and act correctly on each. | |
Read four real failures cycle by cycle, fix each, and watch the proof close. |
Suggested order: top to bottom. Triage is the entry point for every failure; the other three lessons are the tools it calls on. The worked lesson assumes all of them.
Not a bug report yet: an unreachable start. Fix the reset harness or the initial-state constraint first, then rerun before classifying anything.