chhoumann · Oct 19, 2026 · Oct 18, 2026 · Oct 18, 2026 · Oct 19, 2026 · Oct 19, 2026
diff --git a/.claude-plugin/marketplace.json b/.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-rc.11"
+      "version": "2.0.0-rc.12"
     }
   ]
 }
diff --git a/CHANGES.md b/CHANGES.md
@@ -2,6 +2,18 @@
 
 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.0.0-rc.12 - Lauren's `6b78e9f`: setup offers a formal verification skill, with TLA+ as its default for event order
+
+t3-pstack moves to Lauren Tan's pstack at cursor/plugins `6b78e9f` for all three components. Only pstack changed upstream, and its version stays 0.15.27. `/setup-pstack` gains step 8, which offers once to generate a formal verification skill with `/create-formal-verification-skill` unless the project already has one, worded like step 7's verification offer ([pstack #715](https://github.com/cursor/plugins/pull/715)). poteto-help now mentions `/create-formal-verification-skill` when the project has no formal verification skill and the question is about a race, an invariant, or another case tests rarely hit, and its setup step 2 names both offers. Its recipes gain one for formal verification and one for `/ketchup`. In `/create-formal-verification-skill`, TLA+ is now the default for whether events can happen in a bad order, in any language, and the sentence that called TLA+ often the most useful place to start for concurrent and distributed designs is gone. When no verifier runs on the language, the agent says so and tests the real code with generated inputs, not a hand model of the function ([pstack #721](https://github.com/cursor/plugins/pull/721)). Lauren also split poteto-help's "pstack is built for Cursor" paragraph in two: a Claude Code install through her marketplace and Claude Code adapter, then what other tools can read. The poteto-help rule in `tools/substitutions.json` now matches both paragraphs. Its replacement keeps the sentence that the workflow skills dispatch subagents through `delegate_task` and need a T3 thread, and adds that t3-pstack installs in Claude Code and Codex with `npx -y github:chhoumann/t3-pstack install`. It points at neither Lauren's marketplace nor her adapter, since t3-pstack rewrites the Cursor names in place. The port's copy of poteto-help took the new replacement before the sync, so the three-way merge saw the same change on both sides. `bun tools/sync.mjs` merged step 8 into setup-pstack, a declared fork, cleanly, and the other 14 forks are untouched. It updated `/create-formal-verification-skill` cleanly too, since the port's copy matched upstream byte for byte and no substitution or fork touches it. #715's guide pages under `docs/guide/`, the `third_party/` plugins that #717 and #720 change, and upstream's copies under `harness/pstack/claude-code/` sit outside every synced component. At `6b78e9f` 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-rc.11 | 2.0.0-rc.12 | Source |
+| --- | --- | --- | --- |
+| `/setup-pstack` after the model sheet | Offers a verification skill. | Offers a verification skill, then a formal verification skill. | pstack #715 |
+| poteto-help on a project with no formal verification skill | Says nothing about it. | Mentions `/create-formal-verification-skill` for a race, an invariant, or another case tests rarely hit. | pstack #715 |
+| poteto-help on where t3-pstack runs | Its workflow skills need a T3 thread. | It installs in Claude Code and Codex with `npx`, and its workflow skills need a T3 thread. | pstack #715, `tools/substitutions.json` |
+| poteto-help recipes | No formal verification or `/ketchup` recipe. | One of each. | pstack #715 |
+| `/create-formal-verification-skill` choosing a tool | Calls TLA+ often the most useful place to start for concurrent and distributed designs. | Makes TLA+ the default for event order in any language. With no verifier for the language, the agent says so and tests the real code with generated inputs. | pstack #721 |
+
 ## 2.0.0-rc.11 - Lauren's `0148b78`: sharpen no longer forbids handing back a rewritten prompt
 
 t3-pstack moves to Lauren Tan's pstack at cursor/plugins `0148b78` for all three components. Only pstack changed upstream. Sharpen drops its final sentence, "Don't hand back a rewritten prompt.", so the skill now ends on "without narrating the framing, then do the work." ([pstack #712](https://github.com/cursor/plugins/pull/712)). [pstack #710](https://github.com/cursor/plugins/pull/710) and [#713](https://github.com/cursor/plugins/pull/713) bump Lauren's version to 0.15.26 and then 0.15.27 in her manifests, and upstream's copy under `harness/pstack/claude-code/` follows #712. Both sit outside every synced component. `bun tools/sync.mjs` updated `sharpen/SKILL.md` cleanly. The port's copy matched upstream byte for byte, and no substitution matches its old or new text, since the sentence names no Cursor mechanism. No rule was added, and the 15 declared forks are untouched. At `0148b78` each component's dry run reports no undeclared fork, no denylist hit, and no substitution that matches nothing. Neither hooks file changes.

diff --git a/NOTICE-skills.md b/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/0148b78c56c72a1b8412055913c79f767095b217/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/0148b78c56c72a1b8412055913c79f767095b217/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/0148b78c56c72a1b8412055913c79f767095b217/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/6b78e9f4e46c75d1697d837e51f07c2692e60b24/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/6b78e9f4e46c75d1697d837e51f07c2692e60b24/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/6b78e9f4e46c75d1697d837e51f07c2692e60b24/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) |

diff --git a/NOTICE.md b/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 @ 0148b78](https://github.com/cursor/plugins/tree/0148b78c56c72a1b8412055913c79f767095b217/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 @ 0148b78](https://github.com/cursor/plugins/tree/0148b78c56c72a1b8412055913c79f767095b217/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 @ 0148b78](https://github.com/cursor/plugins/tree/0148b78c56c72a1b8412055913c79f767095b217/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 @ 6b78e9f](https://github.com/cursor/plugins/tree/6b78e9f4e46c75d1697d837e51f07c2692e60b24/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 @ 6b78e9f](https://github.com/cursor/plugins/tree/6b78e9f4e46c75d1697d837e51f07c2692e60b24/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 @ 6b78e9f](https://github.com/cursor/plugins/tree/6b78e9f4e46c75d1697d837e51f07c2692e60b24/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) |

diff --git a/README.md b/README.md
@@ -14,7 +14,7 @@ npx -y github:chhoumann/t3-pstack update
 npx -y github:chhoumann/t3-pstack doctor
 ```
 
-`npx -y github:chhoumann/t3-pstack` runs the installer from the latest commit on `main`. That is the rolling channel, the same one each home's marketplace auto-updates from. To run one release's installer, name its tag, as in `npx -y github:chhoumann/t3-pstack#v2.0.0-rc.11 doctor`.
+`npx -y github:chhoumann/t3-pstack` runs the installer from the latest commit on `main`. That is the rolling channel, the same one each home's marketplace auto-updates from. To run one release's installer, name its tag, as in `npx -y github:chhoumann/t3-pstack#v2.0.0-rc.12 doctor`.
 
 `install` and `update` are the same command, and a second run changes nothing. With Node 20 or later, it installs or updates the `t3-pstack@t3-pstack` plugin in every Claude Code and Codex config home T3 can run: `~/.claude` and `~/.codex`, `$CLAUDE_CONFIG_DIR` and `$CODEX_HOME`, and the home of each `claudeAgent` and `codex` instance in T3's settings, disabled ones included. Name any other home with `--claude-home <dir>` or `--codex-home <dir>`. Each home's `t3-pstack` marketplace must come from `chhoumann/t3-pstack`, or from `--source <owner/repo|git URL|dir>` on the same run, and a home whose marketplace has another source is left as it is. A local directory needs a path such as `./t3-pstack`, since `owner/repo` always means GitHub. On Codex it also trusts t3-pstack's session-start hook, once its hooks file is the one this release pins. Codex runs a plugin's hook only once it is trusted, and T3's Codex sessions never ask, so without this step the hook never runs. Run `update` after each release.
 
@@ -34,7 +34,7 @@ The plugin carries 63 skill directories, 24 of them `principle-*` leaves, and 4
 
 ## Staying current
 
-This repository syncs from Lauren's tree directly, synced against upstream `0148b78`. `tools/upstream.json` pins each component, `tools/substitutions.json` holds the rewrite rules and a denylist of Cursor terms, and `tools/forks.json` declares every file the port keeps in its own form and why. `bun tools/sync.mjs <component> <sha>` derives each upstream file through the rules, merges it three ways with the port's copy, and fails on an undeclared fork, a denylist hit, or a rule that no longer matches upstream. [CONTRIBUTING.md](CONTRIBUTING.md#the-sync-boundary) has the details.
+This repository syncs from Lauren's tree directly, synced against upstream `6b78e9f`. `tools/upstream.json` pins each component, `tools/substitutions.json` holds the rewrite rules and a denylist of Cursor terms, and `tools/forks.json` declares every file the port keeps in its own form and why. `bun tools/sync.mjs <component> <sha>` derives each upstream file through the rules, merges it three ways with the port's copy, and fails on an undeclared fork, a denylist hit, or a rule that no longer matches upstream. [CONTRIBUTING.md](CONTRIBUTING.md#the-sync-boundary) has the details.
 
 ## Data handling
 

diff --git a/VERSION b/VERSION
@@ -1 +1 @@
-2.0.0-rc.11
+2.0.0-rc.12
diff --git a/package.json b/package.json
@@ -1,7 +1,7 @@
 {
   "name": "t3-pstack",
   "private": true,
-  "version": "2.0.0-rc.11",
+  "version": "2.0.0-rc.12",
   "description": "The installer and development tooling for t3-pstack, Lauren Tan's pstack rewritten in place for T3 Code. The plugin itself lives in plugins/pstack.",
   "author": {
     "name": "Christian Bager Bach Houmann",

diff --git a/plugins/pstack/.claude-plugin/plugin.json b/plugins/pstack/.claude-plugin/plugin.json
@@ -1,7 +1,7 @@
 {
   "name": "t3-pstack",
   "displayName": "t3-pstack (pstack for T3 Code)",
-  "version": "2.0.0-rc.11",
+  "version": "2.0.0-rc.12",
   "description": "pstack for T3 Code: Lauren Tan's pstack with its Cursor mechanics rewritten in place for T3, so subagents, panels, schedules, and PR watches dispatch through T3's orchestration and panels mix Claude, GPT, and Grok.",
   "author": {
     "name": "Christian Bager Bach Houmann",

diff --git a/plugins/pstack/.codex-plugin/plugin.json b/plugins/pstack/.codex-plugin/plugin.json
@@ -1,6 +1,6 @@
 {
   "name": "t3-pstack",
-  "version": "2.0.0-rc.11",
+  "version": "2.0.0-rc.12",
   "description": "pstack for T3 Code on a Codex host: Lauren Tan's pstack with its Cursor mechanics rewritten in place for T3, so subagents, panels, schedules, and PR watches dispatch through T3's orchestration.",
   "author": {
     "name": "Christian Bager Bach Houmann",

diff --git a/plugins/pstack/skills/create-formal-verification-skill/SKILL.md b/plugins/pstack/skills/create-formal-verification-skill/SKILL.md
@@ -1,3 +1,3 @@
 ---
 name: create-formal-verification-skill
 description: "Generate a project-local skill that formally verifies the code where a bug costs the most and tests reach the least, in any language, with whichever verification tool fits. Use for /create-formal-verification-skill, \"model-check this race\", \"prove this invariant\", or when concurrency, retries, state machines, parsers, or unsafe code need more than tests."
@@ -16,7 +16,7 @@
 
 ## Let the question choose the tool
 
-Pick the tool that answers the question at the lowest cost: a model checker, a proof assistant, an SMT-backed verifier, or another tool. Whether events can happen in a bad order usually suits a model checker over a small model of the design. Whether the code itself behaves for every input, as with memory safety, overflow, or a data-structure invariant, usually suits a verifier that runs on the code. A property that must hold at every size, where a bound is not enough, can need a proof. For concurrent and distributed designs, TLA+ is often the most useful place to start. Prefer a tool that the repo's developers can install and run, and tell the user why you chose it.
+Pick the tool that answers the question at the lowest cost: a model checker, a proof assistant, an SMT-backed verifier, or another tool. Whether events can happen in a bad order usually suits a model checker over a small model of the design, and TLA+ is the default for that in any language. Whether the code itself behaves for every input, as with memory safety, overflow, or a data-structure invariant, usually suits a verifier that runs on the code. If no verifier runs on this language, say so, and test the real code with generated inputs, not a hand model of the function. A property that must hold at every size, where a bound is not enough, can need a proof. Prefer a tool that the repo's developers can install and run, and tell the user why you chose it.
 
 ## What makes it good