What problem does it solve? Natural-language requirements are ambiguous and cannot be machine-checked. This Skill structures extracted requirements into EARS-notation statements and a state/domain model, then lowers them into a TLA+ specification (<Name>.tla / <Name>.cfg) and a Gherkin skeleton (<Name>.feature) ready for model checking. ## Core Features & Use Cases - EARS Structuring: Rewrites each requirement into one of the five EARS patterns (ubiquitous, event, state, unwanted, optional), with a reference of compound patterns for multi-condition, role-based, priority, and quantified NFR cases. - State/Domain Modeling: Derives state variables, types, initial state, and invariants, and records which regions were deliberately abstracted away so they are verified elsewhere. - TLA+ Scaffolding: Generates <Name>.tla and <Name>.feature from templates via the loop-outer toolchain, mapping each EARS clause to one Next disjunct and ubiquitous clauses to invariants, with a traceability matrix back to the requirement ledger. - Use Case: After loopeng-extract closes a requirements ledger for a payment flow, run this Skill to produce EARS statements, a state model, and a TLA+ spec that loopeng-modelcheck can verify with TLC. ## Quick Start Formalize the extracted requirements in tasks/loopeng/Payment.extract.md into EARS statements and generate the TLA+ spec and Gherkin skeleton.
