libohad-dev/dotfiles
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fix instruction order in the spec-formalization step

Browse source
This commit is contained in:
Ohad Livne 2026-02-28 08:55:16 +02:00
parent de599d1850
commit eeb5e6159e
Signed by: libohad-dev
GPG key ID: 34FDC68B51191A4D
1 changed files with 5 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

11
.claude/commands/formspec.formalize.2.md
View file

@ -85,7 +85,10 @@ Every requirement from Phase 1 must appear in this table. If a requirement canno
## Phase 4 — Run TLC model checker ## 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 ```bash
tlc spec/formal/System.tla -config spec/formal/System.cfg -workers auto -metadir /tmp/tlc-states -cleanup 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 ### 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. 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.
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.
### Meaning drift detected (Phase 2 issue) ### Meaning drift detected (Phase 2 issue)