counterexample-debugger
Installation
SKILL.md
Counterexample Debugger
A counterexample is a proof that a property fails — a concrete sequence of states that leads to the violation. The trace is correct by construction; the job is to make it understandable.
Triage by source
| Tool | Counterexample format | Key decoding move |
|---|---|---|
| TLC (TLA+) | Numbered states with full variable dumps | Diff consecutive states — only the changes matter |
| NuSMV / nuXmv | State trace + -> State: N.M <- headers |
Same: diff states, ignore unchanged vars |
| CBMC / ESBMC | C-level trace with assignments | Map each assignment to a source line |
| Alloy | Instance graph (relational) | Project to the atoms involved in the violated assertion |
| Hypothesis / QuickCheck | Shrunk failing input | The input IS the counterexample — no trace to decode |
The compression algorithm
Raw traces are unreadable because they show every variable at every step. Compress: