Adapt Cursor 0.15.35 Statechart and workflow updates

.agents/skills/verify-open-pstack/features/workflows.md

@@ -22,6 +22,8 @@ Users invoke poteto-mode for an engineering task or call a focused skill directl
 - `workflow-ketchup`: manual current-chat catch-up anchors to a real human message, lists every item in pending human calls with evidence, risk and a recommendation, and reads status without starting queued work.
 - `workflow-formal-create`: generate one host-local formal verification skill with scoped properties, code mappings, a full sync commit, native registration and execution, and fault detection on disposable copies.
 - `workflow-formal-maintain`: reconcile covered-code changes with the verification, distinguish drift from bugs, prove sensitivity and advance only confirmed sync commits.
+- `workflow-statechart`: a natural-language workflow compiles to TLA+ and a Mermaid chart, checked by a real TLC run, with visible engine skips when `TLA2TOOLS` is unset.
+- `workflow-ketchup-video`: manual catch-up renders a short subtitled video from real artifacts outside the repo, holding each slide by frame-matched length.
 - `workflow-setup-verification-offers`: after successful setup smoke, offer regular and formal verification independently when no relevant skill or harness exists; only explicit yes generates anything.
 - `workflow-how-handoff`: complex exploration completes before the explainer receives every finding and named dropout.
 - `workflow-why-evidence`: active-host evidence discovery, conflicting citations, null categories, and investigator completion precede synthesis.
@@ -37,7 +39,7 @@ Users invoke poteto-mode for an engineering task or call a focused skill directl
 
 ## How to get to it (user POV)
 
-Claude Code: `/pstack:poteto-mode`, `/pstack:how`, `/pstack:ketchup`, or another named focused skill. Codex: select the same names in the skill picker, or mention `$pstack:poteto-mode`, `$pstack:how`, `$pstack:ketchup`, or the relevant focused skill. Ketchup and in-your-own-words are manual-only in both hosts.
+Claude Code: `/pstack:poteto-mode`, `/pstack:how`, `/pstack:ketchup`, or another named focused skill. Codex: select the same names in the skill picker, or mention `$pstack:poteto-mode`, `$pstack:how`, `$pstack:ketchup`, or the relevant focused skill. Ketchup, ketchup-video, and in-your-own-words are manual-only in both hosts.
 
 ## Driving it with the parent apps and shipped CLIs
 
@@ -59,7 +61,9 @@ Preconditions: installed candidate identity established, authenticated selected
 - **Debug signal:** invoke the root-cause principle with a labeled supplied scenario whose deciding fact needed a deep dig. Expect a concrete cheap always-on signal proposal tied to that fact, no instrumentation writes, and no claim that the hypothetical incident happened in the fixture.
 - **Ketchup history and decisions:** in a dedicated real host chat, establish an unresolved human decision, then give a later human instruction. After that instruction, collect a completed agent result with an existing screenshot or video it produced, a running task, a visible change with no captured media, and an actual automated notification or heartbeat if the host emits one. Invoke Ketchup manually. Expect the last actual human instruction before invocation to remain the anchor. The invocation, scheduler prompts, system messages, notifications, and subagent results do not reset it, even when rendered as user-role events. Later automated activity is still summarized. Expect the older unresolved decision to count, a resolved or already-authorized approval to be omitted, and queued agent work to appear on its own remaining-work line without starting. Expect the what-happened story under 100 words, with table words counted and pictures excluded. Every pending item remains present even when a large batch requires far more than 150 words; no count or link substitutes for an item. Expect the provided screenshot or video embedded inline first, then only a diagram that explains a change such as a real flow or dependency chain, never a status list, unconnected boxes, or a Markdown table treated as a picture. Expect no fact repeated across prose and visuals, one summary bullet per requested thing that leaves out what the action items say, and the action items as plain bullets rather than a diagram or box. Expect small explanatory visuals only where they help. A choice does not require a diagram; all weighed options still give gains, costs and the current state when one exists, with gains and costs under screenshots that show those options. Expect the media-less visible change marked "No screenshot yet" on its summary line along with what changed on screen, and no fabricated media, invented numbers, or pictures of uncaptured screens. Keep each drawn visual within six boxes and eight words per box. Each item gives its link when known, user impact, supporting evidence, risk even when low, and a recommendation, or names missing facts as unknown. A shared call states its recommendation once and lists each item riskiest first, naming a different pick only where needed. Waiting costs appear only when more than delay; no per-item no-answer line is required. Option costs supply the risk for a choice without a duplicate risk line. Inspect every option label for unsupported mechanism, freshness or load claims; proposed parameters alone do not establish those effects. Retain semantic limitations rather than claiming universal output precision. Verify current PR, CI, or agent status through available read-only readers and retain their outputs. Include a status that requires unauthorized UI; expect a concrete unchecked gap and no computer-use call. In a fresh chat with no intervening work or pending decision, expect a short no-change reply. With unavailable history, expect a stated anchor/history gap and only confirmed current-chat facts. Explicit Poteto Help must recommend Ketchup for this chat and Recall for cross-chat context without executing either. Inspect Claude's `disable-model-invocation` flag and Codex's `allow_implicit_invocation: false`, then verify manual invocation through both installed entry points and exercise the picture, diagram, bullet, and missing-media expectations in each host. Compare files, issues, PRs, installs, model sheets, scheduler state, and dispatched-task inventory before and after. Do not create a scheduled event as part of Ketchup or label a synthetic event as a real host heartbeat; record an unavailable heartbeat case as unverified.
 - **Ketchup complete batches:** supply a labeled set of thirty pending items in a dedicated installed-parent chat, including one older unresolved call, one shared call with a different recommendation for one item, low and high risks, an unavailable fact, and one meaningful deadline. Invoke manual Ketchup. Expect every item individually named with its known link, user impact, evidence, risk and recommendation. Count the items against the supplied set rather than trusting a claimed total. Expect shared-call recommendations once, riskiest-first item order, explicit unknowns, and the deadline cost only where relevant. This synthetic batch proves the reply format, not live PR state. Retain the read-only and human-anchor checks above.
