What problem does it solve? Concurrent, stateful, and protocol-heavy designs hide interaction bugs that manual testing cannot enumerate. This Skill routes natural-language requirements through a triple feedback loop—EARS structuring, TLA+ exhaustive model checking, and counterexample-to-Gherkin conversion—so design correctness is verified before implementation begins. ## Core Features & Use Cases - Two-question activation gate: Starts only when transitions, ordering, or concurrency exist and the state space can be bounded; otherwise defers to TDD or property-based testing. - Four-phase pipeline: Delegates to loopeng-extract (requirement ledger), loopeng-formalize (EARS to TLA+ spec), loopeng-modelcheck (TLC plus mutation oracle), and loopeng-gherkin (counterexamples to acceptance scenarios). - Compliance review gate: Requires dispatching a loop-engineering-reviewer subagent before claiming the design is verified, checking ledger completeness and artifact hygiene. - Use Case: Designing a connection lifecycle with retries and locks—extract every requirement into a numbered ledger, write a bounded TLA+ spec, let TLC exhaustively check invariants, and convert any counterexample trace into a failing Gherkin scenario. ## Quick Start Ask the AI to verify the design of your stateful protocol or concurrency logic with loop-engineering, providing the requirement text or specification file path.
