diff --git a/.claude-plugin/marketplace.json b/.claude-plugin/marketplace.json index 129b5692..afe18629 100644 --- 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.13" + "version": "2.0.0-rc.14" } ] } diff --git a/CHANGES.md b/CHANGES.md index b034ae9f..b0eb93d1 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -2,6 +2,15 @@ This file is the release changelog, with one `## - ` 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.14 - Lauren's `d457567`: a skill that brings formal verification back in line with the code + +t3-pstack moves to Lauren Tan's pstack at cursor/plugins `d457567` for all three components. Only pstack changed upstream, and its version moves to 0.15.28. The new `maintain-formal-verification-skill` is the upkeep loop for a verify skill that `/create-formal-verification-skill` generated, or for any project skill that runs a verifier against named code ([pstack #716](https://github.com/cursor/plugins/pull/716)). It reads every commit that touched the covered code since the commit the skill records as last in sync, updates the model, harness, or properties from the code before it reruns, and breaks each updated check on purpose to show it can still fail. It reports each check as in sync, updated, bug, or blocked, replays each counterexample against the real code to tell drift in the verification from a bug in the code, and never edits product code or weakens a property to make it pass. It keeps Lauren's `disable-model-invocation`, so on Claude Code it runs when the user types `/t3-pstack:maintain-formal-verification-skill`. On Codex it is `$t3-pstack:maintain-formal-verification-skill`, and Codex ignores the flag. `/create-formal-verification-skill` now records which files and functions each check covers and the commit at which the verification last described them, tells the next agent to move that commit forward only after it confirms the verification, and points at the new skill in its hand-off. poteto-help gains its row and mentions it when covered code changed after the recorded commit, and its recipes gain a pointer. `bun tools/sync.mjs` added the skill and updated `/create-formal-verification-skill`, poteto-help, and the recipes cleanly through existing substitutions. The new skill names no Cursor tool, path, model, command, or subagent, so no rule was added, and the 15 declared forks are untouched. The README's skill count moves to 64. #724's guide pages and upstream's README row sit outside every synced component. At `d457567` 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.13 | 2.0.0-rc.14 | Source | +| --- | --- | --- | --- | +| Formal verification upkeep | No skill. A generated verify skill rechecks a change made while an agent uses it. | `/maintain-formal-verification-skill` reads the commits since the recorded sync commit, updates the verification from the code, proves each updated check can still fail, and calls each failure drift or a bug. | pstack #716 | +| Generated formal verify skill | Something tells the next agent when verified code changes. | Records the covered files and functions and the commit last confirmed in sync, and moves that commit only after the verification is confirmed. | pstack #716 | + ## 2.0.0-rc.13 - poteto-help: one installer run covers every home, and Codex skill names carry `t3-pstack:` Two lines in poteto-help were wrong, and both came from the port's own rules in `tools/substitutions.json`, not from Lauren. Setup step 1 told users to install t3-pstack once per harness that T3 runs. One `npx -y github:chhoumann/t3-pstack install` run installs it in every Claude Code and Codex config home T3 can run, as the README's "Install, update, and check" says, and step 1 now says so. The line on skill names by harness gave Codex's form as `$poteto-mode`. Codex names a plugin's skills with the plugin prefix: after a throwaway-HOME install, the Codex 0.163.0 app-server's `skills/list` returns `t3-pstack:poteto-mode`, `t3-pstack:poteto-help`, and `t3-pstack:setup-pstack`. The line now reads `$t3-pstack:poteto-mode`, as the README does. Both rules and the port's copy of poteto-help changed together. No other skill, playbook, hook, README line, or rule writes a bare `$<skill>` or a per-harness install. The pins stay at Lauren's `6b78e9f`, where 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 index 7b429863..f2823f7f 100644 --- 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/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 pstack skills, principles, scripts, and the `poteto-agent` and `comment-sicko` definitions | [cursor/plugins/pstack](https://github.com/cursor/plugins/tree/d457567332aa6989e753ea289f30ea2bfbc80bc0/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/d457567332aa6989e753ea289f30ea2bfbc80bc0/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/d457567332aa6989e753ea289f30ea2bfbc80bc0/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 index b501e0d2..18a515c1 100644 --- 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 @ 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) | +| 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 @ d457567](https://github.com/cursor/plugins/tree/d457567332aa6989e753ea289f30ea2bfbc80bc0/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 @ d457567](https://github.com/cursor/plugins/tree/d457567332aa6989e753ea289f30ea2bfbc80bc0/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 @ d457567](https://github.com/cursor/plugins/tree/d457567332aa6989e753ea289f30ea2bfbc80bc0/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 index 75e75a8c..1c45f31f 100644 --- 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.13 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.14 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. @@ -30,11 +30,11 @@ Use poteto-mode to fix the search filter resetting when I change pages. The session-start hook tells each new chat when to enter `poteto-mode` on its own: work that touches more than one file, a design choice, or a bug whose cause is unknown. `poteto-mode` matches the task to a playbook and opens the other skills from there. They ship as upstream ships them, invoked by `poteto-mode` or typed by you (`/t3-pstack:<name>` on Claude Code, `$t3-pstack:<name>` on Codex). -The plugin carries 63 skill directories, 24 of them `principle-*` leaves, and 4 agents. +The plugin carries 64 skill directories, 24 of them `principle-*` leaves, and 4 agents. ## Staying current -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. +This repository syncs from Lauren's tree directly, synced against upstream `d457567`. `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 index 3b229186..c38333cf 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -2.0.0-rc.13 +2.0.0-rc.14 diff --git a/package.json b/package.json index ab3085a9..6c3efbd3 100644 --- a/package.json +++ b/package.json @@ -1,7 +1,7 @@ { "name": "t3-pstack", "private": true, - "version": "2.0.0-rc.13", + "version": "2.0.0-rc.14", "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 index ca0d7bbf..4ce8bddb 100644 --- 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.13", + "version": "2.0.0-rc.14", "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 index a4ccc354..3b968db4 100644 --- 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.13", + "version": "2.0.0-rc.14", "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 index 893f6042..b97609fd 100644 --- a/plugins/pstack/skills/create-formal-verification-skill/SKILL.md +++ b/plugins/pstack/skills/create-formal-verification-skill/SKILL.md @@ -26,11 +26,11 @@ Pick the tool that answers the question at the lowest cost: a model checker, a p - **Honest about scope.** Say what is verified, under which bounds and assumptions, and what is left out. A pass covers the model or the bound, not the whole system. - **Readable without the tool.** State the property and the harm in one plain sentence each. Tell a counterexample as a short sequence of steps in the code's words. - **Cheap to rerun.** One command, a reproducible tool version, and a run short enough that the next agent will use it on every relevant change. -- **Kept in step with the code.** When verified code changes, something tells the next agent that the verification needs another look. +- **Kept in step with the code.** Record which files and functions each check covers, and the commit at which you last confirmed that the verification describes them. When the covered code changes after that commit, the next agent can see that the verification needs another look. ## Generate the verify skill -Write a project-local skill with frontmatter that names the area and says when to use it. Without frontmatter, the skill never registers. From the skill alone, the next agent must be able to tell whether a change touches the verified code, run the check, tell a real bug from a modeling error, and update the verification when a change is intended. Use this repo's real commands, paths, and nouns, and leave no placeholders. +Write a project-local skill with frontmatter that names the area and says when to use it. Without frontmatter, the skill never registers. From the skill alone, the next agent must be able to tell whether a change touches the verified code, run the check, tell a real bug from a modeling error, and update the verification when a change is intended. Put the coverage record and the sync commit in the skill, and tell the next agent to move the sync commit forward only after it confirms that the verification describes the code at the new commit. Use this repo's real commands, paths, and nouns, and leave no placeholders. ## Prove it before you hand off @@ -38,4 +38,4 @@ Follow the generated skill once, as the next agent would, on a scratch change th ## Hand off -Tell the user what you verified, which tool you used and why, the bounds, what the check found in plain words, how to run it, and what it does not cover. Suggest a second target only if you found a close one. +Tell the user what you verified, which tool you used and why, the bounds, what the check found in plain words, how to run it, and what it does not cover. Suggest a second target only if you found a close one. Point the user at `/maintain-formal-verification-skill` for bringing the verification back in line after changes that did not recheck it. diff --git a/plugins/pstack/skills/maintain-formal-verification-skill/SKILL.md b/plugins/pstack/skills/maintain-formal-verification-skill/SKILL.md new file mode 100644 index 00000000..5d2f7f22 --- /dev/null +++ b/plugins/pstack/skills/maintain-formal-verification-skill/SKILL.md @@ -0,0 +1,58 @@ +--- +name: maintain-formal-verification-skill +description: "Bring a project's formal verification back in line with the code after the code changes: find the commits that touched verified code, update the model, harness, or properties to describe the code as it is now, rerun, and say whether each failure is drift in the verification or a bug in the code. Use for /maintain-formal-verification-skill, \"is the model still true to the code\", or after merges and refactors that touched verified code without rechecking it." +disable-model-invocation: true +--- + +# Maintain a formal verification skill + +A formal check proves a property of what it describes. When the code changes and the verification does not, the check can keep passing while it describes code that no longer exists. That pass is the dangerous case, because it looks like a proof. This skill is the upkeep loop for a verify skill that `/create-formal-verification-skill` generated, or for any project-local skill that runs a model checker, prover, or code-level verifier against named code. The project-local skill handles a change that an agent makes while it uses that skill. This skill handles the changes that skipped it: merges, edits made without the skill, and drift that builds up across many commits. + +## Outcomes + +Give each check one outcome, and say which: + +- **in sync**: no change since the last sync alters what the check describes, and the check passes. +- **updated**: the code changed, the verification now describes the new code, and the check passes. +- **bug**: the verification describes the current code, and the code breaks the property. This is a finding about the code. It is not drift. +- **blocked**: the check could not be brought back in line or could not run. Say exactly why. + +A check can be both updated and bug: the update makes the verification describe the code again, and then the property fails on it. + +## Edit scope + +Edit only the verification: models, harnesses, property files, and the verify skill itself. Never edit product code during a run, unless the user asks you to. When a property fails on the current code, do not weaken the property or the model to make it pass. Report the failure. + +## Pass + +1. **Find the checks.** A verify skill has no fixed name, so find it by what it does: a project skill that runs a model checker, a prover, or another verifier against named code. Read each one you find, or the one the user named. For each check, collect the property, the code it covers, the bounds and assumptions, the command that runs it, and the commit where it was last confirmed to describe the code. If no verify skill exists, stop and point at `/create-formal-verification-skill`. If the skill does not record a sync commit, use the last commit that changed the verification files, and say that you did. + +2. **Run it as it is.** Run each check once before you change anything, and record the result. A pass here does not tell you that the code is correct. It tells you that the old description still holds. A failure here can be drift or a bug. Do not decide which until step 5. + +3. **Read every change to covered code.** Diff the covered files from the sync commit to the current commit, and read each commit message. Also look for code that moved: a covered function that is renamed, split, or moved to another file is still covered code. Also look for new code that touches the state that a check guards, such as a new function that writes the same fields. For each change, decide which of these it is: + - **No effect.** The change does not alter anything the verification describes, such as formatting, comments, or code paths that the verification does not cover. Check this against the model or harness, not against the commit message. + - **The verification no longer describes the code.** A step that was one indivisible action is now two, a branch was added or removed, a check moved, a new path reaches the guarded state, or a value now has a different range. The model or harness must change. + - **The promise changed on purpose.** The change alters what the code promises, and evidence in the change says that this is intended: the doc comment, the tests, the changelog, or the commit message. The property must change, and you must cite that evidence. + - **The promise may be broken.** The code changed, and no evidence says that the promise changed. Treat a failure that follows as a bug candidate. + +4. **Update from the code, not from the result.** Change the model or harness so that each changed part again points to code that a reviewer can open, and keep one indivisible step in the code as one step in the verification. Write the update from the code before you rerun, and do not shape it by what makes the check pass. Change a property only for a promise that changed on purpose. Write down the old wording, the new wording, and the evidence. Keep the bounds unless the change makes them wrong. If you must reduce a bound, say so in the report. + +5. **Rerun and judge each result.** + - **Pass:** the check can now pass on a description that has lost the ability to fail. Break the new code the way the property guards against, such as removing a new check or reordering a new step, and confirm that the check catches it. Then drop the break. + - **Fail:** replay the counterexample against the real code, step by step. If a step cannot happen in the code, the verification is wrong. Fix the verification, and say what was wrong. If every step can happen, it is a bug. Name the commit that introduced it, tell the counterexample as a sequence of steps in the code's own words, and state the harm in one sentence. If a cheap test or reproduction against the real code shows the bug, add it to the report as evidence. Do not commit it to the product code. + +6. **Update the verify skill.** Update the code that each check covers, the commands, the bounds, the assumptions, and the sync commit. Set the sync commit to the commit that you checked. Do not move the sync commit for a blocked check, and say so in the report. Then follow the verify skill once as the next agent would, so that you know its steps still run. + +## Report + +Tell the user, for each check: + +- the outcome, and the commits that you read; +- what changed in the verification and why, with a short reason for each change: the code changed shape, or the promise changed on purpose (with the evidence); +- the rerun result, and the break that you used to show the updated check can still fail; +- each bug, in plain words: the counterexample as steps in the code's words, the harm, and the commit that introduced it; +- what the verification still does not cover, including new code that it should cover and does not. + +Say outright which failures were drift in the verification and which were bugs in the code. For a check that passed before you updated it and fails after, say that the old pass was on a stale description. + +Put the verification updates in a change of their own, separate from any product fix. diff --git a/plugins/pstack/skills/poteto-help/SKILL.md b/plugins/pstack/skills/poteto-help/SKILL.md index b1c80ebd..25134df8 100644 --- a/plugins/pstack/skills/poteto-help/SKILL.md +++ b/plugins/pstack/skills/poteto-help/SKILL.md @@ -26,7 +26,7 @@ Check the state that changes the answer, and mention it only when it does: - No model sheet (`~/.config/t3-pstack/models.md`, see `/setup-pstack`) means `/setup-pstack` hasn't run for this user, so every role uses its default model. - No `verify-*` skill or other app harness in the project means agents have no scripted way to drive the app. Mention `/create-verification-skill` when the question is about proving a change works. -- No formal verification skill in the project means no property is checked past what tests reach. Mention `/create-formal-verification-skill` when the question is about a race, an invariant, or another case tests rarely hit. +- No formal verification skill in the project means no property is checked past what tests reach. Mention `/create-formal-verification-skill` when the question is about a race, an invariant, or another case tests rarely hit. When one exists and the code it covers changed after the commit it records as last in sync, mention `/maintain-formal-verification-skill` if the question touches that code. When the model sheet is missing and it matters, ask whether the user wants to pick a model for each role and a reasoning budget now. It matters when the user is new, the question is about setup or cost, or the answer depends on which models run. Ask at most once per chat. If the need is also unclear, ask both questions together. Offer two choices: @@ -87,6 +87,7 @@ The default answer is `/poteto-mode`, which runs most of the others when its ste | Give agents a scripted way to drive the app and prove behavior | [`/create-verification-skill`](../create-verification-skill/SKILL.md) | | Bring a verification skill and its feature map back in line with the app | [`/maintain-verification-skill`](../maintain-verification-skill/SKILL.md) | | Formally verify a race, invariant, or other property that tests rarely reach | [`/create-formal-verification-skill`](../create-formal-verification-skill/SKILL.md) | +| Bring a formal verification back in line after the code it covers changed, and learn whether a failure is drift or a bug | [`/maintain-formal-verification-skill`](../maintain-formal-verification-skill/SKILL.md) | | Vet a performance number before reporting or acting on it | [`/benchmark-checklist`](../benchmark-checklist/SKILL.md) | | Run a large or cross-cutting change, or one to review after stepping away | [`/figure-it-out`](../figure-it-out/SKILL.md) | | Keep a decision log during a run, and review it afterward | [`/show-me-your-work`](../show-me-your-work/SKILL.md) | diff --git a/plugins/pstack/skills/poteto-help/references/recipes.md b/plugins/pstack/skills/poteto-help/references/recipes.md index 2d785761..c4f60466 100644 --- a/plugins/pstack/skills/poteto-help/references/recipes.md +++ b/plugins/pstack/skills/poteto-help/references/recipes.md @@ -34,7 +34,7 @@ Swap in the real paths, skills, and done checks. Informal wording works. ## Review and ship - `/interrogate the whole branch, but skeptically. don't change anything yet. no nitpicks unless it's a real bug or regression.` Read the dismissals too. -- `/create-formal-verification-skill prove <property> holds in <module>, even when <steps> interleave or retry.` +- `/create-formal-verification-skill prove <property> holds in <module>, even when <steps> interleave or retry.` After merges or refactors in that code: `/maintain-formal-verification-skill`. - `/swarm check every package under <dir> against its check script. one worker per package. one report.` - `/poteto-mode open the pr. small ordered commits, evidence in the description.` - `/poteto-mode babysit this pr. get it green.` For status only: `/poteto-mode check on pr <number>. anything outstanding?` diff --git a/plugins/pstack/skills/poteto-mode/references/licenses/NOTICE.md b/plugins/pstack/skills/poteto-mode/references/licenses/NOTICE.md index 7b429863..f2823f7f 100644 --- a/plugins/pstack/skills/poteto-mode/references/licenses/NOTICE.md +++ b/plugins/pstack/skills/poteto-mode/references/licenses/NOTICE.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/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 pstack skills, principles, scripts, and the `poteto-agent` and `comment-sicko` definitions | [cursor/plugins/pstack](https://github.com/cursor/plugins/tree/d457567332aa6989e753ea289f30ea2bfbc80bc0/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/d457567332aa6989e753ea289f30ea2bfbc80bc0/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/d457567332aa6989e753ea289f30ea2bfbc80bc0/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/tools/upstream.json b/tools/upstream.json index ca984c99..84446aa8 100644 --- a/tools/upstream.json +++ b/tools/upstream.json @@ -4,7 +4,7 @@ "pstack": { "upstreamPath": "pstack", "localPath": "plugins/pstack", - "sha": "6b78e9f4e46c75d1697d837e51f07c2692e60b24", + "sha": "d457567332aa6989e753ea289f30ea2bfbc80bc0", "exclude": [ ".cursor-plugin/", ".gitignore", @@ -20,7 +20,7 @@ "cursor-team-kit": { "upstreamPath": "cursor-team-kit/skills", "localPath": "plugins/pstack/skills", - "sha": "6b78e9f4e46c75d1697d837e51f07c2692e60b24", + "sha": "d457567332aa6989e753ea289f30ea2bfbc80bc0", "exclude": [ "check-compiler-errors/", "control-cli/", @@ -39,7 +39,7 @@ "thermos": { "upstreamPath": "thermos", "localPath": "plugins/pstack", - "sha": "6b78e9f4e46c75d1697d837e51f07c2692e60b24", + "sha": "d457567332aa6989e753ea289f30ea2bfbc80bc0", "exclude": [ ".cursor-plugin/", "CHANGELOG.md",