What problem does it solve? Formal verification tools like TLA+ and Lean rigorously check the requirements they are given, but they cannot guarantee that the extraction of requirements from the original specification was complete. This Skill closes that gap by enforcing an exhaustive, auditable extraction step before any formalization begins, so missing requirements surface at the entry point instead of at the exit. ## Core Features & Use Cases - Exhaustive requirement extraction: Scans RFCs, Japanese PRDs, OpenAPI/protobuf schemas, user stories, and IaC code using document-type-specific anchors (normative-word grep, full element enumeration, acceptance criteria) and assigns each requirement a sequential ID (S-001...) in a checkbox ledger. - Traceability matrix: Maps each specification clause to its EARS requirement, formal method artifact (TLA+ invariant / Lean property), and test in one shared ledger, making gaps visible as empty cells. - Hard gate enforcement: A PreToolUse hook mechanically blocks downstream formalization steps until every ID is checked off with no numbering gaps. - Use Case: Given an RFC for a protocol you must implement, run this Skill to produce a complete requirements ledger and traceability matrix before writing any TLA+ spec, so no MUST requirement silently disappears from the implementation. ## Quick Start Extract all requirements from this RFC specification into a numbered checklist ledger with a traceability matrix.
