chore(upstream): sync latest pstack and harness versions

.github/workflows/validate.yml

@@ -45,7 +45,7 @@ jobs:
       - uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 # v5
         with:
           repository: cursor/plugins
-          ref: 11713c683fe4add4fd403ea880580abbc9e0875f
+          ref: eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10
           path: .upstream/cursor-plugins
           sparse-checkout: pstack
       - uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 # v5

README.md

@@ -441,15 +441,15 @@ cover MCP tools, so Claude Code also gets `--strict-mcp-config` and pi gets
 shell commands, and mstack has not checked whether it limits configured MCP
 tools; run Codex with a profile that has no MCP servers when that matters.
 OpenCode selects its built-in `plan` agent, which denies direct edits but still
-allows shell commands in OpenCode 1.18; use a disposable checkout when its
+allows shell commands in OpenCode 1.19; use a disposable checkout when its
 prompt-only write boundary is insufficient. Antigravity's `--mode plan` has the
 same limit: it is an agent mode, not a tool allowlist. In Antigravity 1.2.17 it
 left the workspace untouched but still wrote its own plan file under
 `~/.gemini/antigravity-cli/`. A live check also needs that
 Harness's credentials and configured model access.
 
-The read-only live prompt last passed on 2026-10-10 with Claude Code 2.1.296,
-Codex CLI 0.162.0, OpenCode 1.18.34, and pi 1.1.0 on Windows.
+The read-only live prompt was checked on 2026-10-22 with Claude Code 2.1.306,
+Codex CLI 0.163.0, OpenCode 1.19.3, and pi 1.3.0 on Windows.
 
 The Claude skill-invocation path was verified with Claude Code 2.1.267, the Kiro-Pro
 configuration, and `claude-haiku-4-5-20251001`. The check required Claude
@@ -515,16 +515,20 @@ target directory and restores backups if a commit fails.
 
 ## Included skills
 
-The current bundle contains 54 skills. It includes the 50 entries in the
-portable pstack tree, three skills adapted from `mattpocock/skills`, and the
-local `mstack-help` skill:
+The current bundle contains 60 skills. It includes the 56 shipped entries in
+the portable pstack tree, three skills adapted from `mattpocock/skills`, and
+the local `mstack-help` skill:
 
 - Engineering principles for boundaries, domain modelling, idempotence,
   verification, sequencing, and type safety.
 - Workflows for diagnosis, design review, context recovery, TDD, and agent
   instruction writing.
 - `create-verification-skill` for generating a project-specific verification
   workflow.
+- `create-formal-verification-skill` and `maintain-formal-verification-skill`
+  for TLA+ based formal verification workflows.
+- `statechart` for turning statecharts and TLA+ models into visual charts.
+- `in-your-own-words` and `sharpen` for goal restatement and prompt refinement.
 - `meta-mode` for routing a multi-step task through the capabilities available
   in the current harness.
 - `benchmark-checklist` and `correct` for vetting a measured number and for

docs/guide/01-setup.md

@@ -13,6 +13,8 @@ npx @3metajun/mstack --harness <codex|claude|opencode|pi>
 The installer reports the target directory and the number of skills it staged.
 Run it again for another Harness when you use more than one.
 
+Claude Code can load mstack through the installer command above. Its skill root and frontmatter rules differ from the shared Harness copy; see the [Harness adapter reference](../harness-adapters.md).
+
 ## Pick your models
 
 Run:
@@ -29,14 +31,16 @@ You only override what you care about. A role with no line in the rule keeps the
 
 Use `inherit-parent` for the current chat model through the Harness's documented native inheritance. A new CLI process needs `run-role --parent-model <known-parent-model>` to use that same model. `auto` requests the Harness's default selection, which may differ from the chat model. Neither value is a model name. The `reviewer` role accepts a model string or a non-empty list of unique model strings. `/interrogate` runs one reviewer per list entry. CLI fanout uses `--all-models --read-only`; select just one entry with `--model-index 0`. The `implementer` role sets the default model for `/swarm` workers unless a race names a model for each arm.
 
