OutlineDriven Validation-first development
Contract
| Field | Bound contract |
|---|---|
| Trigger | The work builds protocols, workflows, concurrent systems, or lifecycle-heavy state, or needs temporal properties or a state machine. |
| Authority | Reversible local: writes only within the stated target; rollback is version control. No remote mutation. No file or VCS mutation outside the stated target. |
| Side effect | Writes the model and spec plus implementation assertions and tests; creates a TLA+ or Alloy spec for high-risk designs. |
| Done | The state space is explicit, transitions are total, invariants are checked, and each temporal property maps to an assertion, test, or model-checker run. |
Inputs
- Requirements or design document. Required.
- Current codebase. Optional.
- Support files: approaches, examples, formal-tools, event-sourcing reference notes. Optional; the skill is self-contained without them.
Procedure
- Identify scope. Confirm the work involves explicit states, transitions, temporal properties, or lifecycle-heavy state. If it is a stateless endpoint, pure data transformation, simple CRUD without lifecycle, configuration parse, or stateless batch process, stop and return the work unaltered. Done when: the work is confirmed as state-heavy or returned unaltered.
- Capture states and transitions. Extract all named states, state variables, actions, guards, and side effects from the requirements. Identify every temporal property: "always eventually", "never", "until", "leads-to". Done when: all states, transitions, and temporal properties are extracted.
- Choose mechanism level.
Level Mechanism Use when Typestate Generic type params, phantom data Protocol APIs, builder patterns, Rust FFI Statecharts Nested states, parallel regions Game state, multi-modal UI, XState Flat FSM Enum + match/switch Order lifecycle, connection management Actor model Independent entities, message passing Distributed systems, Erlang/Elixir Default: use the strongest mechanism the language supports. Done when: one mechanism level is chosen with rationale. - Write state machine specification. Use this template:
Done when: the specification is written with all states, variables, actions, and invariants.STATE MACHINE: <Name> STATES: S1 | S2 | S3 VARIABLES: var1: type, var2: type INIT: var1 = val, state = S1 ACTION name(args): PRE: guard -> POST: new_state, effects INVARIANT: condition_that_always_holds - Define validation level. Rank each invariant by enforcement strength: Type system (strongest) > State machine > Contract > Runtime check (weakest). Done when: every invariant has a validation level.
- Encode compile-time properties in types. Use typestate, sealed classes, or discriminated unions to make invalid states unrepresentable. Encode every invariant the type system can express. Done when: every type-expressible invariant is encoded.
- Layer state machine modeling. For properties types cannot express, define a state machine with explicit states and transitions. For high-risk designs, write a TLA+ or Alloy spec and run the model checker. High-risk threshold: the design involves distributed consensus, lock-free concurrency, a protocol with liveness or safety guarantees, or multi-party state coordination. Designs below this threshold use the state machine spec and tests without a model checker. Done when: every non-type-expressible property has a state machine or model-checker spec.
- Check every transition. Verify invariants hold after each action. Confirm exhaustive matching on all states. Block on any invariant violation. Done when: every transition is checked and invariants hold.
- Write assertions and tests. Map each temporal property to an assertion, a test, or a model-checker run. Every transition must have a test. Every invariant must have a verification point. Done when: every temporal property, transition, and invariant has a verification point.
- Implement. Mirror the specification exactly: one state type, one transition function, one invariant check per concern. Keep state and behavior together. Done when: the implementation mirrors the specification.
Failure and recovery
- Wrong-scope work: Return the work unaltered. Do not apply state machine modeling to stateless work.
- Checker unavailable (high-risk branch only): The design met the high-risk threshold but the TLA+ or Alloy model checker could not be installed or run. Return exit code 11 and a blocked verdict. Do not proceed without verification. Designs below the high-risk threshold do not require a model checker and are not blocked by its absence.
- Specification syntax or type error: Return exit code 12 and the first error location. Block implementation.
- Invariant violation: Return exit code 13 and the violating state or transition. Block implementation. Do not mask or suppress.
- Test failure: Return exit code 14 and the failing test. Block if tests are required.
- Implementation not matching spec: Return exit code 15 and the mismatched function or type. Block finalization.
- Partial result: Return the highest verification gate that passed with its exit code and evidence. Do not claim the done predicate holds if any blocking gate failed.
- Non-converged: If the state space is undecidable or the model checker does not terminate, stop and report the open temporal properties with no coverage.
Output
A state machine specification, verified implementation with assertions for every transition and invariant, test suite covering all states and transitions, optional TLA+/Alloy model, and exit code (0 or the blocking gate code).