99 lines
5.3 KiB
Markdown
99 lines
5.3 KiB
Markdown
---
|
|
description: Create an implementation plan with formal verification strategy
|
|
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.
|
|
|
|
## 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:
|
|
|
|
```markdown
|
|
# 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.
|