What problem does it solve? A TLA+ spec that passes TLC model checking may still be weak: its invariants might not actually distinguish buggy behavior. This Skill runs TLC model checking on a formalized design and then injects mechanical mutations into the spec itself to verify that the checks can catch injected faults, closing the gap between "no error found" and "the design is actually verified". ## Core Features & Use Cases - TLC Model Checking: Runs TLC against the Inv invariant over all reachable states of a <Name>.tla / <Name>.cfg pair produced by loopeng-formalize, surfacing counterexample traces when the design violates invariants. - Mutation Oracle: Injects mechanical mutations (e.g., < to \leq, = to #, /\ to \/) into the spec and confirms TLC kills each mutant, with procedures to distinguish true survivors (design holes) from equivalent mutants and to detect false-killed mutants where the mutation was never applied. - Use Case: After formalizing a queue protocol in TLA+, run the middle loop to confirm TLC reports no invariant violations, then verify every surviving mutant is an equivalent-mutant before declaring the design verified and handing off to Gherkin acceptance-spec generation. ## Quick Start Run the middle loop on my TLA+ spec by model-checking it with TLC and then applying the mutation oracle to check for surviving mutants.
