--- description: Break the implementation plan into ordered tasks argument-hint: allowed-tools: [Read, Write, Edit, Glob, Grep] --- # FormSpec Tasks You are breaking a feature's implementation plan into concrete, dependency-ordered tasks that can be executed one at a time. ## Steps ### 1. Read artifacts **$ARGUMENTS must provide a feature name.** If empty, ask the user for a feature name. The feature name should be the kebab-case identifier used when the feature was designed (e.g., `user-auth`, `billing`). **Locate the feature directory**: Glob for `spec/features/*-/plan.md`. If no match is found, tell the user to run `/formspec.4.plan ` first and stop. Read: - The feature's `plan.md` - The feature's `design.md` - `spec/formal/traceability.md` - Other features' `tasks.md` files (Glob for `spec/features/*/tasks.md`) — to understand what infrastructure and components already exist or are in progress, avoiding duplicate work ### 2. Generate the feature's tasks Write `spec/features/YYYY-MM-DD-/tasks.md` (in the same directory as the feature's `design.md` and `plan.md`) with two sections: implementation tasks and verification milestones. Implementation tasks are fine-grained and component-oriented — they track what code to write. Verification milestones are coarser and property-oriented — they define when a TLA+ property can actually be validated end-to-end. This separation exists because the implementation architecture is more fine-grained than the specification: a single formal property (e.g., crash safety) typically spans multiple implementation components (persistence layer + coordinator + integration tests), so no single task is a meaningful checkpoint for validating it. #### Task format ```markdown # Implementation Tasks ## Task T-01: [Title] **Depends on**: (none | T-XX, T-YY) **Implements**: US-3, SC-1 (from 2026-02-10-user-auth) **Description**: [What to implement — specific enough that the implementer knows exactly what code to write] **Acceptance**: [Unit-level criteria — how to verify this component works in isolation. Must be objectively verifiable. These are TDD checkpoints, not TLA+ property verification.] ``` Tasks do NOT have a "Verifies" field for TLA+ properties. Individual tasks verify their own component contracts through unit tests; TLA+ properties are verified at the milestone level. Task IDs are scoped to this feature — each feature's tasks start at T-01. When referencing tasks across features (rare, but possible for shared infrastructure), use the feature directory name as a prefix (e.g., `2026-02-10-user-auth/T-03`). Dependencies on components from other features are not expressed as task dependencies. Instead, note them in the task description as preconditions (e.g., "Requires the persistence layer from 2026-02-10-user-auth to be implemented"). The developer is responsible for ensuring cross-feature preconditions are met before starting. #### Milestone format After the tasks, add a milestones section: ```markdown # Verification Milestones ## Milestone M-01: [TLA+ Property or property group] **Tasks**: T-02, T-04, T-05, T-08 **Verifies**: PersistBeforeGrant, EventualRecovery (from System.tla) **Verification method**: `go test -race -run Recovery ./coordinator/...` **Description**: [What this milestone validates and why it requires all the listed tasks to be complete first] ``` A milestone gates on a set of tasks. Only after all of its tasks are complete can the verification method be run and the result recorded in the verification matrix. A single task may appear in multiple milestones. A single milestone may verify multiple related properties. ### 3. Coverage requirements **Tasks** must collectively cover: - **All user stories** from this feature's design doc (every US-N must appear in at least one task's "Implements" field) - **All implementation components** from this feature's plan architecture - **F* proof modules** if included in this feature's plan - **Infrastructure setup** tasks (project scaffolding, CI configuration, test harness) where needed — but only if not already provided by a prior feature **Milestones** must collectively cover: - **Every TLA+ property** sourced from this feature in traceability.md that has a runtime or integration-level verification method - **Every verification method** from this feature's plan Verification Strategy table - Properties verified by structural or compile-time guarantees do not need milestones — they are validated by the data model or type system, not by test execution ### 4. Dependency ordering rules - Foundational types, interfaces, and data models before business logic - Verification infrastructure (test harness, F* module structure) before verification tasks - Core functionality before features that depend on it - No circular dependencies - Tasks should be small enough to implement in a single session but large enough to be meaningful (not "create a file" granularity) - Each task should be independently testable with unit tests after its dependencies are met — if a task can only be tested as part of a larger integration, it should be merged with the tasks it depends on or the milestone structure should be reconsidered ### 5. Validation Before finishing, check: - Every US-N from this feature's design doc is covered by at least one task - Every TLA+ property sourced from this feature in traceability.md with a runtime verification method is covered by at least one milestone - Every milestone's task list references valid task IDs within this feature - Every task's dependencies reference valid task IDs within this feature - No circular dependency chains exist in the task graph - The dependency graph has a valid topological ordering - Every milestone's tasks collectively provide the components needed to execute its verification method (e.g., a milestone that verifies crash recovery must include tasks for persistence, the coordinator, and the recovery integration test) Report any gaps found during validation. Suggest proceeding with `/formspec.6.implement ` to start implementing tasks.