From 16b89024b558e136f7b3a8d8bb5dbcc447d54b28 Mon Sep 17 00:00:00 2001 From: Ohad Livne Date: Fri, 6 Mar 2026 15:15:58 +0200 Subject: [PATCH 1/4] Update Claude settings --- .claude/settings.json | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.claude/settings.json b/.claude/settings.json index beffa9d..2ac8850 100644 --- a/.claude/settings.json +++ b/.claude/settings.json @@ -34,5 +34,6 @@ "enabledPlugins": { "gopls-lsp@claude-plugins-official": true }, - "skipDangerousModePermissionPrompt": true + "skipDangerousModePermissionPrompt": true, + "effortLevel": "high" } From 53e83a666b1299af0a7cca33ba2db3c562997461 Mon Sep 17 00:00:00 2001 From: Ohad Livne Date: Sat, 7 Mar 2026 15:03:20 +0200 Subject: [PATCH 2/4] Update Claude WebFetch permissions --- .claude/settings.json | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/.claude/settings.json b/.claude/settings.json index 2ac8850..459b0ab 100644 --- a/.claude/settings.json +++ b/.claude/settings.json @@ -28,7 +28,11 @@ "WebFetch(domain:datatracker.ietf.org)", "WebFetch(domain:docs.cloud.google.com)", "WebFetch(domain:docs.gauge.sh)", - "WebFetch(domain:docs.temporal.io)" + "WebFetch(domain:docs.temporal.io)", + "WebFetch(domain:libfuse.github.io)", + "WebFetch(domain:lwn.net)", + "WebFetch(domain:man7.org)", + "WebFetch(domain:www.phoronix.com)" ] }, "enabledPlugins": { From 77b25c461ec4bf6513e6e647b9c2d5400d302342 Mon Sep 17 00:00:00 2001 From: Ohad Livne Date: Sat, 28 Feb 2026 09:56:26 +0200 Subject: [PATCH 3/4] 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. From c2430308c7e111f3225133271ea3f03ddc567255 Mon Sep 17 00:00:00 2001 From: Ohad Livne Date: Sat, 28 Feb 2026 04:15:06 +0200 Subject: [PATCH 4/4] Rename workflow steps for lexical order --- .../{formspec.init.0.md => formspec.0.init.md} | 10 +++++----- .../{formspec.design.1.md => formspec.1.design.md} | 6 +++--- ...formspec.formalize.2.md => formspec.2.formalize.md} | 8 ++++---- .../{formspec.verify.3.md => formspec.3.verify.md} | 6 +++--- .../{formspec.plan.4.md => formspec.4.plan.md} | 6 +++--- .../{formspec.tasks.5.md => formspec.5.tasks.md} | 4 ++-- ...formspec.implement.6.md => formspec.6.implement.md} | 8 ++++---- .../{formspec.docs.7.md => formspec.7.docs.md} | 6 +++--- .../{formspec.check.8.md => formspec.8.check.md} | 2 +- 9 files changed, 28 insertions(+), 28 deletions(-) rename .claude/commands/{formspec.init.0.md => formspec.0.init.md} (94%) rename .claude/commands/{formspec.design.1.md => formspec.1.design.md} (96%) rename .claude/commands/{formspec.formalize.2.md => formspec.2.formalize.md} (97%) rename .claude/commands/{formspec.verify.3.md => formspec.3.verify.md} (83%) rename .claude/commands/{formspec.plan.4.md => formspec.4.plan.md} (96%) rename .claude/commands/{formspec.tasks.5.md => formspec.5.tasks.md} (98%) rename .claude/commands/{formspec.implement.6.md => formspec.6.implement.md} (92%) rename .claude/commands/{formspec.docs.7.md => formspec.7.docs.md} (95%) rename .claude/commands/{formspec.check.8.md => formspec.8.check.md} (96%) diff --git a/.claude/commands/formspec.init.0.md b/.claude/commands/formspec.0.init.md similarity index 94% rename from .claude/commands/formspec.init.0.md rename to .claude/commands/formspec.0.init.md index 1e21e7f..8739117 100644 --- a/.claude/commands/formspec.init.0.md +++ b/.claude/commands/formspec.0.init.md @@ -14,7 +14,7 @@ You are initializing a formal-specification-driven development project. Your job Use Glob to check if `spec/system.md` already exists in the project root. -If it exists: **STOP**. Tell the user that the project is already initialized and they should use `/formspec.design.1` to add features. Do not modify anything. +If it exists: **STOP**. Tell the user that the project is already initialized and they should use `/formspec.1.design` to add features. Do not modify anything. ### 2. Gather system description @@ -52,7 +52,7 @@ Write `spec/system.md` with the following structure. Fill in the System Overview ## Feature Index -*No features designed yet. Use `/formspec.design.1 ` to add features.* +*No features designed yet. Use `/formspec.1.design ` to add features.* ## Changelog @@ -63,7 +63,7 @@ The System Overview should be a concise but complete description — enough for ### 5. Report -Tell the user what was created and suggest they proceed with `/formspec.design.1 ` to start designing features. +Tell the user what was created and suggest they proceed with `/formspec.1.design ` to start designing features. ## Hook convention @@ -75,7 +75,7 @@ If a hook script does not exist, the command falls back to its default behavior **Path**: `spec/hooks/run-checks` -**Called by**: `/formspec.formalize`, `/formspec.verify`, `/formspec.implement`, `/formspec.check` +**Called by**: `/formspec.2.formalize`, `/formspec.3.verify`, `/formspec.6.implement`, `/formspec.8.check` **When**: When verification needs to be performed (TLC model checking, milestone tests, consistency checks). @@ -85,7 +85,7 @@ If a hook script does not exist, the command falls back to its default behavior ```json { - "command": "formspec.implement", + "command": "formspec.6.implement", "project_root": "/home/user/projects/mutex", "checks": [ { diff --git a/.claude/commands/formspec.design.1.md b/.claude/commands/formspec.1.design.md similarity index 96% rename from .claude/commands/formspec.design.1.md rename to .claude/commands/formspec.1.design.md index e02e063..5e3f803 100644 --- a/.claude/commands/formspec.design.1.md +++ b/.claude/commands/formspec.1.design.md @@ -12,7 +12,7 @@ You are creating a detailed natural-language design document for a single featur ### 1. Validate preconditions -**spec/system.md must exist.** Check with Glob. If it does not exist, tell the user to run `/formspec.init.0` first and stop. +**spec/system.md must exist.** Check with Glob. If it does not exist, tell the user to run `/formspec.0.init` first and stop. **$ARGUMENTS must provide a feature name.** If empty, ask the user for a feature name. The feature name should be a short kebab-case identifier (e.g., `user-auth`, `billing`, `rate-limiting`). @@ -103,7 +103,7 @@ SC-1: [Criterion with measurable target] ## Amendments -[Do NOT create this section in new design docs. It is added by `/formspec.formalize.2` when TLC counterexamples force design changes. If this section already exists in a design doc you are editing, preserve it — amendments are permanent records of corrections discovered through formal verification. Only remove an amendment if the requirement it annotates is itself removed through a larger redesign, or changed significantly enough that a plain rewrite is simpler than preserving the amendment history.] +[Do NOT create this section in new design docs. It is added by `/formspec.2.formalize` when TLC counterexamples force design changes. If this section already exists in a design doc you are editing, preserve it — amendments are permanent records of corrections discovered through formal verification. Only remove an amendment if the requirement it annotates is itself removed through a larger redesign, or changed significantly enough that a plain rewrite is simpler than preserving the amendment history.] ``` **Quality bar**: The design must be specific enough that a different developer could implement it without further conversation. Vague statements like "should be fast" or "handle errors gracefully" are not acceptable — quantify or describe the specific behavior. @@ -134,4 +134,4 @@ Also update the affected feature's design doc if the impact is significant enoug ### 6. Report -Summarize what was created, highlight any cross-feature impacts, and note any open questions that need resolution before formalization. Suggest proceeding with `/formspec.formalize.2` to translate the design into a TLA+ specification. +Summarize what was created, highlight any cross-feature impacts, and note any open questions that need resolution before formalization. Suggest proceeding with `/formspec.2.formalize` to translate the design into a TLA+ specification. diff --git a/.claude/commands/formspec.formalize.2.md b/.claude/commands/formspec.2.formalize.md similarity index 97% rename from .claude/commands/formspec.formalize.2.md rename to .claude/commands/formspec.2.formalize.md index a45376c..0f4d1e7 100644 --- a/.claude/commands/formspec.formalize.2.md +++ b/.claude/commands/formspec.2.formalize.md @@ -85,7 +85,7 @@ Every requirement from Phase 1 must appear in this table. If a requirement canno ## Phase 4 — Run TLC model checker -If `spec/hooks/run-checks` exists and is executable, delegate TLC verification to it instead of running locally (see `/formspec.init` for the hook interface). Present the returned results to the developer, including any dashboard URLs, and skip to Phase 5. +If `spec/hooks/run-checks` exists and is executable, delegate TLC verification to it instead of running locally (see `/formspec.0.init` for the hook interface). Present the returned results to the developer, including any dashboard URLs, and skip to Phase 5. If the hook does not exist or fails, run TLC locally: @@ -116,7 +116,7 @@ Parse the TLC output to determine: ### All properties pass -Update all statuses in `spec/formal/traceability.md` from `formalized` to `checked`. Report success with a summary of what was verified: number of properties checked, state space explored, time taken. Suggest proceeding with `/formspec.plan.4` to create an implementation plan. +Update all statuses in `spec/formal/traceability.md` from `formalized` to `checked`. Report success with a summary of what was verified: number of properties checked, state space explored, time taken. Suggest proceeding with `/formspec.4.plan` to create an implementation plan. ### Meaning drift detected (Phase 2 issue) @@ -147,7 +147,7 @@ Present to the developer: 5. **Classification**: Whether this violates an explicit design requirement or a best-practice property that you added **Do not proceed** until the developer explicitly acknowledges and decides how to resolve. Possible resolutions: -- Redesign the component (go back to `/formspec.design.1`) +- Redesign the component (go back to `/formspec.1.design`) - Add a constraint to the design - Accept the risk with documented justification - Modify the TLA+ model if the property was too strict @@ -182,7 +182,7 @@ Amendments are permanent — they document the design's provenance and record wh **Evaluating amendment volume**: Multiple amendments in a single formalization run are not necessarily a problem — they may indicate that the design was written at a high level (e.g., by an AI agent or during an early brainstorming phase) and the formalization is doing its job of tightening it. The signal to watch for is not the count but the *pattern*: - **Amendments spread across different parts of the spec** (different user stories, different components, different properties) suggest the design was broadly sketched and TLC is finding the expected gaps. This is normal and productive. -- **Amendments concentrated around the same requirement or interaction** suggest a localized design flaw that incremental patching may not resolve. After 2-3 amendments to the same area, consider whether the component needs a broader redesign via `/formspec.design.1` rather than further patching. +- **Amendments concentrated around the same requirement or interaction** suggest a localized design flaw that incremental patching may not resolve. After 2-3 amendments to the same area, consider whether the component needs a broader redesign via `/formspec.1.design` rather than further patching. After recording the amendment, restart from Phase 2. diff --git a/.claude/commands/formspec.verify.3.md b/.claude/commands/formspec.3.verify.md similarity index 83% rename from .claude/commands/formspec.verify.3.md rename to .claude/commands/formspec.3.verify.md index caeb654..5963f40 100644 --- a/.claude/commands/formspec.verify.3.md +++ b/.claude/commands/formspec.3.verify.md @@ -16,11 +16,11 @@ Check that both files exist: - `spec/formal/System.tla` - `spec/formal/System.cfg` -If either is missing, tell the user to run `/formspec.formalize.2` first and stop. +If either is missing, tell the user to run `/formspec.2.formalize` first and stop. ### 2. Run TLC -If `spec/hooks/run-checks` exists and is executable, delegate verification to it instead of running TLC locally (see `/formspec.init` for the hook interface). Build the request from `spec/formal/traceability.md` (properties and their types) and `spec/formal/System.cfg` (the TLC invocation hint). Present the returned results to the developer, including any dashboard URLs. +If `spec/hooks/run-checks` exists and is executable, delegate verification to it instead of running TLC locally (see `/formspec.0.init` for the hook interface). Build the request from `spec/formal/traceability.md` (properties and their types) and `spec/formal/System.cfg` (the TLC invocation hint). Present the returned results to the developer, including any dashboard URLs. If the hook does not exist or fails, run TLC locally: @@ -52,4 +52,4 @@ Read the TLC output (or hook response) and produce a structured report: ### 4. No modifications -Do not modify `System.tla`, `System.cfg`, `traceability.md`, or any other file. This command is purely diagnostic. If violations are found, advise the user to run `/formspec.formalize.2` to address them. +Do not modify `System.tla`, `System.cfg`, `traceability.md`, or any other file. This command is purely diagnostic. If violations are found, advise the user to run `/formspec.2.formalize` to address them. diff --git a/.claude/commands/formspec.plan.4.md b/.claude/commands/formspec.4.plan.md similarity index 96% rename from .claude/commands/formspec.plan.4.md rename to .claude/commands/formspec.4.plan.md index 8d29aff..4f76ef0 100644 --- a/.claude/commands/formspec.plan.4.md +++ b/.claude/commands/formspec.4.plan.md @@ -14,7 +14,7 @@ You are creating an implementation plan for a single feature, bridging its forma **$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. +**Locate the feature directory**: Glob for `spec/features/*-/design.md`. If no match is found, tell the user to run `/formspec.1.design ` first and stop. If multiple matches exist (unlikely), use the most recent by date prefix. Read: - `spec/system.md` @@ -30,7 +30,7 @@ All of these must exist. If any are missing, tell the user which prerequisite co 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 +- Direct them to run `/formspec.2.formalize` first - Stop ### 3. Generate the feature's plan @@ -106,4 +106,4 @@ Before finishing, verify: ### 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.5.tasks ` to break it into implementable tasks. diff --git a/.claude/commands/formspec.tasks.5.md b/.claude/commands/formspec.5.tasks.md similarity index 98% rename from .claude/commands/formspec.tasks.5.md rename to .claude/commands/formspec.5.tasks.md index b7f2315..fdc5e15 100644 --- a/.claude/commands/formspec.tasks.5.md +++ b/.claude/commands/formspec.5.tasks.md @@ -14,7 +14,7 @@ You are breaking a feature's implementation plan into concrete, dependency-order **$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. +**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` @@ -95,4 +95,4 @@ Before finishing, check: - 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.6.implement ` to start implementing tasks. diff --git a/.claude/commands/formspec.implement.6.md b/.claude/commands/formspec.6.implement.md similarity index 92% rename from .claude/commands/formspec.implement.6.md rename to .claude/commands/formspec.6.implement.md index d283a19..414c327 100644 --- a/.claude/commands/formspec.implement.6.md +++ b/.claude/commands/formspec.6.implement.md @@ -15,7 +15,7 @@ You are implementing tasks from a feature's `tasks.md` with continuous verificat **$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. +**Locate the feature directory**: Glob for `spec/features/*-/tasks.md`. If no match is found, tell the user to run `/formspec.5.tasks ` first and stop. Read: - The feature's `tasks.md` @@ -30,7 +30,7 @@ If $ARGUMENTS includes a task ID (e.g., `T-03`) or milestone ID (e.g., `M-01`): 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. +If all tasks are complete, report that and suggest running `/formspec.7.docs` to generate documentation, then `/formspec.8.check` to validate consistency. ### 3. Implement the task @@ -81,7 +81,7 @@ Stop regardless of the developer's preference when: 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. +**a. Run the milestone's verification**: If `spec/hooks/run-checks` exists and is executable, delegate the milestone's verification to it (see `/formspec.0.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. If the hook does not exist or fails, run the milestone's verification method locally (e.g., integration tests, property-based tests, recovery tests). These are the tests that validate TLA+ properties end-to-end across multiple components. @@ -101,4 +101,4 @@ Update existing rows or add new ones. Set status to PASS with today's date. Only ### 5. Cross-check (periodic) -After completing a milestone, briefly check whether the changes could have affected any previously verified properties. If there's a risk of regression, advise running `/formspec.check.8` or `/formspec.verify.3`. +After completing a milestone, briefly check whether the changes could have affected any previously verified properties. If there's a risk of regression, advise running `/formspec.8.check` or `/formspec.3.verify`. diff --git a/.claude/commands/formspec.docs.7.md b/.claude/commands/formspec.7.docs.md similarity index 95% rename from .claude/commands/formspec.docs.7.md rename to .claude/commands/formspec.7.docs.md index 6a90cf5..26a7be9 100644 --- a/.claude/commands/formspec.docs.7.md +++ b/.claude/commands/formspec.7.docs.md @@ -18,7 +18,7 @@ Read: - `spec/formal/traceability.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. +All spec artifacts must exist. If `spec/system.md` or feature design docs are missing, direct the user to the prerequisite commands (`/formspec.0.init`, `/formspec.1.design`) and stop. ### 2. Determine documentation scope @@ -50,7 +50,7 @@ Create or update documentation files. The exact structure depends on the project ### 4. Add spec traceability -Documentation should link back to design documents where it describes feature behavior. Use inline references so that readers (and `/formspec.check.8`) can trace documentation claims to their source: +Documentation should link back to design documents where it describes feature behavior. Use inline references so that readers (and `/formspec.8.check`) can trace documentation claims to their source: ```markdown @@ -74,4 +74,4 @@ Flag any discrepancies found. ### 6. Report -Summarize what documentation was created or updated, which design documents it traces to, and any gaps where documentation could not be generated (e.g., design doc lacks enough detail for user-facing docs). Suggest running `/formspec.check.8` to validate full cross-artifact consistency. +Summarize what documentation was created or updated, which design documents it traces to, and any gaps where documentation could not be generated (e.g., design doc lacks enough detail for user-facing docs). Suggest running `/formspec.8.check` to validate full cross-artifact consistency. diff --git a/.claude/commands/formspec.check.8.md b/.claude/commands/formspec.8.check.md similarity index 96% rename from .claude/commands/formspec.check.8.md rename to .claude/commands/formspec.8.check.md index 27e1292..fc7709b 100644 --- a/.claude/commands/formspec.check.8.md +++ b/.claude/commands/formspec.8.check.md @@ -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), feature plans (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.0.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: