athul-ramesh · Oct 26, 2026 · Oct 25, 2026
diff --git a/.devin-plugin/plugin.json b/.devin-plugin/plugin.json
@@ -1,6 +1,6 @@
 {
   "name": "pstack",
-  "version": "0.6.1",
+  "version": "0.7.0",
   "description": "Rigorous agent workflows for Devin CLI. Write less, higher quality code.",
   "homepage": "https://github.com/athul-ramesh/ptstack-devin",
   "repository": "https://github.com/athul-ramesh/ptstack-devin",

diff --git a/README.md b/README.md
@@ -22,19 +22,21 @@ The 0.2.0 release was verified against Devin CLI 3000.11.3 (9c803229faa4), local
 
 Avoid installing two copies with the same plugin name. Devin may source-qualify inventory names while loading skills from an older copy; verify the path returned by the skill tool.
 
-## Using 0.5.0
+## Using 0.7.0
 
 Ask `/pstack:poteto-help` with a setup or workflow question. This explicit-user skill answers with one suggested prompt and a source link. It does not start a task for a help question. A request to do work follows poteto-mode instead.
 
-Invoke [`/pstack:ketchup`](skills/ketchup/SKILL.md) to catch up on this chat since your last message. It is explicit-user and read-only. It summarizes changes and decisions well under 150 words in plain sentences, with small available visuals, options, costs, a recommendation, and what happens without an answer. The CLI uses compact text when no renderer is available.
+Invoke [`/pstack:ketchup`](skills/ketchup/SKILL.md) to catch up on this chat since your last message. It is explicit-user and read-only. It keeps the story short, then lists every call waiting on you, each with its link, what it changes, the evidence, the risk, and a pick, so you can decide from the reply alone. A large batch makes a long reply rather than a cut list. Small visuals appear only when the host renders them; the CLI uses compact text otherwise.
 
 The [usage guide](docs/usage-guide.md) covers prompting, investigation, prototypes before plans, real behavior verification, benchmark evidence, repeated-mistake enforcement, and bounded in-session delivery. The help skill includes [prompting guidance](skills/poteto-help/references/prompting.md) and [copyable recipes](skills/poteto-help/references/recipes.md).
 
-Invoke [`/pstack:sharpen`](skills/sharpen/SKILL.md) before a task to have the agent frame it the way a top expert would, keep one outside check, leave your choices open, and then do the work. It runs only when requested.
+Invoke [`/pstack:sharpen`](skills/sharpen/SKILL.md) on a prompt before you send it. The agent says what a top professional would add, the raw material and methods they would use, and an outside check, then hands back the rewritten prompt with your choices left open. It does not do the task. It runs only when requested.
+
+Invoke [`/pstack:create-formal-verification-skill`](skills/create-formal-verification-skill/SKILL.md) when tests cannot reach the case that breaks a race, retry, state machine, parser, or unsafe code. It verifies one property with a tool that fits and runs on your machine, shows the check failing on a broken variant, and writes a project skill under `.devin/skills/` to recheck it. [`/pstack:maintain-formal-verification-skill`](skills/maintain-formal-verification-skill/SKILL.md) brings that verification back in line after the covered code changes. This plugin bundles no verifier; the agent asks before installing one.
 
 Invoke [`/pstack:in-your-own-words`](skills/in-your-own-words/SKILL.md) to hear the goals and problem the agent understood. It runs only when requested and adds no confirmation gate.
 
-Release 0.6.1 selectively ports upstream pstack 0.15.25; see the [0.15.25 port audit](docs/pstack-0.15.25-port-audit.md). Release 0.6.0 selectively ported upstream pstack 0.15.24; see the [0.15.24 port audit](docs/pstack-0.15.24-port-audit.md). The prior release selectively ported upstream pstack 0.15.23. It adds goal playback, shorter ketchup replies, usable-state verification, a cheap observability proposal after deep debugging, robust Markdown fence checks, and configurable worktree merge bases. Devin dispatch, profile pins, and delivery authority are preserved. See the [port audit](docs/pstack-0.15.23-port-audit.md) for source coverage, exclusions, and evidence limits. Earlier audits cover [0.15.17](docs/pstack-0.15.17-port-audit.md) and [0.15.13](docs/pstack-0.15.13-port-audit.md).
+Release 0.7.0 selectively ports upstream pstack 0.15.26 through 0.15.32 and follow-ups to `e73df47`; see the [0.15.32 port audit](docs/pstack-0.15.32-port-audit.md). Release 0.6.1 selectively ported upstream pstack 0.15.25; see the [0.15.25 port audit](docs/pstack-0.15.25-port-audit.md). Release 0.6.0 selectively ported upstream pstack 0.15.24; see the [0.15.24 port audit](docs/pstack-0.15.24-port-audit.md). The prior release selectively ported upstream pstack 0.15.23. It adds goal playback, shorter ketchup replies, usable-state verification, a cheap observability proposal after deep debugging, robust Markdown fence checks, and configurable worktree merge bases. Devin dispatch, profile pins, and delivery authority are preserved. See the [port audit](docs/pstack-0.15.23-port-audit.md) for source coverage, exclusions, and evidence limits. Earlier audits cover [0.15.17](docs/pstack-0.15.17-port-audit.md) and [0.15.13](docs/pstack-0.15.13-port-audit.md).
 
 ## Features retained from 0.2.0
 

diff --git a/docs/pstack-0.15.32-port-audit.md b/docs/pstack-0.15.32-port-audit.md
@@ -0,0 +1,43 @@
+# Port pstack 0.15.26 to 0.15.32 to Devin
+
+Audited on 2026-10-26 on top of `main` at `28917b5` (PRs #8 and #9 merged). Plugin version is 0.7.0, with 39 public skills, 24 internal principle leaves, and 20 playbooks.
+
+## Source and coverage
+
+Upstream range: [`99743e9...e73df47`](https://github.com/cursor/plugins/compare/99743e9c151c8537cbbf1f98bb38f34ef3368453...e73df471cd4bd918367e99f3dd9c51bd53ddf5f0) (`pstack/`, 0.15.25 to 0.15.32 and six follow-ups). All 32 commits that touch `pstack/` were read.
+
+| Upstream change | Devin disposition |
+| --- | --- |
+| [#700](https://github.com/cursor/plugins/commit/0317eb8) brand with a type guard, not `as` | Ported. The Branded types row and the `AgentId` example use an `isAgentId` guard. |
+| [#692](https://github.com/cursor/plugins/commit/16541c6), [#708](https://github.com/cursor/plugins/commit/bc14437) ketchup lists every waiting item | Adapted. The story stays under 100 words, each item gets about 30 words with its link, user change, evidence, risk, and pick, and items are never cut to meet a word count. Rendered pictures stay conditional on the Devin host and the text fallback is kept. |
+| [#712](https://github.com/cursor/plugins/commit/75fabac), [#729](https://github.com/cursor/plugins/commit/88d4751) sharpen returns only the rewritten prompt | Ported in its final form, the four numbered asks and a rewrite. One Devin line is added: hand back only the rewrite and do not start the task, because this plugin's always-on rule otherwise routes nontrivial work to poteto-mode. Help, recipes, README, and usage guide follow. |
+| [#709](https://github.com/cursor/plugins/commit/4382e68), [#721](https://github.com/cursor/plugins/commit/6b78e9f), [#716](https://github.com/cursor/plugins/commit/7b353f7), [#724](https://github.com/cursor/plugins/commit/d457567) create and maintain formal verification skills | Adapted as explicit-user `/pstack:create-formal-verification-skill` and `/pstack:maintain-formal-verification-skill`. Generated skills go under `.devin/skills/`. The plugin bundles no verifier, so the agent confirms the tool runs with `exec`, asks before installing a toolchain, and reports a check that could not run as blocked. The TLA+ default and the generated-input fallback are kept. Maintenance stops at merge-ready. |
+| [#715](https://github.com/cursor/plugins/commit/f9be7aa) formal verification in setup, help, and guide | Help state check, routing rows, and recipes ported. The setup offer is skipped: this port's `/pstack:setup-pstack` only writes the role sheet and has no verification offer step to extend. Cursor guide pages are not shipped; the usage guide gains the equivalent section. |
+| [#794](https://github.com/cursor/plugins/commit/00d5dec) generated verify skills read results with `/statechart` | Skipped. `/statechart` is not shipped. Counterexamples are still told as steps in the code's words. |
+| [#741](https://github.com/cursor/plugins/commit/eb4db2b), [#776](https://github.com/cursor/plugins/commit/7698375), [#779](https://github.com/cursor/plugins/commit/4ec7ffa), [#791](https://github.com/cursor/plugins/commit/076f4b2) statechart skill and Pele renderer | Skipped as uncertain. About 12,000 lines of Node scripts and tests (about 5,200 without tests) that install TLC and Java with mise (about 305 MB), render PNGs with Pele and resvg, and expect the agent to look at each PNG. Devin documents image attachments as input, not inline image output in the CLI. A separate port needs native testing first. |
+| [#797](https://github.com/cursor/plugins/commit/3c0fdb4) ketchup-video | Skipped as uncertain. It needs a video renderer and inline video in the reply. Devin documents neither, and this plugin ships no renderer. |
+| [#800](https://github.com/cursor/plugins/commit/7054003) reflect edits leave the plugin cache | Adapted. Reflect never edits a skill inside an installed plugin. A remote plugin is re-fetched by `devin plugins update`; a `--local` plugin is linked to its checkout. Edits go to a copy under `.devin/skills/` or `~/.config/devin/skills/`, shown before approval, with no PR or push. |
+| [#702](https://github.com/cursor/plugins/commit/a968159) name every skill after its folder | Already satisfied. A contract test now enforces it, since Devin uses the folder as the skill identifier. |
+| [#807](https://github.com/cursor/plugins/commit/e73df47) swarm Phase A numbering and table reference | Already satisfied. This port's swarm is numbered 1 to 4 and Phase C keeps the result table that Phase D reports. |
+| [#801](https://github.com/cursor/plugins/commit/96dec8e), [#802](https://github.com/cursor/plugins/commit/fe096ef) watch-pr fork heads and deadline sleeps; [#804](https://github.com/cursor/plugins/commit/3c596e7) orch prefers the active PR | Not applicable. The Bun watch-pr and orch scripts are not shipped in this port. `worktree-audit.sh` already prefers an open PR per branch. |
+| [#803](https://github.com/cursor/plugins/commit/86c2448) inline code delimiters in check-plan | Not applicable. This port's `check-plan.mjs` validates structure and has no prose lint that strips inline code. |
+| [#805](https://github.com/cursor/plugins/commit/f83fbe6) GNU stat and date in worktree-audit | Not applicable. This port's `worktree-audit.sh` reads no transcript mtimes; it uses `git log --format=%ct`, which is portable. |
+| [#637](https://github.com/cursor/plugins/commit/182f2ce), [#705](https://github.com/cursor/plugins/commit/1b80080), [#806](https://github.com/cursor/plugins/commit/a0b0ad9) Claude Code plugin, adapter, and auto-update note | Skipped. Claude Code only. |
+| [#704](https://github.com/cursor/plugins/commit/019a6a2) docs refresh and docs-vs-tree check | Skipped. Cursor README and guide wording plus a repo script for the generated Claude Code tree. The existing link and help-table tests cover this port's docs. |
+| [#710](https://github.com/cursor/plugins/commit/0b8e952), [#713](https://github.com/cursor/plugins/commit/0148b78), [#792](https://github.com/cursor/plugins/commit/642289e), [#798](https://github.com/cursor/plugins/commit/b1a1298) version bumps | Plugin bumped independently to 0.7.0. |
+
+## Devin compatibility
+
+| Capability | Evidence |
+| --- | --- |
+| Explicit-user skills and folder names | `triggers` and `name` are documented; the directory name is the identifier. [Creating skills](https://docs.devin.ai/cli/extensibility/skills/creating-skills). |
+| Project and global skill paths | `.devin/skills/`, `.agents/skills/`, `.windsurf/skills/`, `~/.config/devin/skills/`. [Skills overview](https://docs.devin.ai/cli/extensibility/skills/overview). |
+| Plugin update and local links | `devin plugins info`, `devin plugins update` re-fetches, and `--local` installs link to the source folder. [Plugins](https://docs.devin.ai/cli/extensibility/plugins/overview). |
+| Inline images, video, Mermaid | Not documented for the CLI terminal. [CLI changelog](https://docs.devin.ai/cli/changelog/stable). Ketchup keeps its text fallback; statechart and ketchup-video are not shipped. |
+| Verifier toolchains | Not provided by Devin or this plugin. The agent runs them with `exec` only after confirming they exist, and asks before installing. |
+
+The other changes are prose and touch no Devin tool, profile, hook, or helper.
+
+## Verification and limits
+
+`node --test tests/*.test.mjs` passes, including new contract tests for skill folder names and this port's Devin paths, tool limits, and reflect destinations. These are static checks. Native 0.7.0 skill registration, a real TLA+ or other verifier run through the new skills, and inline rendering in Devin are untested.
diff --git a/docs/release-notes.md b/docs/release-notes.md
@@ -1,5 +1,7 @@
 # Release notes
 
+Plugin `pstack` 0.7.0 selectively ports upstream 0.15.26 through 0.15.32 and follow-ups to `e73df47`. It adds explicit-user `/pstack:create-formal-verification-skill` and `/pstack:maintain-formal-verification-skill`, which write project skills under `.devin/skills/`, bundle no verifier, and ask before installing one. `/pstack:sharpen` now hands back a rewritten prompt and does not do the task. Ketchup lists every waiting item with its link, evidence, risk, and pick, and never cuts items to meet a word count. Reflect never edits a skill inside an installed plugin. The TypeScript brand example uses a type guard. Statechart and ketchup-video are not shipped. Native activation of 0.7.0 remains untested. See the [port audit](pstack-0.15.32-port-audit.md).
+
 Plugin `pstack` 0.6.1 selectively ports upstream 0.15.25. Four principles (attack-the-premise, fix-root-causes, make-operations-idempotent, test-behavior-not-implementation) are restated as reasoning instead of rules, and `/pstack:correct` follows the new test rule. Marginal sections are cut from interrogate's lead judgment, migrate-callers, type-system-discipline, and swarm. Ketchup now explains each change, leads with existing screenshots, videos, and diagrams when the host renders them, sums up in bullets, and lists action items as plain bullets. The Devin text fallback is kept. Native activation of 0.6.1 and inline image rendering remain untested. See the [port audit](pstack-0.15.25-port-audit.md).
 
 Plugin `pstack` 0.6.0 selectively ports upstream 0.15.24. It adds explicit-user `/pstack:sharpen`, rewrites ketchup to a reply well under 150 words with small plain-language visuals, states that Devin dispatch has no per-call effort or speed knob, and runs the full plan audit set once at the code-ready SHA with a single fresh-context verifier for rebases and minor fixes. Native activation of 0.6.0 remains untested. See the [port audit](pstack-0.15.24-port-audit.md).
@@ -14,7 +16,7 @@ Plugin 0.2.0 was verified on local Devin CLI 3000.11.3 (9c803229faa4). Earlier 3
 
 ## Shipped
 
-37 public skills under `/pstack:<name>`. 24 `principle-*` leaves, model-triggered. 20 poteto-mode playbooks. Profiles `pstack:poteto-agent`, `pstack:poteto-agent-{swe,opus,sonnet,codex}`, `pstack:comment-sicko`, and `pstack:panel-{swe,opus,sonnet,codex}`.
+39 public skills under `/pstack:<name>`. 24 `principle-*` leaves, model-triggered. 20 poteto-mode playbooks. Profiles `pstack:poteto-agent`, `pstack:poteto-agent-{swe,opus,sonnet,codex}`, `pstack:comment-sicko`, and `pstack:panel-{swe,opus,sonnet,codex}`.
 
 SessionStart injects `PSTACK_ROUTE=/pstack:poteto-mode`.
 

diff --git a/docs/usage-guide.md b/docs/usage-guide.md
@@ -44,6 +44,8 @@ Keep the verification skill with the project when delivery is authorized. Update
 
 [`/pstack:benchmark-checklist`](../skills/benchmark-checklist/SKILL.md) vets a number before reporting or acting on it. Comparisons require five interleaved runs per side, median and range, correct outputs, and proof that timed work happened. A requested ballpark can use one labeled run while retaining error and work checks. Missing evidence means inconclusive. Performance playbooks already apply this checklist.
 
+Some bugs live on paths nobody drives: two retries that overlap, a lock that expires mid-write, a state change that arrives out of order. For code where such a bug is costly, use [`/pstack:create-formal-verification-skill`](../skills/create-formal-verification-skill/SKILL.md). The question picks the tool. TLA+ is the default for whether events can happen in a bad order. A verifier that runs on the code suits whether the code behaves for every input. When no verifier runs on the language, the agent says so and tests the real code with generated inputs. The plugin bundles no verifier, so the agent confirms the tool runs on this machine and asks before installing it. The check must fail on a broken variant, a finding stays a finding, and the generated skill under `.devin/skills/` records the covered code and the commit it last matched. After merges or refactors that skipped that skill, run [`/pstack:maintain-formal-verification-skill`](../skills/maintain-formal-verification-skill/SKILL.md). It updates the verification from the code, reruns it, and says whether each failure is drift or a bug.
+
 ## Deliver in this session
 
 Request commits, pushes, or a PR explicitly. Opening a PR does not start babysitting. [`/pstack:babysit`](../skills/babysit/SKILL.md) handles checks and feedback in the current session. Merge remains with the operator.
@@ -70,6 +72,8 @@ The help skill's [prompting reference](../skills/poteto-help/references/promptin
 
 Use `/pstack:in-your-own-words` to hear the goals and problem the agent understood. This explicit-user skill restates them without starting a workflow or adding a confirmation gate.
 
-Use `/pstack:ketchup` to catch up since your previous message. Replies stay under 250 words and include older unresolved user decisions. Existing captures and available diagrams show status and before/after options. When the Devin host cannot render them, compact text includes the same facts and unknowns. The skill does not start an app, install a renderer, or post anything to produce a visual.
+Use `/pstack:sharpen <the prompt you're about to send>` when you are unsure a prompt is aimed right. It hands back the prompt rewritten deeper, not bigger, with an outside check and your choices left open. It does not do the task. Send the rewrite yourself.
+
+Use `/pstack:ketchup` to catch up since your previous message. The story stays under 100 words. Every call waiting on you gets its own bullet with its link, what it changes, the evidence, the risk, and a pick, including older unresolved decisions, so a large batch makes a long reply instead of a cut list. Existing captures and available diagrams show status and before/after options. When the Devin host cannot render them, compact text includes the same facts and unknowns. The skill does not start an app, install a renderer, or post anything to produce a visual.
 
 Verification skills must launch a usable app from an empty data directory. Include migrations and seed data. Missing journey preconditions are failed checks, not a reason to weaken the journey. Proof from a stand-in must identify target setup steps it has not exercised.