jiangkoumo · Oct 28, 2026 · Oct 28, 2026 · Oct 28, 2026 · Oct 28, 2026
diff --git a/adapters/pi/overrides/skills/create-formal-verification-skill/SKILL.md.template b/adapters/pi/overrides/skills/create-formal-verification-skill/SKILL.md.template
@@ -33,6 +33,10 @@ Pick the tool that answers the question at the lowest cost: a model checker, a p
 
 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.
 
+If the check is a TLA+ model, tell the next agent to read every result with the pstack [`/statechart`](../statechart/SKILL.md) skill. It shows each invariant violation the checker finds as its shortest path in plain words. When the check passes, `/statechart` draws a chart of how the system moves between states. Refer to `/statechart` by name. Its commands, options, and file paths change between releases and machines, so copy none of them into the generated skill or its scripts.
+
+On Pi, run formal TLC verification through the restricted `verification_exec` entry with a structured `tlc` request, repository-relative model and config paths in a read-only repository, and only whitelisted options. Draw charts through the `/statechart` entry in the parent shell, currently `node <package>/adapters/pi/statechart/entry.mjs`; resolve that entry from the installed skill at run time. Chart rendering does not establish a formal verification pass, and a restricted TLC run does not replace chart rendering. Keep concrete jar paths and machine-specific paths out of the generated skill and its scripts.
+
 ## Prove it before you hand off
 
 Follow the generated skill once, as the next agent would, on a scratch change that breaks the property in the real code. It must catch the break. Then drop the scratch change and confirm that the check is back where it started: passing, or failing only on the findings you will report. A verify skill that was never run is a draft. If the skill misses the break or a step does not run, fix the skill or the verification, not the scratch change.
@@ -65,13 +69,13 @@ Twice, on the real code the property guards, make a deliberate break — remove
 
 ### What the generated skill must record
 
-Record the tool version and how it was resolved (jar path plus Java major version), the exact command and options, the sync commit — the commit at which you actually ran the check — and the bounds and assumptions the check relies on, including what is left out. Tell the next agent to move the sync commit forward only after it re-ran the check at the new commit and confirmed the verification still describes the code there. A skill that was never executed, or that has only ever seen a passing run, is a draft, and the handoff must say `draft` instead of reporting a verified property.
+Record the tool version and how it was resolved (the jar configuration source plus Java major version, without a concrete jar or machine-specific path), the exact command and options, the sync commit — the commit at which you actually ran the check — and the bounds and assumptions the check relies on, including what is left out. Tell the next agent to move the sync commit forward only after it re-ran the check at the new commit and confirmed the verification still describes the code there. A skill that was never executed, or that has only ever seen a passing run, is a draft, and the handoff must say `draft` instead of reporting a verified property.
 
 ### Completion self-check
 
 Before declaring this task complete or handing off, execute the completion self-check. The generation is not complete until every item below is satisfied:
 - Re-run every "Run it" command documented in the generated SKILL.md from the target repository. Confirm that all quantities, counts, and conclusions in the command output (such as step counts, state counts, distinct states, queue/member counts, and scenario totals) match the descriptions in SKILL.md exactly. Any discrepancy between execution output and the written skill must be reconciled before finishing.
-- The Record section in the generated skill must be fully written, specifying the tool version and resolution (jar path plus Java major version), exact command and options, sync commit, bounds, assumptions, and explicit exclusions of what is left out.
+- The Record section in the generated skill must be fully written, specifying the tool version and resolution (the jar configuration source plus Java major version, without a concrete jar or machine-specific path), exact command and options, sync commit, bounds, assumptions, and explicit exclusions of what is left out.
 - Deliver the final completion report covering:
   1. The verified scope and target promise;
   2. Concrete evidence of deliberate breakage: the two break-and-restore cycles on the real code, citing the modified code, the observed counterexample in code terms, and non-zero failing exit status;

diff --git a/adapters/pi/overrides/skills/poteto-help/SKILL.md.template b/adapters/pi/overrides/skills/poteto-help/SKILL.md.template
@@ -72,6 +72,7 @@ The default answer is `/skill:poteto-mode`, which runs most of the others when i
 | Understand a change or subsystem, explained plainly | [`/teach`](../teach/SKILL.md) |
 | Catch up on their own recent work on a topic | [`/recall`](../recall/SKILL.md) |
 | Catch up on what changed in this chat since their last message, in plain words and small visuals, with every item waiting on them listed and decidable from the reply alone | [`/ketchup`](../ketchup/SKILL.md) |
