96 lines
5.1 KiB
Markdown
96 lines
5.1 KiB
Markdown
---
|
|
description: Implement tasks with continuous formal verification
|
|
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.
|
|
|
|
## Steps
|
|
|
|
### 1. Read context
|
|
|
|
Read:
|
|
- `spec/tasks.md`
|
|
- `spec/plan.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` is empty: find the next task 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`.
|
|
|
|
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.
|
|
2. Write the implementation.
|
|
3. Run unit tests and iterate until passing.
|
|
|
|
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.
|
|
|
|
**b. Run the task's unit-level verification**:
|
|
- Unit tests for the component being implemented
|
|
- Compile-time checks: ensure code compiles and types check
|
|
- Structural guarantees: verify that the data model makes the property violation unrepresentable (no runtime check needed — record the structural reason in the verification matrix instead)
|
|
- Static analysis tools specified in the plan (e.g., `go vet`, `cargo clippy`)
|
|
|
|
**c. Handle failures**:
|
|
|
|
If the failure is a **code bug** (the unit test caught an implementation error):
|
|
- Diagnose and fix. This is normal TDD flow.
|
|
|
|
If the failure reveals an **inconsistency with the TLA+ spec** (the implementation cannot satisfy a formal property as specified, not due to a simple bug but due to a fundamental mismatch):
|
|
- **STOP**
|
|
- Explain to the developer:
|
|
- Which TLA+ property cannot be satisfied
|
|
- Why the implementation cannot satisfy it (what real-world constraint prevents it)
|
|
- Whether this indicates the TLA+ model is too idealized or the design needs revision
|
|
- Do not continue until the developer decides how to resolve
|
|
|
|
**d. Mark task complete**:
|
|
|
|
After unit tests pass, mark the task complete in `spec/tasks.md` (e.g., append `✓ COMPLETE` to the title).
|
|
|
|
**e. Continue to next task**:
|
|
|
|
After completing a task, if the next task's dependencies are all met, continue implementing it without stopping. Keep going until either:
|
|
- A unit test failure or spec inconsistency requires developer input
|
|
- A verification milestone is reached (all of its tasks are now complete)
|
|
- No more tasks are ready (unmet dependencies)
|
|
|
|
### 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:
|
|
|
|
**a. Run the milestone's verification method** (e.g., integration tests, property-based tests, recovery tests). These are the tests that validate TLA+ properties end-to-end across multiple components.
|
|
|
|
**b. Handle milestone verification failures**: If the integration test fails, diagnose whether the issue is in one of the component tasks (go back and fix it) or a cross-component interaction that wasn't caught by unit tests. If it reveals a spec inconsistency, STOP as described above.
|
|
|
|
**c. Update the verification matrix**: After the milestone's verification passes, update `spec/verification/matrix.md`. Create the file if it doesn't exist, using this format:
|
|
|
|
```markdown
|
|
# Verification Matrix
|
|
|
|
| Source Document | Requirement ID | TLA+ Property | Verification Tool | Status | Last Checked |
|
|
|----------------|----------------|---------------|-------------------|--------|--------------|
|
|
| features/YYYY-MM-DD-feature/design.md | US-1 | PropertyName | tool name | PASS | YYYY-MM-DD |
|
|
```
|
|
|
|
Update existing rows or add new ones. Set status to PASS with today's date. Only record a property as PASS when its milestone has been reached and the verification method has actually been executed.
|
|
|
|
### 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`.
|