--- 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 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 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` - 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` All of these must exist. If any are missing, tell the user which prerequisite command to run and stop. ### 2. Validate formal verification status 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 the feature's plan Write `spec/features/YYYY-MM-DD-/plan.md` (in the same directory as the feature's `design.md`) with these sections: ```markdown # Implementation Plan: ## Technology Choices [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 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 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 | |----------------|----------------|---------------|---------------------|------| | system.md | Architectural constraint | NoDeadlock | Race detection | go test -race | | features/.../user-auth/design.md | US-2 | AuthInvariant | Type system + unit tests | Rust ownership + cargo test | | system.md | Best practice | NoBackdoorTokens | Formal proof | F* (Auth.fst) | Verification methods include: - **Structural guarantees**: The implementation's data model makes a property violation unrepresentable. This happens when a TLA+ spec has redundant variables kept in sync (e.g., separate `holder` and `clientState` maps) but the implementation collapses them into a single source of truth (e.g., a struct with one `Holder` field). The property is enforced by construction — there is no code path, however buggy, that could violate it. When claiming a structural guarantee, name the specific data model choice that enforces it. - **Compile-time guarantees**: The language's type system or ownership model prevents the violation. Rust ownership preventing use-after-free, F* dependent types proving a bound, Go's type system preventing a type confusion. Distinct from structural guarantees: compile-time guarantees rely on the *language*, structural guarantees rely on the *data model*. - **Static analysis**: cargo clippy, go vet, staticcheck, rust-analyzer - **Runtime checks**: go test -race, property-based tests, fuzzing - **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 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. ## F* Integration Plan [Include this section only if F* is part of the verification strategy.] - Which properties will be formally proved in F* - How F* modules correspond to TLA+ properties - How F* proofs relate to the implementation code (extracted code vs. separate proof) ## Testing Strategy [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 - Integration tests that exercise cross-component interactions modeled in the TLA+ spec - Coverage targets and how they relate to formal verification completeness ``` ### 4. Quality check Before finishing, verify: - 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.