138 lines
5.8 KiB
Markdown
138 lines
5.8 KiB
Markdown
---
|
|
description: Initialize formspec project structure
|
|
argument-hint: <system-description>
|
|
allowed-tools: [Read, Write, Edit, Glob, Grep, Bash]
|
|
---
|
|
|
|
# FormSpec Init
|
|
|
|
You are initializing a formal-specification-driven development project. Your job is to create the `spec/` directory structure and a foundational `spec/system.md` document.
|
|
|
|
## Steps
|
|
|
|
### 1. Check for existing spec/ directory
|
|
|
|
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.1.design` to add features. Do not modify anything.
|
|
|
|
### 2. Gather system description
|
|
|
|
If `$ARGUMENTS` is provided, use it as the high-level system description.
|
|
|
|
If `$ARGUMENTS` is empty or too vague to work with, ask the user to describe:
|
|
- What the system is and its purpose
|
|
- Who the primary actors are (users, services, external systems)
|
|
- Key constraints (non-negotiable properties like statelessness, partition tolerance, latency bounds, security requirements)
|
|
|
|
### 3. Create directory structure
|
|
|
|
Create the following directories:
|
|
```
|
|
spec/formal/subsystems/
|
|
spec/features/
|
|
spec/verification/
|
|
spec/hooks/
|
|
```
|
|
|
|
### 4. Generate spec/system.md
|
|
|
|
Write `spec/system.md` with the following structure. Fill in the System Overview and Architectural Constraints based on the gathered description. Leave Feature Index and Changelog empty with placeholder text.
|
|
|
|
```markdown
|
|
# System Design
|
|
|
|
## System Overview
|
|
|
|
[What is this system, who uses it, why does it exist. Derived from the user's description.]
|
|
|
|
## Architectural Constraints
|
|
|
|
[Non-negotiable properties of the system. Each constraint should be a clear, testable statement.]
|
|
|
|
## Feature Index
|
|
|
|
*No features designed yet. Use `/formspec.1.design <feature-name>` to add features.*
|
|
|
|
## Changelog
|
|
|
|
*No changes recorded yet.*
|
|
```
|
|
|
|
The System Overview should be a concise but complete description — enough for someone unfamiliar with the project to understand what they're looking at. The Architectural Constraints should be concrete and specific, not vague aspirations.
|
|
|
|
### 5. Report
|
|
|
|
Tell the user what was created and suggest they proceed with `/formspec.1.design <feature-name>` to start designing features.
|
|
|
|
## Hook convention
|
|
|
|
The `spec/hooks/` directory holds executable scripts that formspec commands invoke at defined points. This allows projects to plug in custom behavior (e.g., delegating verification to a TCMS, triggering CI pipelines, posting notifications) without modifying the commands themselves.
|
|
|
|
If a hook script does not exist, the command falls back to its default behavior (running checks locally and updating markdown tables). If a hook exists and is executable, the command delegates to it instead.
|
|
|
|
### run-checks
|
|
|
|
**Path**: `spec/hooks/run-checks`
|
|
|
|
**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).
|
|
|
|
**Purpose**: Delegate verification execution to an external system. The agent determines *what* needs checking from the workflow state; the hook tells an external system to *run* the checks, store the results in its own datastore, and report back. This keeps the external system as the independent record-keeper — results are produced by the verification infrastructure, not self-reported by the agent.
|
|
|
|
**Request** (JSON on stdin):
|
|
|
|
```json
|
|
{
|
|
"command": "formspec.6.implement",
|
|
"project_root": "/home/user/projects/mutex",
|
|
"checks": [
|
|
{
|
|
"property": "MutualExclusion",
|
|
"source": "features/2026-02-10-mutex/design.md",
|
|
"requirement": "US-1",
|
|
"type": "invariant",
|
|
"method": "integration test",
|
|
"hint": "go test -race -run TestMutualExclusion ./..."
|
|
}
|
|
]
|
|
}
|
|
```
|
|
|
|
**Request fields**:
|
|
- `command`: Which formspec command is requesting verification.
|
|
- `project_root`: Absolute path to the project root, so the external system can locate source files and specs.
|
|
- `checks`: Array of verification requests:
|
|
- `property`: TLA+ property name (or descriptive label for non-formalized checks).
|
|
- `source`: Design document path relative to `spec/`.
|
|
- `requirement`: Requirement ID (e.g., `US-1`, `SC-3`).
|
|
- `type`: `invariant`, `temporal`, `safety`, `liveness`, `structural`, `compile-time`, `static-analysis`, `unit-test`, or `integration-test`.
|
|
- `method`: Description of the verification method.
|
|
- `hint`: Suggested command or approach. The external system may use this directly, adapt it to its own environment, or ignore it entirely.
|
|
|
|
**Response** (JSON on stdout):
|
|
|
|
```json
|
|
{
|
|
"results": [
|
|
{
|
|
"property": "MutualExclusion",
|
|
"status": "pass",
|
|
"details": "1024 states explored, 0 violations",
|
|
"url": "https://dashboard.example.com/runs/4821#MutualExclusion"
|
|
}
|
|
]
|
|
}
|
|
```
|
|
|
|
**Response fields**:
|
|
- `results`: Array of verification outcomes, one per requested check:
|
|
- `property`: Echoes back the property name from the request.
|
|
- `status`: `pass`, `fail`, or `error`.
|
|
- `details`: Human-readable summary of the result — counterexample, error message, state space size, etc. The agent presents this to the developer.
|
|
- `url`: Optional. Link to the full result in the external system's dashboard. If present, the agent includes it in the report to the developer.
|
|
|
|
**Exit codes**: 0 = all checks executed (individual checks may still have `fail` status). Non-zero = the hook itself failed (could not reach the external system, configuration error, etc.). On non-zero exit, the command warns and falls back to running checks locally and updating the markdown tables.
|
|
|
|
**Behavior when hook is absent**: Commands run checks locally (TLC, `go test`, etc.) and update `spec/formal/traceability.md` and `spec/verification/matrix.md` directly. The markdown tables serve as the built-in, zero-configuration default.
|