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