validation-first-driven

Validation-first development

Contract

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

1. 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.
2. 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.
3. 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.

4. Write state machine specification. Use this template:

   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
   

   Done when: the specification is written with all states, variables, actions, and invariants.
5. 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.
6. 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.
7. 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.
8. 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.
9. 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.
10. 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.