diff --git a/.claude/commands/formspec.formalize.2.md b/.claude/commands/formspec.formalize.2.md
index a4d20f5..a45376c 100644
--- a/.claude/commands/formspec.formalize.2.md
+++ b/.claude/commands/formspec.formalize.2.md
@@ -85,7 +85,10 @@ Every requirement from Phase 1 must appear in this table. If a requirement canno
 
 ## Phase 4 — Run TLC model checker
 
-Run:
+If `spec/hooks/run-checks` exists and is executable, delegate TLC verification to it instead of running locally (see `/formspec.init` for the hook interface). Present the returned results to the developer, including any dashboard URLs, and skip to Phase 5.
+
+If the hook does not exist or fails, run TLC locally:
+
 ```bash
 tlc spec/formal/System.tla -config spec/formal/System.cfg -workers auto -metadir /tmp/tlc-states -cleanup
 ```
@@ -113,11 +116,7 @@ Parse the TLC output to determine:
 
 ### All properties pass
 
-If `spec/hooks/run-checks` exists and is executable, delegate TLC verification to it instead of running TLC locally (see `/formspec.init` for the hook interface). Present the returned results to the developer, including any dashboard URLs.
-
-If the hook does not exist or fails, run TLC locally as described in Phase 4.
-
-In either case, update all statuses in `spec/formal/traceability.md` from `formalized` to `checked`. Report success with a summary of what was verified: number of properties checked, state space explored, time taken. Suggest proceeding with `/formspec.plan.4` to create an implementation plan.
+Update all statuses in `spec/formal/traceability.md` from `formalized` to `checked`. Report success with a summary of what was verified: number of properties checked, state space explored, time taken. Suggest proceeding with `/formspec.plan.4` to create an implementation plan.
 
 ### Meaning drift detected (Phase 2 issue)