Release 2.1.0: sync Lauren's pstack to 519d36a (statechart compiler)

.claude-plugin/marketplace.json

@@ -10,7 +10,7 @@
       "name": "t3-pstack",
       "source": "./plugins/pstack",
       "description": "pstack for T3 Code: rigorous agent workflows whose panels and fan-outs run across model families through T3. Original pstack by Lauren Tan (poteto).",
-      "version": "2.0.0"
+      "version": "2.1.0"
     }
   ]
 }

.github/workflows/ci.yml

@@ -127,9 +127,13 @@ jobs:
       - name: Check formatting
         run: bunx prettier@3.6.2 --check watch-pr/settle.ts watch-pr/settle.test.ts watch-pr/verdicts.test.ts resolve-codex-transcript.ts
 
-  # The same step as upstream's validate-plugins.yml, on the Node it uses,
-  # which is also the oldest the installer accepts. The runner has no TLC, so
-  # the statechart tests that need it skip.
+  # The same test step as upstream's validate-plugins.yml, on the Node 22 it
+  # uses, the oldest line the statechart launcher runs TypeScript on.
+  # Upstream installs fast-check outside a lockfile, so the root bun.lock
+  # pins the version the statechart scripts' package.json names. node --test
+  # passes on a glob that matches nothing, so failglob fails the step
+  # instead. The runner has no TLC, so the statechart tests that need it
+  # skip.
   skill-scripts:
     name: Skill script tests
     runs-on: ubuntu-latest
@@ -139,9 +143,16 @@ jobs:
           persist-credentials: false
       - uses: actions/setup-node@949feb2413d6458794dcd2491c4babbbce0c15c1 # v7.1.0
         with:
-          node-version: "20"
+          node-version: "22"
+      - uses: oven-sh/setup-bun@0c5077e51419868618aeaa5fe8019c62421857d6 # v2.2.0
+        with:
+          bun-version: "1.4.4"
+      - name: Install dependencies
+        run: bun install --frozen-lockfile
       - name: Test skill scripts
