Adopt Cursor Pstack 0.15.28

.claude-plugin/marketplace.json

@@ -9,7 +9,7 @@
       "name": "pstack",
       "source": "./plugins/pstack",
       "description": "if you want to go fast, go deep first. pstack helps you write less, but higher quality code. rigorous agent workflows you can parallelize with confidence.",
-      "version": "1.17.5",
+      "version": "1.17.6",
       "author": {
         "name": "Lauren Tan (original)"
       },

CHANGELOG.md

@@ -4,6 +4,12 @@ This file records what each version of the Open Pstack package changed. Versions
 
 Entries describe package versions. Published release checkpoints have tag links; installation follows `main` unless pinned. Validation belongs to the linked pull requests. Older reports remain available through immutable links.
 
+## 1.17.6 adds formal-verification creation and upkeep
+
+Cursor baseline: [0.15.28](https://github.com/cursor/plugins/tree/d457567332aa6989e753ea289f30ea2bfbc80bc0/pstack). [Issue #164](https://github.com/arjitj2/open-pstack/issues/164). [PR #165](https://github.com/arjitj2/open-pstack/pull/165). Tag [v1.17.6](https://github.com/arjitj2/open-pstack/releases/tag/v1.17.6).
+
+Adds formal-verification creation and maintenance skills, optional Setup offers and Help entry points. Ketchup lists every waiting item without a word-count cutoff. Sharpen permits an explicitly requested rewritten prompt while retaining task execution and manual invocation. Generated skills use the active host’s project directory and preserve parent Git ownership, bounded-scope reporting and separate product findings. README content and saved provider policy remain unchanged. Validation and its limits are recorded in the PR.
+
 ## 1.17.5 validates branded identifiers without casts
 
 Cursor baseline: [0.15.25](https://github.com/cursor/plugins/tree/1b800800583ee8ff7f2676caf7a5cb7f0804be85/pstack). [Issue #157](https://github.com/arjitj2/open-pstack/issues/157). [PR #158](https://github.com/arjitj2/open-pstack/pull/158). Tag [v1.17.5](https://github.com/arjitj2/open-pstack/releases/tag/v1.17.5).

NOTICE.md

@@ -38,3 +38,5 @@ The `99743e9` adaptation shortens the migration, type-system, Swarm and lead-rev
 The `182f2ce` adaptation retains the shared Codex/Claude tree while applying the Claude question-tool mapping to setup and recognizing upstream's official Claude package. Its generated tree and incompatible routing and transcript rules are not imported.
 
 The `0317eb8` TypeScript update adopts Lauren Tan's verifying type-guard branding rule and example. The `a968159` naming validation is adapted to this distribution's static checks. The generated Claude tree and alternate setup policies from `1b80080` remain excluded.
+
+The formal-verification creation and maintenance skills, complete Ketchup call lists, and Sharpen prompt-ban removal derive from Cursor commits through [`d457567`](https://github.com/cursor/plugins/tree/d457567332aa6989e753ea289f30ea2bfbc80bc0/pstack). Port adaptations preserve host-local skill registration, scoped proof, parent Git ownership, approved provider policy and optional post-setup offers. Cursor-specific guide prose and the generated duplicate Claude tree remain excluded.

UPSTREAM.md

@@ -10,13 +10,13 @@ This page records the current Cursor baseline and the maintainer procedure for r
 | --- | --- |
 | Repository | `https://github.com/cursor/plugins.git` |
 | Path | `pstack/` |
-| Commit | `1b800800583ee8ff7f2676caf7a5cb7f0804be85` |
-| Upstream version | `0.15.25` |
-| open-pstack version | `1.17.5` |
+| Commit | `d457567332aa6989e753ea289f30ea2bfbc80bc0` |
+| Upstream version | `0.15.28` |
+| open-pstack version | `1.17.6` |
 
 The table records the packaged version on `main` and the Cursor content it incorporates, minus the exclusions below. Detecting or reviewing a newer Cursor commit does not advance this baseline. Cursor's version identifies the imported content. The open-pstack version identifies the cross-harness package, and its numbers are independent of Cursor and Eric's port.
 
-The upstream README at this baseline is [cursor/plugins `pstack/README.md` @ 1b80080](https://github.com/cursor/plugins/blob/1b800800583ee8ff7f2676caf7a5cb7f0804be85/pstack/README.md). [CHANGELOG.md](CHANGELOG.md) records the baseline of each release, and [NOTICE.md](NOTICE.md) records provenance.
+The upstream README at this baseline is [cursor/plugins `pstack/README.md` @ d457567](https://github.com/cursor/plugins/blob/d457567332aa6989e753ea289f30ea2bfbc80bc0/pstack/README.md). [CHANGELOG.md](CHANGELOG.md) records the baseline of each release, and [NOTICE.md](NOTICE.md) records provenance.
 
 ## Upstream-only exclusions
 
@@ -42,6 +42,12 @@ The `a968159` skill-name corrections already match this distribution. Its naming
 
 The `019a6a2` README and Cursor-guide refresh remains upstream. Its docs-vs-tree checker assumes Cursor paths, complete README inventories, built-ins and model defaults. This distribution keeps its owning-document inventory, link/anchor checks and provider-ID checks. No README edits were approved or made, and no packaged skill, agent or manifest changed. This excluded commit advances the review ledger without changing the incorporated package baseline.
 
+The `16541c6` and `bc14437` Ketchup changes list every waiting item without a word-count cutoff. They supersede the earlier per-item waiting-cost and mandatory-visual format while preserving human-message anchoring, read-only scope, UI authorization and evidence limits. The `75fabac` Sharpen change removes its rewritten-prompt ban; manual invocation, task execution and explicit user constraints remain.
+
+The `4382e68`, `6b78e9f` and `7b353f7` formal-verification skills use the active host’s project-skill location and parent-owned Git operations. Native registration, bounded real-code execution, disposable fault sensitivity and verification-only maintenance remain required. The `f9be7aa` setup offers require successful smoke and an explicit yes; existing matching harnesses suppress duplicate offers. Help links the shared skills. Cursor-specific version, README and guide copies through `d457567` stay upstream.
+
+The `disable-model-invocation: true` flags from `4382e68` and `7b353f7` are not applied to `create-formal-verification-skill` or `maintain-formal-verification-skill`. Both remain model-invocable for parent verification workflows, matching the existing regular verification pair. In particular, Setup must invoke formal creation after successful smoke and explicit consent; the upstream flag blocks that model-origin Skill call in Claude Code. Automatic selection in either host remains unverified.
+
 Earlier exclusions include Cursor's Benny automation, tutorial and sticky-mode UI, Cursor-only agent metadata, and Team Kit tools covered by host built-ins or bundled skills. The [historical port record](https://github.com/arjitj2/open-pstack/blob/5f0bb42dea46344c2f1961ebeebaeee135b49778/docs/reference.md#whats-deliberately-not-ported) records those source revisions.
 
 ## Port adaptations

maintenance/upstream-ledger.json

@@ -415,9 +415,89 @@
       "subject": "pstack: refresh the docs and add a docs-vs-tree check (#704)",
       "reason": "Keep Cursor README/guide prose and generated copies upstream. The new checker assumes Cursor-specific paths, complete README skill/playbook/agent inventories, built-ins and model defaults. This distribution keeps its owning-document inventory, link/anchor and provider-ID checks instead; no unapproved README edits or duplicate guide are introduced. Source skills, agents and plugin manifest are unchanged, so the packaged baseline and release remain unchanged.",
       "evidence": "https://github.com/arjitj2/open-pstack/pull/160"
+    },
+    {
+      "commit": "16541c6bc1ed6c8d808b2f78a33364003e82b967",
+      "date": "2026-10-17",
+      "status": "adapted",
+      "subject": "fix(pstack): list every waiting item so each ketchup call is decidable (#692)",
+      "reason": "List every waiting item with context, recommendation, evidence and risk. Preserve human-message anchoring, read-only scope, UI permission and supplied-evidence limits; the new item format supersedes the older per-item waiting-cost and mandatory-visual format.",
+      "evidence": "https://github.com/arjitj2/open-pstack/pull/165"
+    },
+    {
+      "commit": "bc1443790cc980d0ea857663260a831299884508",
+      "date": "2026-10-17",
+      "status": "adopted",
+      "subject": "fix(pstack): say outright that ketchup never cuts items to stay under a word count (#708)",
+      "reason": "Never cut waiting items to satisfy a word count. Both real hosts retained all thirty supplied items; Claude renamed labels while preserving item coverage.",
+      "evidence": "https://github.com/arjitj2/open-pstack/pull/165"
+    },
+    {
+      "commit": "4382e687a50b8d2c5ce4d141d001186589cff8d5",
+      "date": "2026-10-17",
+      "status": "adapted",
+      "subject": "feat(pstack): add /create-formal-verification-skill (#709)",
+      "reason": "Add formal verification creation with one active-host project-skill tree, parent-owned Git and observed native registration/execution. Real-code generated-input fallback and disposable fault checks passed in both hosts; source guide and generated duplicate packaging are excluded. Exclude the upstream disable-model-invocation flag so the parent can invoke creation after successful Setup smoke and explicit consent, matching the regular verification pair. Automatic selection in either host remains unverified.",
+      "evidence": "https://github.com/arjitj2/open-pstack/pull/165"
+    },
+    {
+      "commit": "0b8e952052d482ee6de06deebf14d590d77b1b34",
+      "date": "2026-10-18",
+      "status": "excluded",
+      "subject": "chore(pstack): bump to 0.15.26 (#710)",
+      "reason": "Retain independent distribution numbering. Cursor patch releases map to one tested distribution patch for this batch; upstream manifest and README/guide version copies are not imported.",
+      "evidence": "https://github.com/arjitj2/open-pstack/pull/165"
+    },
+    {
+      "commit": "75fabace38ce507ee044546eaca64167c8c1e21b",
+      "date": "2026-10-18",
+      "status": "adapted",
+      "subject": "pstack: drop the rewritten-prompt ban from sharpen (#712)",
+      "reason": "Remove only the rewritten-prompt ban while preserving manual invocation, task execution and explicit constraints. Both real hosts calculated the supplied control result and delivered the explicitly requested rewrite.",
+      "evidence": "https://github.com/arjitj2/open-pstack/pull/165"
+    },
+    {
+      "commit": "0148b78c56c72a1b8412055913c79f767095b217",
+      "date": "2026-10-18",
+      "status": "excluded",
+      "subject": "chore(pstack): bump to 0.15.27 (#713)",
+      "reason": "Retain independent distribution numbering and exclude Cursor-specific manifest/README version copies. This patch increment is covered by the batch distribution patch.",
+      "evidence": "https://github.com/arjitj2/open-pstack/pull/165"
+    },
+    {
+      "commit": "f9be7aa00c2b2bf4b13562143a6918445e06b99d",
+      "date": "2026-10-18",
+      "status": "adapted",
+      "subject": "pstack: offer formal verification in setup, sync help and guide (#715)",
+      "reason": "Offer regular and formal generators independently only after successful setup smoke and explicit yes; preserve no/duplicate/failure/routing-only guards. Portable Help names both skills. Both hosts exercised supplied-state offer decisions; unchanged setup probes/persistence were not repeated, and full yes-path setup transactions remain unverified. Cursor guide/README edits stay upstream.",
+      "evidence": "https://github.com/arjitj2/open-pstack/pull/165"
+    },
+    {
+      "commit": "6b78e9f4e46c75d1697d837e51f07c2692e60b24",
+      "date": "2026-10-19",
+      "status": "adapted",
+      "subject": "fix(pstack): add TLA+ default and no-verifier fallback to create-formal-verification-skill (#721)",
+      "reason": "Retain TLA+ as the default for interleaving models and use bounded generated inputs against real code when no suitable verifier is available. Both hosts distinguished the supplied modeling plan from actual parser fallback checks; no TLA+ engine execution is claimed.",
+      "evidence": "https://github.com/arjitj2/open-pstack/pull/165"
+    },
+    {
+      "commit": "7b353f78f6ec193bdbe48ed8059444eb09b6878e",
+      "date": "2026-10-19",
+      "status": "adapted",
+      "subject": "pstack: add maintain-formal-verification-skill (#716)",
+      "reason": "Add verification-only maintenance with exact sync commits, no-effect/intended-promise/renamed-implementation classification, stale-pass disclosure, fault sensitivity and reachable bug reports. Both hosts loaded updated native local skills and executed real code; parent staged reviewed artifacts and owned fixture Git. Preserve failures, policy deviations and scope limits. Exclude the upstream disable-model-invocation flag so parent verification workflows can invoke maintenance, matching the regular verification pair. Automatic selection in either host remains unverified.",
+      "evidence": "https://github.com/arjitj2/open-pstack/pull/165"
+    },
+    {
+      "commit": "d457567332aa6989e753ea289f30ea2bfbc80bc0",
+      "date": "2026-10-19",
+      "status": "excluded",
+      "subject": "chore(pstack): bump to 0.15.28, sync guide with create-formal-verification-skill (#724)",
+      "reason": "Record Cursor0.15.28 as the incorporated source checkpoint while retaining distribution1.17.6. Exclude upstream version/README/guide copies; portable skill intent is implemented by preceding adapted entries.",
+      "evidence": "https://github.com/arjitj2/open-pstack/pull/165"
     }
   ],
-  "reviewed_through": "019a6a20592c10bf92869e5740368f578a9997fd",
+  "reviewed_through": "d457567332aa6989e753ea289f30ea2bfbc80bc0",
   "schema": 1,
   "source": {
     "path": "pstack/",

plugins/pstack/.claude-plugin/plugin.json

@@ -1,7 +1,7 @@
 {
   "name": "pstack",
   "displayName": "pstack",
-  "version": "1.17.5",
+  "version": "1.17.6",
   "description": "if you want to go fast, go deep first. pstack helps you write less, but higher quality code. rigorous agent workflows you can parallelize with confidence. Ported from cursor/plugins/pstack for Claude Code and Codex.",
   "author": {
     "name": "Lauren Tan"

plugins/pstack/.codex-plugin/plugin.json

@@ -1,6 +1,6 @@
 {
   "name": "pstack",
-  "version": "1.17.5",
+  "version": "1.17.6",
   "description": "if you want to go fast, go deep first. pstack helps you write less, but higher quality code. rigorous agent workflows you can parallelize with confidence. Codex port of the Claude Code plugin; skills are shared, tool names resolve via skills/poteto-mode/references/codex-tools.md.",
   "author": {
     "name": "Lauren Tan"

plugins/pstack/NOTICE.md

@@ -38,3 +38,5 @@ The `99743e9` adaptation shortens the migration, type-system, Swarm and lead-rev
 The `182f2ce` adaptation retains the shared Codex/Claude tree while applying the Claude question-tool mapping to setup and recognizing upstream's official Claude package. Its generated tree and incompatible routing and transcript rules are not imported.
 
 The `0317eb8` TypeScript update adopts Lauren Tan's verifying type-guard branding rule and example. The `a968159` naming validation is adapted to this distribution's static checks. The generated Claude tree and alternate setup policies from `1b80080` remain excluded.
+
+The formal-verification creation and maintenance skills, complete Ketchup call lists, and Sharpen prompt-ban removal derive from Cursor commits through [`d457567`](https://github.com/cursor/plugins/tree/d457567332aa6989e753ea289f30ea2bfbc80bc0/pstack). Port adaptations preserve host-local skill registration, scoped proof, parent Git ownership, approved provider policy and optional post-setup offers. Cursor-specific guide prose and the generated duplicate Claude tree remain excluded.