From 77b25c461ec4bf6513e6e647b9c2d5400d302342 Mon Sep 17 00:00:00 2001 From: Ohad Livne Date: Sat, 28 Feb 2026 09:56:26 +0200 Subject: [PATCH] Scope some workflow steps to individual features --- .claude/commands/formspec.check.8.md | 16 ++++----- .claude/commands/formspec.docs.7.md | 6 ++-- .claude/commands/formspec.implement.6.md | 26 ++++++++------- .claude/commands/formspec.plan.4.md | 40 +++++++++++++--------- .claude/commands/formspec.tasks.5.md | 42 +++++++++++++++--------- 5 files changed, 77 insertions(+), 53 deletions(-) diff --git a/.claude/commands/formspec.check.8.md b/.claude/commands/formspec.check.8.md index 9060ada..27e1292 100644 --- a/.claude/commands/formspec.check.8.md +++ b/.claude/commands/formspec.check.8.md @@ -17,8 +17,8 @@ Read every artifact that exists (skip gracefully if some don't exist yet): - All feature design docs: Glob for `spec/features/*/design.md` - `spec/formal/System.tla` and `spec/formal/System.cfg` - `spec/formal/traceability.md` -- `spec/plan.md` -- `spec/tasks.md` +- All feature plans: Glob for `spec/features/*/plan.md` +- All feature task lists: Glob for `spec/features/*/tasks.md` - `spec/verification/matrix.md` Also scan: @@ -35,13 +35,13 @@ Perform each of these checks and record findings: - No TLA+ properties exist in System.tla without a corresponding entry in traceability.md - No orphaned entries in traceability.md (property exists in table but not in System.tla) -**TLA+ <-> Implementation (if plan.md and matrix.md exist)**: -- Every TLA+ property has at least one implementation-level verification method in plan.md +**TLA+ <-> Implementation (if feature plans and matrix.md exist)**: +- Every TLA+ property has at least one implementation-level verification method in a feature plan - Every verification method has been executed and recorded in matrix.md - No FAIL or PENDING entries in matrix.md that lack explanation -- Verification matrix entries correspond to completed milestones, not individual tasks — flag any property marked PASS whose milestone tasks are not all complete +- Verification matrix entries correspond to completed milestones, not individual tasks — flag any property marked PASS whose milestone tasks (in the relevant feature's tasks.md) are not all complete -**Design <-> Implementation (if tasks.md exists)**: +**Design <-> Implementation (if feature task lists exist)**: - Every user story (US-N) from every feature design doc is covered by at least one task - Every task is marked complete or has a documented reason for incompleteness - No tasks reference nonexistent user stories or properties @@ -65,7 +65,7 @@ Perform each of these checks and record findings: - No implementation code files that don't trace back to any task (heuristic — flag files that seem substantial but aren't referenced) **Tests <-> Specification (if test files exist)**: -- Every TLA+ property with a runtime verification method (from plan.md's Verification Strategy) has corresponding test cases in the codebase +- Every TLA+ property with a runtime verification method (from the feature's plan.md Verification Strategy) has corresponding test cases in the codebase - Test names or comments reference the TLA+ property or design requirement they verify - No test files exist that don't trace back to any task or verification method (heuristic — flag test files that seem unrelated to the spec) - Property-based tests (if specified in the plan) exist and cover the properties they claim to verify @@ -86,7 +86,7 @@ Perform each of these checks and record findings: ### 3. Run verification -If `spec/hooks/run-checks` exists and is executable, delegate all verification (TLC and language-specific tools) to it (see `/formspec.init` for the hook interface). Build the request from `spec/formal/traceability.md` (TLA+ properties), `spec/plan.md` (verification methods), and detected source files (language-specific checks). The external system runs all checks independently and returns results. +If `spec/hooks/run-checks` exists and is executable, delegate all verification (TLC and language-specific tools) to it (see `/formspec.init` for the hook interface). Build the request from `spec/formal/traceability.md` (TLA+ properties), feature plans (verification methods), and detected source files (language-specific checks). The external system runs all checks independently and returns results. If the hook does not exist or fails, run checks locally: diff --git a/.claude/commands/formspec.docs.7.md b/.claude/commands/formspec.docs.7.md index a4eb25f..6a90cf5 100644 --- a/.claude/commands/formspec.docs.7.md +++ b/.claude/commands/formspec.docs.7.md @@ -14,8 +14,8 @@ You are generating user-facing documentation derived from the system's design do Read: - `spec/system.md` - All feature design docs: Glob for `spec/features/*/design.md` +- All feature plans: Glob for `spec/features/*/plan.md` - `spec/formal/traceability.md` -- `spec/plan.md` - Existing documentation in the project root and `docs/` directory (Glob for `*.md`, `docs/**/*.md`, excluding `spec/`) All spec artifacts must exist. If `spec/system.md` or feature design docs are missing, direct the user to the prerequisite commands (`/formspec.init.0`, `/formspec.design.1`) and stop. @@ -25,7 +25,7 @@ All spec artifacts must exist. If `spec/system.md` or feature design docs are mi From the design artifacts, identify what needs to be documented: - System-level overview and purpose (from `spec/system.md`) - Per-feature user-facing behavior (from feature design docs — user stories, success criteria) -- Configuration, setup, and usage (from plan.md — technology choices, architecture) +- Configuration, setup, and usage (from feature plans — technology choices, architecture) - API contracts and interfaces (from design docs — Interface Contract sections are the primary source; user stories describe the behavior behind those interfaces) - Behavioral guarantees the system makes (from traceability — which formal properties translate to user-visible promises) @@ -40,7 +40,7 @@ Create or update documentation files. The exact structure depends on the project **README.md** (if it doesn't exist or needs updating): - Project description derived from `spec/system.md` System Overview -- Setup and usage instructions derived from `spec/plan.md` technology choices +- Setup and usage instructions derived from feature plans' technology choices - Feature descriptions derived from feature design docs **docs/** (for projects complex enough to warrant separate pages): diff --git a/.claude/commands/formspec.implement.6.md b/.claude/commands/formspec.implement.6.md index 7a7ee9f..d283a19 100644 --- a/.claude/commands/formspec.implement.6.md +++ b/.claude/commands/formspec.implement.6.md @@ -1,36 +1,40 @@ --- description: Implement tasks with continuous formal verification -argument-hint: [task-id] +argument-hint: [task-id] allowed-tools: [Read, Write, Edit, Glob, Grep, Bash, Task] model: opus --- # FormSpec Implement -You are implementing tasks from `spec/tasks.md` with continuous verification against the formal specification. +You are implementing tasks from a feature's `tasks.md` with continuous verification against the formal specification. ## Steps ### 1. Read context +**$ARGUMENTS must provide at least a feature name.** It may optionally include a task ID or milestone ID (e.g., `user-auth T-03` or `user-auth M-01`). If the feature name is missing, ask the user for it. + +**Locate the feature directory**: Glob for `spec/features/*-/tasks.md`. If no match is found, tell the user to run `/formspec.tasks.5 ` first and stop. + Read: -- `spec/tasks.md` -- `spec/plan.md` +- The feature's `tasks.md` +- The feature's `plan.md` +- The feature's `design.md` - `spec/formal/traceability.md` - `spec/formal/System.tla` -- Relevant feature design docs (determine which ones from the task's "Implements" field) ### 2. Select task -If `$ARGUMENTS` specifies a task ID (e.g., `T-03`) or milestone ID (e.g., `M-01`): implement that task or all remaining tasks for that milestone. Verify dependencies are complete first — if not, warn the user and suggest implementing dependencies first. +If $ARGUMENTS includes a task ID (e.g., `T-03`) or milestone ID (e.g., `M-01`): implement that task or all remaining tasks for that milestone. Verify dependencies are complete first — if not, warn the user and suggest implementing dependencies first. -If `$ARGUMENTS` is empty: find the next task whose dependencies are all complete. If multiple tasks are ready, pick the lowest-numbered one. +If no task ID is specified: find the next task in this feature's `tasks.md` whose dependencies are all complete. If multiple tasks are ready, pick the lowest-numbered one. If all tasks are complete, report that and suggest running `/formspec.docs.7` to generate documentation, then `/formspec.check.8` to validate consistency. ### 3. Implement the task -Read the task's full specification from `spec/tasks.md`. +Read the task's full specification from the feature's `tasks.md`. Follow TDD: 1. Write unit tests first, derived from the task's acceptance criteria. These tests verify the component's contract in isolation — they are not TLA+ property checks, they are component-level correctness checks. @@ -39,7 +43,7 @@ Follow TDD: Unit tests at this level serve two purposes: they catch implementation bugs early (before dependent tasks build on a broken foundation), and they force component boundaries to remain clear and well-defined, which makes later integration smoother. -**a. Implement the code** following the plan's architecture and technology choices. When the task involves a component that exposes or consumes an interface, refer to the Interface Contract section in the relevant design doc for the concrete schemas, wire formats, and error conventions. +**a. Implement the code** following the feature plan's architecture and technology choices. When the task involves a component that exposes or consumes an interface, refer to the Interface Contract section in the feature's design doc for the concrete schemas, wire formats, and error conventions. **b. Run the task's unit-level verification**: - Unit tests for the component being implemented @@ -62,7 +66,7 @@ If the failure reveals an **inconsistency with the TLA+ spec** (the implementati **d. Mark task complete**: -After unit tests pass, mark the task complete in `spec/tasks.md` (e.g., append `✓ COMPLETE` to the title). +After unit tests pass, mark the task complete in the feature's `tasks.md` (e.g., append `✓ COMPLETE` to the title). **e. Continue to next task**: @@ -75,7 +79,7 @@ Stop regardless of the developer's preference when: ### 4. Verify milestones -After completing a task, check whether any verification milestones in `spec/tasks.md` have all their tasks complete. For each newly-completed milestone: +After completing a task, check whether any verification milestones in the feature's `tasks.md` have all their tasks complete. For each newly-completed milestone: **a. Run the milestone's verification**: If `spec/hooks/run-checks` exists and is executable, delegate the milestone's verification to it (see `/formspec.init` for the hook interface). The request should include the milestone's properties, verification methods, and hints (e.g., the test commands from the plan). The external system runs the checks independently and returns results. diff --git a/.claude/commands/formspec.plan.4.md b/.claude/commands/formspec.plan.4.md index 5bfa812..8d29aff 100644 --- a/.claude/commands/formspec.plan.4.md +++ b/.claude/commands/formspec.plan.4.md @@ -1,19 +1,25 @@ --- description: Create an implementation plan with formal verification strategy +argument-hint: allowed-tools: [Read, Write, Edit, Glob, Grep, Task] --- # FormSpec Plan -You are creating an implementation plan that bridges the formal TLA+ specification to concrete code, with a verification strategy ensuring each formal property is checked by implementation-level tools. +You are creating an implementation plan for a single feature, bridging its formal TLA+ properties to concrete code with a verification strategy ensuring each property is checked by implementation-level tools. ## Steps -### 1. Read all artifacts +### 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/*-/design.md`. If no match is found, tell the user to run `/formspec.design.1 ` first and stop. If multiple matches exist (unlikely), use the most recent by date prefix. Read: - `spec/system.md` -- All feature design docs: Glob for `spec/features/*/design.md` +- The feature's `design.md` +- Other feature design docs under `spec/features/` (for cross-feature context) - `spec/formal/System.tla` - `spec/formal/System.cfg` - `spec/formal/traceability.md` @@ -22,33 +28,37 @@ All of these must exist. If any are missing, tell the user which prerequisite co ### 2. Validate formal verification status -Check `spec/formal/traceability.md`. Every formalizable property must have status `checked` (meaning TLC has verified it). If any property has status `formalized`, `violated`, or `not-yet-formalized` without adequate justification: +Check `spec/formal/traceability.md`. Every formalizable property **sourced from this feature's design doc** must have status `checked` (meaning TLC has verified it). If any such property has status `formalized`, `violated`, or `not-yet-formalized` without adequate justification: - Tell the user which properties are not yet verified - Direct them to run `/formspec.formalize.2` first - Stop -### 3. Generate spec/plan.md +### 3. Generate the feature's plan -Write `spec/plan.md` with these sections: +Write `spec/features/YYYY-MM-DD-/plan.md` (in the same directory as the feature's `design.md`) with these sections: ```markdown -# Implementation Plan +# Implementation Plan: ## Technology Choices -[Language(s), frameworks, infrastructure. Each choice must be justified against the formal properties where relevant.] +[Language(s), frameworks, infrastructure needed for this feature. Each choice must be justified against the formal properties where relevant.] Example: "Rust for the auth module — ownership system prevents use-after-free, directly satisfying the MemorySafety invariant. Go for the API gateway — goroutines with race detector verify the NoConcurrentAccess property at test time." Do not justify choices that have no relationship to formal properties — just state them. +For the first feature in a project, this section establishes the system-wide technology stack. For subsequent features, reference existing choices and only document additions or deviations. + ## Architecture -[Component structure, communication patterns, data flow. Reference how the architecture maps to the TLA+ model's actors and processes. Where design docs define Interface Contracts, the architecture should describe how components connect through those interfaces and confirm that the planned component boundaries align with the contracts.] +[Component structure, communication patterns, data flow for this feature. Reference how the architecture maps to the TLA+ model's actors and processes. Where design docs define Interface Contracts, the architecture should describe how components connect through those interfaces and confirm that the planned component boundaries align with the contracts.] + +For subsequent features, describe how this feature's components integrate with the existing system — what it reuses, what it adds, and where boundaries lie. ## Verification Strategy -[A table mapping each TLA+ property to implementation-level verification methods.] +[A table mapping each of this feature's TLA+ properties to implementation-level verification methods. Include system-level properties (e.g., architectural constraints) that this feature's implementation must satisfy.] | Source Document | Requirement ID | TLA+ Property | Verification Method | Tool | |----------------|----------------|---------------|---------------------|------| @@ -64,7 +74,7 @@ Verification methods include: - **Formal proofs**: F* modules that verify TLA+ properties - **Test coverage**: Specific test cases derived from TLC state exploration -Every TLA+ property in the traceability matrix must have at least one verification method. Properties with only "manual review" are not acceptable — find a tool-assisted method. +Every TLA+ property in the traceability matrix that is sourced from this feature must have at least one verification method. Properties with only "manual review" are not acceptable — find a tool-assisted method. When a TLA+ property is satisfied structurally, do not claim it is verified by a runtime test. A no-op test function that "checks" a structurally-guaranteed property is misleading — it will never fail, so it provides no signal. Instead, record the verification method as "Structural guarantee" and explain what data model decision enforces it. @@ -78,7 +88,7 @@ When a TLA+ property is satisfied structurally, do not claim it is verified by a ## Testing Strategy -[Unit, integration, and property-based testing approach.] +[Unit, integration, and property-based testing approach for this feature.] - How tests trace back to TLA+ properties - Property-based test generators derived from the TLA+ state space @@ -89,11 +99,11 @@ When a TLA+ property is satisfied structurally, do not claim it is verified by a ### 4. Quality check Before finishing, verify: -- Every TLA+ property from traceability.md appears in the Verification Strategy -- Every feature's user stories are addressed by the architecture +- Every TLA+ property sourced from this feature in traceability.md appears in the Verification Strategy +- Every user story from this feature's design doc is addressed by the architecture - Technology choices don't contradict architectural constraints from system.md - The verification strategy is actually executable (tools exist, are available, and can check what's claimed) ### 5. Report -Summarize the plan and suggest proceeding with `/formspec.tasks.5` to break it into implementable tasks. +Summarize the plan and suggest proceeding with `/formspec.tasks.5 ` to break it into implementable tasks. diff --git a/.claude/commands/formspec.tasks.5.md b/.claude/commands/formspec.tasks.5.md index cfff86c..b7f2315 100644 --- a/.claude/commands/formspec.tasks.5.md +++ b/.claude/commands/formspec.tasks.5.md @@ -1,24 +1,30 @@ --- description: Break the implementation plan into ordered tasks +argument-hint: allowed-tools: [Read, Write, Edit, Glob, Grep] --- # FormSpec Tasks -You are breaking the implementation plan into concrete, dependency-ordered tasks that can be executed one at a time. +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.plan.4 ` first and stop. + Read: -- `spec/plan.md` (must exist — if not, direct user to `/formspec.plan.4`) +- The feature's `plan.md` +- The feature's `design.md` - `spec/formal/traceability.md` -- All feature design docs: Glob for `spec/features/*/design.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 spec/tasks.md +### 2. Generate the feature's tasks -Write `spec/tasks.md` with two sections: implementation tasks and verification milestones. +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. @@ -36,6 +42,10 @@ Implementation tasks are fine-grained and component-oriented — they track what 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: @@ -55,14 +65,14 @@ A milestone gates on a set of tasks. Only after all of its tasks are complete ca ### 3. Coverage requirements **Tasks** must collectively cover: -- **All user stories** from all feature design docs (every US-N must appear in at least one task's "Implements" field) -- **All implementation components** from the plan's architecture -- **F* proof modules** if included in the plan -- **Infrastructure setup** tasks (project scaffolding, CI configuration, test harness) where needed +- **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** from traceability.md that has a runtime or integration-level verification method -- **Every verification method** from the plan's Verification Strategy table +- **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 @@ -77,12 +87,12 @@ A milestone gates on a set of tasks. Only after all of its tasks are complete ca ### 5. Validation Before finishing, check: -- Every US-N from every feature design doc is covered by at least one task -- Every TLA+ property from traceability.md with a runtime verification method is covered by at least one milestone -- Every milestone's task list references valid task IDs -- Every task's dependencies reference valid task IDs +- 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.implement.6` to start implementing tasks. +Report any gaps found during validation. Suggest proceeding with `/formspec.implement.6 ` to start implementing tasks.