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.

Steps

1. Read all artifacts

Read:

spec/system.md
All feature design docs: Glob for spec/features/*/design.md
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 must have status checked (meaning TLC has verified it). If any 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

Write spec/plan.md with these sections:

# Implementation Plan

## Technology Choices

[Language(s), frameworks, infrastructure. 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.

## 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.]

## Verification Strategy

[A table mapping each TLA+ property to implementation-level verification methods.]

| 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 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.]

- 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 from traceability.md appears in the Verification Strategy
Every feature's user stories are 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.

5.3 KiB Raw Blame History