-- **Formal creation:** in each installed host, use a disposable local CLI project with named code, a costly invariant, and a real verifier or generated-input fallback. Invoke `pstack:create-formal-verification-skill`. Expect one generated tree at `.claude/skills/<name>/` on Claude Code or `.agents/skills/<name>/` on Codex, matching name/directory frontmatter, real commands and tool version, code mappings, bounds, assumptions, exclusions and the exact full sync commit. Observe registration and invocation of the generated project skill through the host, then actual check execution. A direct file read is insufficient. Retain baseline result, fault-copy bytes and failure, counterexample, cleanup, and the original-byte rerun. Check that fault injection stays in disposable copies and that original product files and Git state are unchanged; Git mutations remain parent-owned. For a model, verify the code-to-model fault mapping rather than claiming an unchanged hand model detected a code edit. A generated-input fallback must be labeled testing, not formal proof. Missing tool, registration or execution leaves that path unverified; do not weaken a property to pass.
+- **Formal creation:** in each installed host, use a disposable local CLI project with named code, a costly invariant, and a real verifier or generated-input fallback. Invoke `pstack:create-formal-verification-skill`. Expect one generated tree at `.claude/skills/<name>/` on Claude Code or `.agents/skills/<name>/` on Codex, matching name/directory frontmatter, real commands and tool version, code mappings, bounds, assumptions, exclusions and the exact full sync commit. Observe registration and invocation of the generated project skill through the host, then actual check execution. A direct file read is insufficient. Retain baseline result, fault-copy bytes and failure, counterexample, cleanup, and the original-byte rerun. Check that fault injection stays in disposable copies and that original product files and Git state are unchanged; Git mutations remain parent-owned. For a model, verify the code-to-model fault mapping rather than claiming an unchanged hand model detected a code edit. A generated-input fallback must be labeled testing, not formal proof. Missing tool, registration or execution leaves that path unverified; do not weaken a property to pass. For the Statechart handoff, expect the generated skill to invoke the registered `pstack:statechart` skill by host name, not copied commands or installed paths, and observe a model-origin invocation on Claude Code.
+- **Statechart host routes:** in each installed host, invoke `pstack:statechart` with a small natural-language workflow plus a rule a run can break. With `TLA2TOOLS` pointing at a real `tla2tools.jar` (or the documented first-run `mise` provisioning the operator approved), expect an actual TLC run, a Mermaid chart, and the shortest path to a breaking state, and expect a passing model over 500 states to possibly produce no `chart.mmd` rather than a fabricated chart. For the automated test suite with `TLA2TOOLS` unset, expect visible engine skips, never engine-pass claims. Do not invoke the compiler without the jar unless first-run provisioning is approved. Record the actual Java version, jar checksum, engine skip counts, and any Node or Bun launcher actually exercised; replay and recorded fixtures are not live engine proof.
+- **Ketchup video catch-up:** in each installed host, manually invoke `pstack:ketchup-video` in a dedicated chat whose work produced real screenshots or diffs. Expect a short silent landscape video written outside the repository (the sole write exception), at most 10 slides built from actual artifacts, one subtitle line per slide burned into a fixed strip below the slide without covering content, holds measured by matching frames to slides rather than freeze detection at one second per three added words, and the waiting calls as text under the video. A render failure gets a one-line report with the calls only.
 - **Formal maintenance:** use parent-prepared fixtures with exact sync commits and covered-code changes for no-effect drift, a changed indivisible step, an intentionally changed promise with evidence, and a reachable bug. Invoke `pstack:maintain-formal-verification-skill`. Expect baseline execution before edits, review of all covered changes including moved functions and new state writers, code-grounded updates, and distinct in-sync, updated, bug or blocked outcomes. Require old/new property wording and intent evidence for a changed promise, disclosed bound reductions, disposable fault detection for a pass, and real-code counterexample replay for a failure. Confirm product code is unchanged, bug findings remain findings, blocked checks retain their old sync commit, and other sync records name only the full commit actually checked with dirty deltas separate. Observe native loading and execution of the updated generated skill, original-byte restoration without stash/reset, and retained evidence after failed and successful cleanup. A previously passing stale model that now exposes a bug must be reported as stale, not a successful old proof.
 - **Setup verification offers:** in dedicated parent profiles, complete steps 1 through 10 using the approved test sheet and actual required probes, confirmation and smoke. With no relevant harness, expect one regular offer and one formal offer. Decline each and verify no generated files; separately accept each explicitly and observe the active installed generator loading and the generated project skill's native registration and execution. Existing relevant regular or formal harnesses suppress only their matching duplicate offer. Test routing-only, failed-probe, declined-confirmation and failed-smoke paths with no offers or generation, preserving the setup workflow's existing snapshot and readback requirements. Do not modify personal installation or model sheets for fixtures. Record unavailable setup branches as unverified rather than fabricating probe success.
 - **Formal help:** ask installed Poteto Help how to check a race and keep its verification current. Expect links to both formal skills, the correct host-local directory and namespace, explicit bounds, and the two optional post-smoke setup offers with no work started. Repeat with an existing formal skill whose covered code changed after its sync commit; expect the maintenance pointer rather than duplicate generation.