+| Catch up like `/ketchup`, in a short silent video of slides, with the waiting calls as text under it | [`/ketchup-video`](../ketchup-video/SKILL.md) |
 | Know what a small diff could break outside itself | [`/blast-radius`](../blast-radius/SKILL.md) |
 | Settle types and module shape before code that crosses a function boundary | [`/architect`](../architect/SKILL.md) |
 | Get several attempts at one brief, merged into the best one | [`/arena`](../arena/SKILL.md) |
@@ -87,7 +88,7 @@ The default answer is `/skill:poteto-mode`, which runs most of the others when i
 | 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) |
-| Show a PM or designer what the user sees as a chart checked by a model, with each bug drawn as a numbered path, turn an agreed chart into a TLA+ skeleton, or audit the code against its TLA+ spec | [`/statechart`](../statechart/SKILL.md) |
+| Show a PM or designer what the user sees as a chart checked by a TLA+ model, with the shortest path to each state that breaks a rule | [`/statechart`](../statechart/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/adapters/pi/statechart/skill-replacements.json b/adapters/pi/statechart/skill-replacements.json
@@ -4,6 +4,11 @@
     "to": "node <package>/adapters/pi/statechart/entry.mjs SPEC.tla [--config FILE] [--view FILE] [--out DIR]",
     "reason": "Route command through the Pi boundary, which never installs TLC automatically."
   },