-## Accept the verification offer, or don't
+## Accept the verification offers, or don't
 
 At the end of setup, `/setup-mstack` looks for a way to prove app behavior in your project, either a `verify-*` skill or an existing harness. If it finds neither, it offers once to generate one with [`/create-verification-skill`](../../skills/create-verification-skill/SKILL.md).
 
 Say yes and it writes `verify-<app>/` under the active Harness's project skill root. See [the project skill paths](../../skills/create-verification-skill/references/harness-paths.md) for the root used by each Harness. The generated skill teaches agents to drive your app the way a user does, and setup proves it once before handing it over. Say no and setup moves on. You can run `/create-verification-skill` yourself any time. [Verify and ship](./06-verify-and-ship.md#create-a-project-verification-skill) covers it in depth.
 
 If you're new to mstack, say yes. An agent that can check its own work keeps going until the check passes. An agent that can't hands every result back to you to check by hand. Of everything in this guide, the verification skill pays off the most.
 
+Then setup offers once to generate a formal verification skill with [`/create-formal-verification-skill`](../../skills/create-formal-verification-skill/SKILL.md), unless the project already has one. Tests check the cases someone thought to write. A formal verification skill checks one key property of your code, such as "a job never runs twice at once", in every case within a stated scope. Say yes when your code has concurrency, retries, a state machine, or a parser, where a bug is costly and tests rarely reach the case that breaks. Otherwise say no, and run it later if that changes. [Verify and ship](./06-verify-and-ship.md#prove-a-property-with-a-formal-verification-skill) covers it.
+
 After setup, start a new session. The model configuration applies to new sessions.
 
 ## Keep the cost in check
@@ -58,6 +62,6 @@ Pick something real but small, and describe it the way you'd describe it to a co
 
 Watch the todo list. Its first items are the matched playbook's steps copied in, the Feature playbook for this prompt. If `/meta-mode` skips a step, the step stays in the list with `skip: <reason>`, so you can see what it chose not to do.
 
-From here you can type normal follow-ups. To keep `/meta-mode` on for the whole chat, pick it from the `/` menu with Option+Enter (Mac) or Alt+Enter (Windows) instead of Enter. That makes it a [Custom Mode](https://cursor.com/docs/skills), which stays in context on every turn until you exit it. Custom Modes are available in the Agents Window and the CLI. Plain Enter attaches the skill to one message, and it fades as the chat moves on.
+From here you can type normal follow-ups. To keep `/meta-mode` on for the whole chat, pick it from the `/` menu with Option+Enter (Mac) or Alt+Enter (Windows) instead of Enter. That makes it a [Custom Mode](https://cursor.com/docs/skills#using-a-skill-as-a-custom-mode), which stays in context on every turn until you exit it. Custom Modes are available in the Agents Window and the CLI. Plain Enter attaches the skill to one message, and it fades as the chat moves on.
 
 Next: [Route work through `/meta-mode`](./02-meta-mode.md).

docs/guide/02-meta-mode.md

@@ -25,7 +25,7 @@ flowchart TD
     J --> K
 ```
 
-The diagram shows the common routes. There are also playbooks for hillclimbing a metric, diagnosing runtime symptoms and captured traces, prototypes, visual parity, authoring and evaluating skills, autonomous runs, babysitting a PR or stack to merge-ready, shipping a verified stack, running a PR queue on autopilot, orchestrating project-scale programs, session pickup, pausing safely, multi-phase plans, and worktree cleanup. The [playbook directory](../../skills/meta-mode/playbooks/) has the full set.
+The diagram shows the common routes. There are also playbooks for hillclimbing a metric, diagnosing runtime symptoms and captured traces, prototypes, visual parity, authoring and evaluating skills, autonomous runs, opening a PR, babysitting a PR or stack to merge-ready, shipping a verified stack, running a PR queue or a stack on autopilot, orchestrating project-scale programs, session pickup, pausing safely, multi-phase plans, and worktree cleanup. The [playbook directory](../../skills/meta-mode/playbooks/) has the full set.
 
 ## Say the goal, not the ceremony
 
@@ -64,7 +64,15 @@ For a noisy report, such as a long thread or a vague bug, make the restatement t
 /meta-mode read this thread. restate the underlying issue in your own words, in plain english. don't change any code yet.
 ```
 
-A misreading shows up in the restatement, before any code exists. Correct it there, and it costs you one message instead of one wrong fix.
+A misreading shows up in the restatement, before any code exists. Correct it there, and it costs you one message instead of one wrong fix. For the restatement alone, with no playbook, run [`/in-your-own-words`](../../skills/in-your-own-words/SKILL.md). It restates what the agent thinks your goals are and what problem you're trying to solve.
+
+When you're unsure whether a prompt is aimed right, run [`/sharpen`](../../skills/sharpen/SKILL.md) on it before you send it:
+
+```text
+/sharpen write a migration guide for the v2 config format.
+```
+
+The agent says what a top professional would do that you didn't ask for, the rawest material they would start from, the methods and tools they would use, and what other than you or the agent would show the result is right. Then it rewrites your prompt to ask for exactly that, deeper but not bigger, and leaves your choices open. It doesn't do the task. Read the rewrite, then send it, for example with `/meta-mode`.
 
 ## Follow up short
 

docs/guide/03-understand.md

@@ -30,17 +30,17 @@ Ask the question you actually have. [`/how`](../../skills/how/SKILL.md) reads th
 /why was the retry limit set to five? does the reason still hold?
 ```
 
-[`/why`](../../skills/why/SKILL.md) works like a detective on a cold case. It starts from source control, then queries whatever evidence categories your MCPs expose, such as the issue tracker, long-form docs, team chat, observability, error tracking, and analytics, all in parallel. The report cites everything, separates direct evidence from inference, and says "appears to" when the record is thin. A null result gets reported too, because "nobody wrote down why" is itself an answer.
+[`/why`](../../skills/why/SKILL.md) starts from source control, then queries whatever evidence categories your MCPs expose, such as the issue tracker, long-form docs, team chat, observability, error tracking, and analytics, all in parallel. The report cites everything, separates direct evidence from inference, and says "appears to" when the record is thin. A null result gets reported too, because "nobody wrote down why" is itself an answer.
 
-The two compose naturally. `do why first then how` is a perfectly good prompt when you suspect the history explains the mess.
+The two compose naturally. `do why first then how` is a good prompt when you suspect the history explains the mess.
 
 ## Actually understand it with `/teach`
 
 ```text
 /teach me how this PR changes retries. convince me it fixes the cause and not the symptom.
 ```
 
-[`/teach`](../../skills/teach/SKILL.md) is for when a summary isn't enough. It runs `/how` and `/why`, for a small change maybe just one of them, and weaves the findings into a plain explanation that builds up diagram by diagram. The "convince me" framing is worth stealing. It turns the explanation into an argument you can poke at instead of a tour.
+[`/teach`](../../skills/teach/SKILL.md) is for when a summary isn't enough. It runs `/how` and `/why`, for a small change maybe just one of them, and weaves the findings into a plain explanation that builds up diagram by diagram. The "convince me" framing is worth reusing. It turns the explanation into an argument you can test instead of a tour.
 
 It works on the agent's own choices too:
 

docs/guide/04-design.md

@@ -2,7 +2,7 @@
 
 One attempt at a hard design locks in the first shape the model thought of. `/architect` settles types and boundaries before implementation. `/arena` runs several attempts at the same brief and merges the best parts. `/interrogate` has other models try to break the result. When the job is coverage rather than design synthesis, `/swarm` fans out slices or races and aggregates their results.
 
-The two most common design mistakes are taking the agent's first design and polishing a plan that no code has tested. This page fixes both. You plan through code: prototypes answer the open questions, a README or tutorial sets the target, and the written plan comes last.
+The two most common design mistakes are taking the agent's first design and polishing a plan that no code has tested. This page fixes both. You plan through code. Prototypes answer the open questions, a README or tutorial sets the target, and the written plan comes last.
 
 ![Three robots draft competing bridge models at their own tables under /architect, /arena, and /interrogate panels, while a judge robot with a clipboard inspects skeptically.](./images/design.jpg)
 

docs/guide/05-build-and-clean.md

@@ -1,6 +1,6 @@
 # Build the change and clean the diff
 
-The build playbooks share one discipline. Say what you observed, let the playbook demand the evidence. This page shows what to put in the prompt for each common build task, then the cleanup habit that keeps diffs reviewable.
+The build playbooks share one discipline. Say what you observed, and let the playbook demand the evidence. This page shows what to put in the prompt for each common build task, then the cleanup habit that keeps diffs reviewable.
 
 ## Prompt each build playbook with what you know
 
@@ -22,7 +22,7 @@ A refactoring prompt pins behavior before structure moves:
 /meta-mode move parsing into one module, zero behavior change. record the current output first and prove it's unchanged after.
 ```
 
-A perf prompt states the measurement, not a vibe:
+A perf prompt states the measurement, not an impression:
 
 ```text
 /meta-mode startup takes 1.8s on this fixture. trace it, fix the measured cause, show me before and after.