@@ -93,6 +97,7 @@ For changes to TypeScript branding guidance, explicitly load the installed `type
 - Retained provider references do not require repeating unchanged setup, billing, provider availability, fallback, orchestration CLI, or install-source coverage. Named terminal results and receipts still need inspection in the changed prompt workflows.
 - The shipped-CLI recipes exercise the real binaries against fake readers and disposable repos; they do not prove GitHub's live paging, `gh`, or an installed parent's use of them.
 - Formal recipes require actual generated project-skill registration and execution in each host. Source inspection, tool output alone, or a model sensitivity check does not prove that native path. Keep formal scope, fallback testing and stale-model limits explicit.
+- Statechart and generated-verifier recipes need a real TLC run with `TLA2TOOLS` set; a replay fixture, a recorded output, or a typecheck does not prove the engine path. Keep skip counts visible.
 - Setup verification offers extend the setup flow after its successful smoke; these recipes do not waive its existing probe, confirmation, policy or persistence gates.
 - Do not add a timeout, weaker model, or unsaved backup to finish a verification run.
 

.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.6",
+      "version": "1.17.7",
       "author": {
         "name": "Lauren Tan (original)"
       },

.github/workflows/ci.yml

@@ -28,6 +28,23 @@ jobs:
       - name: Typecheck
         working-directory: plugins/pstack/skills/poteto-mode/scripts
         run: bun run typecheck
+      - name: Install Statechart
+        working-directory: plugins/pstack/skills/statechart/scripts
+        run: bun install --frozen-lockfile
+      - name: Typecheck Statechart
+        working-directory: plugins/pstack/skills/statechart/scripts
+        run: bun run typecheck
+      - uses: actions/setup-java@v4
+        with:
+          distribution: temurin
+          java-version: '25'
+      - name: Fetch pinned TLC
+        run: |
+          curl -fsSL --retry 3 --output "$RUNNER_TEMP/tla2tools-1.7.4.jar" https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar
+          echo "936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88  $RUNNER_TEMP/tla2tools-1.7.4.jar" | sha256sum --check --strict
+      - name: Test Statechart with TLC
+        working-directory: plugins/pstack/skills/statechart/scripts
+        run: JAVA="$JAVA_HOME/bin/java" TLA2TOOLS="$RUNNER_TEMP/tla2tools-1.7.4.jar" bun run test
       - name: Test fork maintenance
         run: python3 tests/test-fork-maintenance.py
       - name: Test session-start hook

.gitignore

@@ -11,3 +11,6 @@
 
 # bun deps for the vendored poteto-mode scripts (bootstrap.ts installs them on first run)
 plugins/pstack/skills/poteto-mode/scripts/node_modules/
+
+# Statechart development dependencies
+plugins/pstack/skills/statechart/scripts/node_modules/

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.7 adds Statechart and Ketchup Video
+
+Cursor baseline: [0.15.35](https://github.com/cursor/plugins/tree/ab1f702ce8e8b6557edb56b09f52cde8bfb83f17/pstack). [Issue #168](https://github.com/arjitj2/open-pstack/issues/168). [PR #176](https://github.com/arjitj2/open-pstack/pull/176). Tag [v1.17.7](https://github.com/arjitj2/open-pstack/releases/tag/v1.17.7).
+
+Imports Cursor's Statechart compiler and skill and the Ketchup Video skill. Statechart stays model-invocable so generated formal-verification skills can invoke it by host name, documents the `TLA2TOOLS` and `JAVA` overrides and the networked first-run provisioning, and notes that a passing check over 500 states may produce no chart. Ketchup Video stays manual-only and renders its video outside the repository as its sole write exception. Watch-pr keeps fork-ancestry ordering and deadline sleep caps, check-plan matches its backtick fence delimiters, and worktree-audit probes GNU and BSD `stat` and `date` forms. Prose updates cover first-message goal restatement, Sharpen's numbered framing, Interrogate's run-proven finding ranking, Reflect's outside-cache edit destinations, and playbook rebase and handoff rules. Saved provider routing, the linear Autopilot-stack structure, review output buckets, verifier requirements, and README content remain unchanged. Validation and its limits are recorded in the PR.
+
 ## 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).

CONTRIBUTING.md

@@ -28,6 +28,8 @@ Read [AGENTS.md](AGENTS.md) and [UPSTREAM.md](UPSTREAM.md) before editing. Keep
 
 [Bun](https://bun.sh) runs the packaged TypeScript tools and tests. Node runs `check-plan.mjs`; Python 3 runs repository maintenance scripts and their tests. Install dependencies with `bun install --frozen-lockfile` in `plugins/pstack/skills/poteto-mode/scripts/`.
 
+Statechart has separate dependencies in `plugins/pstack/skills/statechart/scripts/`. Run `bun install --frozen-lockfile`, `bun run typecheck`, and `bun run test` there. Live engine tests need Java and the pinned TLC jar named in `.github/workflows/ci.yml`; set `JAVA` and `TLA2TOOLS` to their paths. Engine tests report skips when the jar is unavailable.
+
 GitHub workflows need an authenticated `gh` CLI. The worktree audit additionally uses `jq` and `rg`. Install and authenticate provider CLIs only for the worker routes you test.
 
 Skill-authoring workflows in Claude Code use `plugin-dev:skill-development`. Install that optional plugin with `/plugin marketplace add anthropics/claude-plugins-official`, then `/plugin install plugin-dev@claude-plugins-official`. It is not declared as a hard dependency because local plugin-directory loading cannot resolve cross-marketplace dependencies. See the [original dependency change](https://github.com/arjitj2/open-pstack/blob/5f0bb42dea46344c2f1961ebeebaeee135b49778/CHANGES.md#093--dependency-declaration-removed).