+  {
+    "from": "`scripts/statechart.ts` is TypeScript, so run it with a runtime that can execute TypeScript.",
+    "to": "The Pi entry runs the TypeScript compiler with the package's supported Node version; always use `node <package>/adapters/pi/statechart/entry.mjs` and never run the upstream compiler or launcher directly.",
+    "reason": "The raw upstream script or launcher can automatically install tools through mise; Pi must run through entry.mjs so the entry hook enforces the no-install boundary."
+  },
   {
     "from": "The first run installs TLC and Java with mise and needs the network.",
     "to": "Set TLA2TOOLS (or TLA2TOOLS_JAR) and JAVA to the already-installed TLC jar and Java binary. Pi does not automatically install mise, TLC, or Java.",

diff --git a/docs/fidelity.md b/docs/fidelity.md
@@ -1,14 +1,14 @@
 # pi-pstack upstream fidelity
 
-Files: 115  flagged: 4  overall kept (excluding Cursor substitutions): 4500/4785 = 94%
+Files: 149  flagged: 4  overall kept (excluding Cursor substitutions): 4753/5039 = 94%
 
 Thresholds: kept >= 0.85, reworded >= 0.55; flag if kept < 70% or lost > 3
 
 | File | Upstream | Kept | Reworded | Lost | Cursor subst | Port-only | Kept % | Flag |
 |---|---|---|---|---|---|---|---|---|
 | skills/make-bot-ui/SKILL.md | 73 | 0 | 0 | 73 | 2 | 0 | MISSING | ! |
 | skills/setup-pstack/SKILL.md | 53 | 0 | 0 | 53 | 9 | 0 | MISSING | ! |
-| skills/poteto-help/SKILL.md | 173 | 140 | 8 | 11 | 14 | 18 | 88% | ! |
+| skills/poteto-help/SKILL.md | 173 | 139 | 9 | 11 | 14 | 19 | 87% | ! |
 | skills/poteto-mode/playbooks/orchestrate.md | 204 | 183 | 15 | 4 | 2 | 45 | 91% | ! |
 | skills/poteto-mode/playbooks/worktree-cleanup.md | 30 | 21 | 7 | 2 | 0 | 59 | 70% |  |
 | skills/how/SKILL.md | 24 | 16 | 5 | 1 | 2 | 22 | 73% |  |
@@ -48,11 +48,11 @@ Thresholds: kept >= 0.85, reworded >= 0.55; flag if kept < 70% or lost > 3
 | skills/poteto-mode/playbooks/eval.md | 37 | 35 | 0 | 1 | 1 | 27 | 97% |  |
 | skills/create-verification-skill/SKILL.md | 73 | 71 | 2 | 0 | 0 | 34 | 97% |  |
 | skills/how/references/explainer-prompt.md | 39 | 38 | 0 | 1 | 0 | 1 | 97% |  |
-| skills/statechart/SKILL.md | 77 | 75 | 1 | 1 | 0 | 27 | 97% |  |
 | skills/poteto-mode/references/bugbot-triage.md | 94 | 92 | 1 | 1 | 0 | 5 | 98% |  |
 | skills/reflect/references/synthesizer.md | 49 | 47 | 0 | 1 | 1 | 1 | 98% |  |
 | skills/why/references/synthesizer-prompt.md | 95 | 93 | 1 | 1 | 0 | 8 | 98% |  |
 | skills/benchmark-checklist/SKILL.md | 50 | 49 | 0 | 1 | 0 | 29 | 98% |  |
+| skills/statechart/SKILL.md | 105 | 103 | 0 | 2 | 0 | 27 | 98% |  |
 | skills/poteto-mode/playbooks/babysit.md | 104 | 102 | 1 | 0 | 1 | 36 | 99% |  |
 | agents/comment-sicko.md | 29 | 29 | 0 | 0 | 0 | 18 | 100% |  |
 | agents/poteto-agent.md | 10 | 8 | 0 | 0 | 2 | 2 | 100% |  |
@@ -62,7 +62,7 @@ Thresholds: kept >= 0.85, reworded >= 0.55; flag if kept < 70% or lost > 3
 | skills/blast-radius/SKILL.md | 51 | 51 | 0 | 0 | 0 | 30 | 100% |  |
 | skills/bro/SKILL.md | 3 | 3 | 0 | 0 | 0 | 0 | 100% |  |
 | skills/correct/SKILL.md | 28 | 28 | 0 | 0 | 0 | 22 | 100% |  |
-| skills/create-formal-verification-skill/SKILL.md | 51 | 51 | 0 | 0 | 0 | 52 | 100% |  |
+| skills/create-formal-verification-skill/SKILL.md | 51 | 51 | 0 | 0 | 0 | 62 | 100% |  |
 | skills/create-verification-skill/references/feature-map-example/README.md | 34 | 34 | 0 | 0 | 0 | 0 | 100% |  |
 | skills/create-verification-skill/references/feature-map-example/create-note.md | 36 | 36 | 0 | 0 | 0 | 0 | 100% |  |
 | skills/create-verification-skill/references/feature-map-example/search.md | 50 | 50 | 0 | 0 | 0 | 0 | 100% |  |
@@ -107,6 +107,40 @@ Thresholds: kept >= 0.85, reworded >= 0.55; flag if kept < 70% or lost > 3
 | skills/reflect/references/judgment-reviewer.md | 44 | 42 | 0 | 0 | 2 | 0 | 100% |  |
 | skills/reflect/references/tooling-reviewer.md | 54 | 52 | 0 | 0 | 2 | 0 | 100% |  |
 | skills/sharpen/SKILL.md | 8 | 8 | 0 | 0 | 0 | 4 | 100% |  |
+| skills/statechart/references/render.md | 25 | 25 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/Counter/report.md | 4 | 4 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterAction/report.md | 6 | 6 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterDeadlock/report.md | 8 | 8 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterFan/report.md | 3 | 3 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterGuard/report.md | 5 | 5 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterInitPast/report.md | 6 | 6 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterInitPastHolds/report.md | 3 | 3 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterInstance/report.md | 4 | 4 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterJump/report.md | 5 | 5 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterLoop/report.md | 4 | 4 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterOrder/report.md | 8 | 8 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterRules/report.md | 7 | 7 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterStart/report.md | 5 | 5 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterStop/report.md | 2 | 2 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterTie/report.md | 9 | 9 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterTieInGraph/report.md | 3 | 3 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/CounterView/report.md | 9 | 9 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/DieHard/report.md | 4 | 4 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/FirstRule/report.md | 6 | 6 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/HiddenClock/report.md | 7 | 7 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/Login/report.md | 4 | 4 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/LoginGuarded/report.md | 5 | 5 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/LoginParallel/report.md | 12 | 12 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/MediaPlayer/report.md | 9 | 9 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/MediaPlayerFixed/report.md | 6 | 6 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/MediaPlayerProps/report.md | 12 | 12 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/PickWorker/report.md | 4 | 4 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/Shadow/report.md | 6 | 6 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/SpacedNames/report.md | 4 | 4 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/TwoPhase/report.md | 14 | 14 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/TwoPhaseFixed/report.md | 8 | 8 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/TypeGuard/report.md | 5 | 5 | 0 | 0 | 0 | 0 | 100% |  |
+| skills/statechart/scripts/test/corpus/UserNoDeadlock/report.md | 4 | 4 | 0 | 0 | 0 | 0 | 100% |  |
 | skills/tdd/SKILL.md | 32 | 32 | 0 | 0 | 0 | 0 | 100% |  |
 | skills/technical-writing/SKILL.md | 136 | 136 | 0 | 0 | 0 | 0 | 100% |  |
 | skills/typescript-best-practices/SKILL.md | 33 | 33 | 0 | 0 | 0 | 1 | 100% |  |
@@ -343,9 +377,6 @@ Thresholds: kept >= 0.85, reworded >= 0.55; flag if kept < 70% or lost > 3
 ### skills/how/references/explainer-prompt.md
 - Use Read, Grep, and Glob as needed.
 
-### skills/statechart/SKILL.md
-- The first run installs TLC and Java with mise, which downloads about 305 MB and needs the network.
-
 ### skills/poteto-mode/references/bugbot-triage.md
 - Reply with a short reason and resolve the thread.
 
@@ -357,3 +388,7 @@ Thresholds: kept >= 0.85, reworded >= 0.55; flag if kept < 70% or lost > 3
 
 ### skills/benchmark-checklist/SKILL.md
 - Check the load average with uptime and the core count with nproc.
+
+### skills/statechart/SKILL.md
+- scripts/statechart.ts is TypeScript, so run it with a runtime that can execute TypeScript.
+- The first run installs TLC and Java with mise and needs the network.
diff --git a/docs/port-map.json b/docs/port-map.json
@@ -469,7 +469,7 @@
       "disposition": "ported",
       "phase": "P5",
       "destination": "skills/poteto-help/SKILL.md",
-      "reason": "poteto-mode 路由表取代本批入口；完整技能索引随其余技能落地",
+      "reason": "已适配完整技能索引；已吸收上游 519d36aa 的 statechart 措辞与 ketchup-video 行",
       "audit": {
         "sourceRead": true,
         "relativeLinks": [

diff --git a/docs/skill-audit.md b/docs/skill-audit.md
@@ -38,7 +38,7 @@
 | 技能 create-verification-skill | P5 | 采用自编 Pi 作者流程；本轮由 prove-it-works 的脚本化检查替代 |
 | 技能 how | P3 | investigation 流程已内嵌 how 的输出结构；完整版依赖子代理 |
 | 技能 maintain-verification-skill | P5 | 采用自编 Pi 作者流程；依赖并行源码读取 |
-| 技能 poteto-help | P5 | poteto-mode 路由表取代本批入口；完整技能索引随其余技能落地 |
+| 技能 poteto-help | P5 | 已适配完整技能索引；已吸收上游 519d36aa 的 statechart 措辞与 ketchup-video 行 |
 | 技能 setup-pstack | P2 | P2 已用 /setup-pstack 扩展命令替代：独立 JSON、实际模型目录与 thinking 校验，不沿用 .mdc；见 validation-p2.md |
 | 技能 show-me-your-work | P5 | principle-prove-it-works 现保留本地证据记录；TSV 决策轨迹依赖会话 transcript |
 | Benny 技能 reproduce-and-fix-issues | P5 | Cursor Benny/Slack/Linear 自动化不在 Pi 范围；本地替代为 Bug fix + 手动 issue 复现 |

diff --git a/scripts/statechart-adapter.test.mjs b/scripts/statechart-adapter.test.mjs
@@ -28,6 +28,26 @@ async function fakeMise() {
   return bin;
 }
 
+test('generated statechart skill routes executable examples through the Pi entry', async () => {
+  const skill = await readFile(resolve(root, 'skills/statechart/SKILL.md'), 'utf8');
+  const body = skill.replace(/^---\n[\s\S]*?\n---\n/, '');
+  assert.ok(!body.includes('`scripts/statechart.ts` is TypeScript, so run it with a runtime that can execute TypeScript.'),
+    'generated guidance must not tell agents to run the raw TypeScript compiler');
+
+  const shellBlocks = [...body.matchAll(/^```(?:sh|bash|shell|zsh|console)[ \t]*\n([\s\S]*?)^```[ \t]*$/gm)];
+  assert.ok(shellBlocks.length > 0, 'the skill must include an executable shell example');
+  const commands = shellBlocks.flatMap(([, block]) => block.split('\n'))
+    .map(line => line.trim()).filter(line => line && !line.startsWith('#')).join('\n');
+  assert.doesNotMatch(commands, /\bscripts\/statechart(?:\.ts)?(?=$|[\s"'`;|&])/m,
+    'shell examples must not execute the upstream compiler or launcher');
+  assert.match(commands, /^(?:\$\s*)?node <package>\/adapters\/pi\/statechart\/entry\.mjs\s+SPEC\.tla\b/m,
+    'an executable Pi entry example must remain available');
+  assert.doesNotMatch(body, /\b(?:first|initial)[ -]run\s+(?:will\s+)?(?:automatically\s+)?(?:installs?|downloads?|sets?\s+up)\b/i,
+    'the skill must not promise installation on the first run');
+  assert.doesNotMatch(body, /\b(?:installs?|downloads?|sets?\s+up)\b[^.\n]*\b(?:on|during)\s+(?:the\s+)?(?:first|initial)[ -]run\b/i,
+    'the skill must not promise installation on the first run');
+});
+
 test('Pi adapter never installs TLC through mise and explains how to install it', async () => {
   const bin = await fakeMise();
   try {