Create an optional hook system for externally-managed verification

.claude/commands/formspec.init.0.md

@@ -32,6 +32,7 @@ Create the following directories:
 spec/formal/subsystems/
 spec/features/
 spec/verification/
+spec/hooks/
 ```
 
 ### 4. Generate spec/system.md
@@ -63,3 +64,75 @@ The System Overview should be a concise but complete description — enough for
 ### 5. Report
 
 Tell the user what was created and suggest they proceed with `/formspec.design.1 <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.formalize`, `/formspec.verify`, `/formspec.implement`, `/formspec.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.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.