-        run: node --test plugins/pstack/skills/*/scripts/test/*.test.mjs
+        run: |
+          shopt -s failglob
+          node --disable-warning=ExperimentalWarning --test plugins/pstack/skills/*/scripts/test/*.test.ts
 
   shellcheck:
     name: Shell scripts

CHANGES.md

@@ -2,6 +2,34 @@
 
 This file is the release changelog, with one `## <version> - <title>` entry per release, newest first. The Cursor-to-T3 rewrite rules live in [`tools/substitutions.json`](tools/substitutions.json), and the [sync boundary](CONTRIBUTING.md#the-sync-boundary) in `CONTRIBUTING.md` defines how a change to upstream's skill content is declared.
 
+## 2.1.0 - Lauren's `519d36a`: statechart becomes one command that checks a TLA+ model and charts it
+
+t3-pstack moves to Lauren Tan's pstack at cursor/plugins `519d36a` for all three components. Only pstack changed upstream, and its version moves to 0.15.34. The `statechart` skill's Node scripts give way to Lauren's TypeScript compiler ([pstack #977](https://github.com/cursor/plugins/pull/977)). One command, `<skill dir>/scripts/statechart SPEC.tla [--config FILE] [--view FILE] [--out DIR]`, checks the model with TLC, draws its state graph as a Mermaid statechart, and writes a `report.md` with the shortest path to each rule that breaks. The reader's words live in a view module given with `--view`. Its `state(vars)` returns a string for a flat chart, an array for parent states, or an object for parallel regions, and it can also export `step`, `group`, `colors`, and `title`. TLC checks the config as written with one worker. When a rule breaks, the command drops it and runs TLC again until none breaks, each later run stops at 100,000 distinct states, and the report lists each rule it could not check. Above 500 states the chart draws only the bug paths, and with no broken rule it writes no `chart.mmd`. The exit code is TLC's on the config as written: 0 when every rule holds, 1 when a rule breaks, and 2 when TLC stops with an error, a signal kills the check, or the command cannot run, with 130 or 143 on SIGINT or SIGTERM. Only exits 0 and 1 write output, into a folder that must be new or empty. `scripts/statechart` is a POSIX launcher that runs `statechart.ts` with no build step on Node 22.18 to 22.x or 23.6 and later, else on Bun 1.1.5 or later, else on Deno 2.0 or later, and exits 127 naming them when `PATH` has none. Because the launcher is an `sh` script and the compiler stops TLC's process group through `/bin/sh`, the skill does not run on native Windows. That comes from reading the source, and no Windows host ran it. The installer still accepts Node 20, so a host on Node 20 or 21 needs Bun or Deno for this skill. TLC still comes from mise on the first run, or from `TLA2TOOLS` and `JAVA`. A broken temporal property's report keeps the path TLC found when an action comes from an `INSTANCE`d module, where it used to lose the path while the verdict and exit code stayed right ([pstack #982](https://github.com/cursor/plugins/pull/982)). `references/render.md` says how to render each chart as an SVG with `pele@1.9.0`, with a light and dark theme for the group and mark classes.
+
+The compiler drops these capabilities of the old skill, and 2.1.0 has nothing in their place:
+
+- `from-chart`, which turned a chart the reader agreed to into a TLA+ skeleton and compared the two, and `render CHART.mmd`, which drew such a chart.
+- `--against` and `--against-config`, which audited a model of the code against an existing spec and said whether the spec already expects each bug.
+- `--fixed` and `--fixed-config`, which colored the states that a proposed fix repairs. With `--fixed` or `--against`, the run also listed each action condition that no `\* file:line` comment tied to code.
+- `--png` and its `--theme`, which wrote a PNG of each chart through Pele and resvg. `references/render.md` gives the SVG steps instead.
+- `--cover`, `--expect-broken`, the mapping file with its `readerActions`, `cause`, and `detail`, and the `stories.md` and `summary.json` outputs.
+- The per-bug charts `bug-N.mmd`, `bug-N-developer.mmd`, and `bug-N-layered.mmd`, and the `tlc/` folder with its `regions-all.mmd` and `regions-proof.mmd` and the `compare-charts.mjs` check between them.
+
+`create-formal-verification-skill` no longer says that `/statechart` shows which violations a change fixes, and poteto-help's row now reads "Show a PM or designer what the user sees as a chart checked by a TLA+ model, with the shortest path to each state that breaks a rule". The skill keeps Lauren's `disable-model-invocation`, so on Claude Code it runs when the user types `/t3-pstack:statechart`. On Codex it is `$t3-pstack:statechart`, and Codex ignores the flag. `bun tools/sync.mjs` added 396 files, deleted 26, and updated 3 cleanly through existing substitutions. The new text names no Cursor tool, path, model, command, or subagent, so no rule was added, and the 15 declared forks are untouched. The `statechart` directory is byte-identical to upstream, and the launcher keeps mode 100755. `<skill dir>` needs no rule. Claude Code names a skill's base directory when it loads the skill, and in a throwaway home `codex debug prompt-input` on Codex 0.164 lists the skill as `r1/statechart/SKILL.md`, where `r1` is the installed plugin's `skills` folder. The installer put this release into a throwaway home's Claude Code 2.1.311 and Codex 0.164 from a clean clone, and both installed copies of the skill match the checkout byte for byte, the launcher at mode 755. Run from either installed path with TLC 1.7.4 and Java 21, a door model with two rules, whose lock does not stop the door opening, exits 1 with the two-step path to the broken rule and the other rule holding. Its fixed model exits 0 with both rules holding and a three-state chart. The same run on a `PATH` with only Bun writes the same chart and report. With no mise and no `TLA2TOOLS`, the command exits 2 with `Cannot find TLC: mise install failed: spawn mise ENOENT` and how to set `TLA2TOOLS` and `JAVA`, and writes nothing. #978 bumps upstream's manifests, and #977's README row, guide page, and copies under `harness/pstack/claude-code/` sit outside every synced component.
+
+Skill script tests follows upstream's CI change. It runs on Node 22, installs fast-check 4.5.3, the version the statechart scripts' `package.json` names, from the root `bun.lock`, and runs `node --test` on `plugins/pstack/skills/*/scripts/test/*.test.ts`. `node --test` passes on a glob that matches nothing, and the old `*.test.mjs` glob now would, so the step sets bash's `failglob`. On macOS, one test used to fail: after a SIGKILL it probed the killed process group once with `kill(-pgid, 0)` and expected ESRCH, where macOS returns EPERM until the zombies are reaped. [pstack #981](https://github.com/cursor/plugins/pull/981) makes it wait for the reap. The README's skill count stays at 66. At `519d36a` each component's dry run reports no undeclared fork, no denylist hit, and no substitution that matches nothing. Neither hooks file changes.
+
+| Change | 2.0.0 | 2.1.0 | Source |
+| --- | --- | --- | --- |
+| Running `statechart` | `node <skill dir>/scripts/statechart.mjs` with `from-spec` or `from-chart`. | `<skill dir>/scripts/statechart SPEC.tla`, one command on Node 22.18 to 22.x or 23.6+, Bun 1.1.5+, or Deno 2.0+. | pstack #977 |
+| The reader's labels | A mapping file that `from-spec` writes. | A view module given with `--view`. | pstack #977 |
+| A chart the reader agreed to, as a TLA+ skeleton | `from-chart`. | None. | pstack #977 |
+| Auditing the code's model against an existing spec | `--against`. | None. | pstack #977 |
+| What a proposed fix repairs | `--fixed` colors the repaired states. | None. | pstack #977 |
+| A chart as an image | `--png` writes a PNG through Pele and resvg. | `references/render.md` gives the steps for an SVG through Pele. | pstack #977 |
+| A large overview | `--cover` trims it to the shortest path to each settled state plus every bug path. | Above 500 states the chart draws only the bug paths, or nothing when no rule breaks. | pstack #977 |
+| CI's Skill script tests | `*.test.mjs` on Node 20. | `*.test.ts` on Node 22 with fast-check, failing when the glob matches nothing. | pstack #977 |
+
 ## 2.0.0 - t3-pstack 2.0: Lauren's pstack, rewritten for T3
 
 2.0.0 is 2.0.0-rc.19 under its final version, with no change to any skill, script, or hooks file. The 2.0 line rebuilds t3-pstack on Lauren Tan's pstack at cursor/plugins, now at `e73df47` (pstack 0.15.32), with Cursor-specific text rewritten in place for T3 on Claude Code and Codex. The release candidates rc.1 to rc.19 below record each step. From here on, each sync of Lauren's pstack ships as a patch or minor release under semantic versioning, as [`CONTRIBUTING.md`](CONTRIBUTING.md#releasing) describes, and each release gets a GitHub release with its entry as notes.

CONTRIBUTING.md

@@ -89,7 +89,7 @@ uvx zizmor@1.29.0 --persona pedantic --min-severity low --collect all -- .
 
 ## Dependency updates
 
-Dependabot keeps the pinned action SHAs current. The vendored scripts' one runtime dependency (`commander`) follows upstream's pin and moves with `tools/sync.mjs`. `osv-scanner` scans every `bun.lock` weekly. The root `bun.lock` pins `typebox`, which the generator uses to check the hooks files.
+Dependabot keeps the pinned action SHAs current. The vendored scripts' one runtime dependency (`commander`) follows upstream's pin and moves with `tools/sync.mjs`. `osv-scanner` scans every `bun.lock` weekly. The root `bun.lock` pins `typebox`, which the generator uses to check the hooks files, and `fast-check`, which the statechart tests import. Upstream installs fast-check in CI without a lockfile, so when the statechart scripts' `package.json` moves its version, move the root pin with it.
 
 ## Releasing
 

NOTICE-skills.md

@@ -4,9 +4,9 @@ This plugin contains MIT-licensed work from six sources. The copyright notices a
 
 | Included work | Upstream | Copyright | License |
 | --- | --- | --- | --- |
-| The pstack skills, principles, scripts, and the `poteto-agent` and `comment-sicko` definitions | [cursor/plugins/pstack](https://github.com/cursor/plugins/tree/e73df471cd4bd918367e99f3dd9c51bd53ddf5f0/pstack) | (c) 2026 Lauren Tan | [MIT](LICENSE) |
-| `deslop`, `make-pr-easy-to-review`, `fix-ci`, `fix-merge-conflicts`, `get-pr-comments`, and `what-did-i-get-done` | [cursor/plugins/cursor-team-kit](https://github.com/cursor/plugins/tree/e73df471cd4bd918367e99f3dd9c51bd53ddf5f0/cursor-team-kit) | (c) 2026 Cursor | [MIT](LICENSE-cursor-team-kit) |
-| `thermos`, `thermo-nuclear-review`, `thermo-nuclear-code-quality-review`, and the `thermo-nuclear-review-subagent` and `thermo-nuclear-code-quality-review-subagent` definitions | [cursor/plugins/thermos](https://github.com/cursor/plugins/tree/e73df471cd4bd918367e99f3dd9c51bd53ddf5f0/thermos) | (c) 2026 Cursor | [MIT](LICENSE-thermos) |
+| The pstack skills, principles, scripts, and the `poteto-agent` and `comment-sicko` definitions | [cursor/plugins/pstack](https://github.com/cursor/plugins/tree/519d36aa98955bf680db01bcde5fdfba686dc901/pstack) | (c) 2026 Lauren Tan | [MIT](LICENSE) |
+| `deslop`, `make-pr-easy-to-review`, `fix-ci`, `fix-merge-conflicts`, `get-pr-comments`, and `what-did-i-get-done` | [cursor/plugins/cursor-team-kit](https://github.com/cursor/plugins/tree/519d36aa98955bf680db01bcde5fdfba686dc901/cursor-team-kit) | (c) 2026 Cursor | [MIT](LICENSE-cursor-team-kit) |
+| `thermos`, `thermo-nuclear-review`, `thermo-nuclear-code-quality-review`, and the `thermo-nuclear-review-subagent` and `thermo-nuclear-code-quality-review-subagent` definitions | [cursor/plugins/thermos](https://github.com/cursor/plugins/tree/519d36aa98955bf680db01bcde5fdfba686dc901/thermos) | (c) 2026 Cursor | [MIT](LICENSE-thermos) |
 | The session-start hook scripts, `read-sheet.sh`, and `reflect/scripts/find-transcript.mjs`, which t3-pstack modified, and four `poteto-mode` rules, the worktree and head-guard rules in the Feature, Opening a PR, and Shipping playbooks, three `watch-pr` fixes, and the ignored-file and reflog-only-commit holds in `poteto-mode/scripts/worktree-audit.sh`, which t3-pstack reworded or adapted for T3, and the plugin icon | [michael-denyer/pstack-claude](https://github.com/michael-denyer/pstack-claude) | (c) 2026 Michael Denyer | [MIT](LICENSE) |
 | The plain-remove prune step in the worktree-cleanup playbook, which t3-pstack adapted | [sergchil/jutsu](https://github.com/sergchil/jutsu/commit/da9442422c72cc99442c1ce3500d2f2485234a31) | (c) 2026 Sergey Chilingaryan | [MIT](LICENSE) |
 | `poteto-mode/scripts/resolve-codex-transcript` and `resolve-codex-transcript.ts`, which t3-pstack modified | [ericlitman/open-pstack](https://github.com/ericlitman/open-pstack/tree/c5c8e237c324359a3d1929037da78fe66da3d1ed/plugins/pstack/skills/poteto-mode/scripts), [PR #151](https://github.com/ericlitman/open-pstack/pull/151) | (c) 2026 Eric A. Litman and Donncha O'Toole | [MIT](LICENSE) |

NOTICE.md

@@ -6,9 +6,9 @@ t3-pstack is a port of [pstack](https://github.com/cursor/plugins/tree/main/psta
 
 | Component | Upstream | Copyright | License | License file |
 | --- | --- | --- | --- | --- |
-| Every skill under `plugins/pstack/skills/` except those named in the next two rows, `plugins/pstack/agents/poteto-agent.md`, `plugins/pstack/agents/comment-sicko.md`, and the vendored scripts under `plugins/pstack/skills/poteto-mode/scripts/` | [cursor/plugins/pstack @ e73df47](https://github.com/cursor/plugins/tree/e73df471cd4bd918367e99f3dd9c51bd53ddf5f0/pstack) | (c) 2026 Lauren Tan | MIT | [LICENSE](LICENSE) |
-| `plugins/pstack/skills/{deslop,fix-ci,fix-merge-conflicts,get-pr-comments,make-pr-easy-to-review,what-did-i-get-done}/` | [cursor/plugins/cursor-team-kit @ e73df47](https://github.com/cursor/plugins/tree/e73df471cd4bd918367e99f3dd9c51bd53ddf5f0/cursor-team-kit) | (c) 2026 Cursor | MIT | [LICENSE-cursor-team-kit](LICENSE-cursor-team-kit) |
-| `plugins/pstack/skills/{thermos,thermo-nuclear-review,thermo-nuclear-code-quality-review}/`, `plugins/pstack/agents/thermo-nuclear-review-subagent.md`, `plugins/pstack/agents/thermo-nuclear-code-quality-review-subagent.md` | [cursor/plugins/thermos @ e73df47](https://github.com/cursor/plugins/tree/e73df471cd4bd918367e99f3dd9c51bd53ddf5f0/thermos) | (c) 2026 Cursor | MIT | [LICENSE-thermos](LICENSE-thermos) |
+| Every skill under `plugins/pstack/skills/` except those named in the next two rows, `plugins/pstack/agents/poteto-agent.md`, `plugins/pstack/agents/comment-sicko.md`, and the vendored scripts under `plugins/pstack/skills/poteto-mode/scripts/` | [cursor/plugins/pstack @ 519d36a](https://github.com/cursor/plugins/tree/519d36aa98955bf680db01bcde5fdfba686dc901/pstack) | (c) 2026 Lauren Tan | MIT | [LICENSE](LICENSE) |
+| `plugins/pstack/skills/{deslop,fix-ci,fix-merge-conflicts,get-pr-comments,make-pr-easy-to-review,what-did-i-get-done}/` | [cursor/plugins/cursor-team-kit @ 519d36a](https://github.com/cursor/plugins/tree/519d36aa98955bf680db01bcde5fdfba686dc901/cursor-team-kit) | (c) 2026 Cursor | MIT | [LICENSE-cursor-team-kit](LICENSE-cursor-team-kit) |
+| `plugins/pstack/skills/{thermos,thermo-nuclear-review,thermo-nuclear-code-quality-review}/`, `plugins/pstack/agents/thermo-nuclear-review-subagent.md`, `plugins/pstack/agents/thermo-nuclear-code-quality-review-subagent.md` | [cursor/plugins/thermos @ 519d36a](https://github.com/cursor/plugins/tree/519d36aa98955bf680db01bcde5fdfba686dc901/thermos) | (c) 2026 Cursor | MIT | [LICENSE-thermos](LICENSE-thermos) |
 | `tools/sync.mjs`, `tools/generate.mjs`, `tools/validate-skills.mjs`, `tools/plugin.mjs`, `plugins/pstack/skills/reflect/scripts/find-transcript.mjs`, `plugins/pstack/hooks/session-start.sh`, `plugins/pstack/hooks/session-start.ps1`, `plugins/pstack/skills/setup-pstack/scripts/read-sheet.sh`, and the tests that cover them, each modified by t3-pstack | [michael-denyer/pstack-claude](https://github.com/michael-denyer/pstack-claude), as merged into t3-pstack through 1.0.14 | (c) 2026 Michael Denyer | MIT | [LICENSE](LICENSE) |
 | Four rules in `plugins/pstack/skills/poteto-mode/SKILL.md` (load a platform's skill before deploying, stop an abandoned agent and confirm it stopped, keep a review gate closed with no independent reviewer, the `todo.md` fallback), the per-delegate worktree rule in `playbooks/feature.md`, the stop-live-agents rule in `playbooks/opening-a-pr.md`, the `--match-head-commit` guard in `playbooks/shipping.md`, and the review-gate, stale-check, and no-checks fixes in `plugins/pstack/skills/poteto-mode/scripts/watch-pr/` with their tests in `verdicts.test.ts`, each reworded or adapted for T3 by t3-pstack | [michael-denyer/pstack-claude](https://github.com/michael-denyer/pstack-claude), pull requests [#95](https://github.com/michael-denyer/pstack-claude/pull/95), [#97](https://github.com/michael-denyer/pstack-claude/pull/97), and [#153](https://github.com/michael-denyer/pstack-claude/pull/153) for watch-pr | (c) 2026 Michael Denyer | MIT | [LICENSE](LICENSE) |
 | The ignored-file and reflog-only-commit holds in `plugins/pstack/skills/poteto-mode/scripts/worktree-audit.sh`, ported from JavaScript to bash, and their wording in `playbooks/worktree-cleanup.md`, with the test cases in `tests/worktree-audit.test.mjs`; the plugin icon with its C2PA manifest removed (`plugins/pstack/.claude-plugin/icon.png`, `plugins/pstack/assets/pstack-icon.png`) and `tests/image-metadata.test.mjs` | [michael-denyer/pstack-claude](https://github.com/michael-denyer/pstack-claude), pull requests [#277](https://github.com/michael-denyer/pstack-claude/pull/277) and [#271](https://github.com/michael-denyer/pstack-claude/pull/271) | (c) 2026 Michael Denyer | MIT | [LICENSE](LICENSE) |