[MEDIUM] Update pstack and add formal verification skills

.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.8.0",
+      "version": "1.15.0-adam.20261019",
       "author": {
         "name": "Lauren Tan (original)"
       },

.claude/skills/verify-open-pstack/SKILL.md

@@ -25,7 +25,11 @@ EVIDENCE="$SESSION/live" # must not exist yet
 .claude/skills/verify-open-pstack/scripts/verify.sh run --pr "$PR" --feature claude:project-skill --self-test --output "$EVIDENCE"
 ```
 
-Pick the features that exercise the PR's changed behavior and pass each as `--feature <harness>:<feature>`, repeatable. List the same features in the PR body, where review sees them. A runtime change needs at least one `--feature`; the run fails before any install without one. The run exercises only the named features, plus `project-skill` in both harnesses under `--self-test`. It never falls back to the classified set, and a full sweep is never the default.
+Pick the features that exercise the PR's changed behavior and pass each as `--feature <harness>:<feature>`, repeatable. List the same features in the PR body, where review sees them. The run exercises only the named features, plus `project-skill` in both harnesses when classification reaches it or under `--self-test`. Before any install or GitHub write, `verify.sh run` makes three checks:
+
+- Scope: a runtime change needs at least one `--feature`, and every named feature must be in the PR's classified reach. The refusal names each refused feature and the reachable set. A manifest change that only bumps the version reaches only `hook:startup` in that manifest's harness.
+- Count: the run prints the number of headless sessions the named features and automatic `project-skill` checks will start.
+- Limit: above 12 sessions, the run refuses unless you pass `--wide "<reason>"`. The reason must be printable ASCII, at most 160 characters, without backticks or angle brackets. The evidence comment records the planned count and the reason.
 
 Reuse the Claude Code and Codex logins you already have; no extra login or credential source flags. Omit `--self-test` for ordinary plugin verification; it is mandatory for this skill's delivery. An agent runs and judges the whole gate from a non-TTY shell; nothing prompts a person. `--runner-route PROVIDER:MODEL@EFFORT`, repeatable, replaces the runner recipe's default route, a role default from the installed candidate's model catalog, for each parent whose provider differs from the route's.
 
@@ -41,7 +45,7 @@ Temporary, GitHub, and fixture state remain run-owned; Git configuration is disa
 
 ## Drive
 
-Read `features/README.md` and the document for every named feature. Path classification still runs: it decides whether the PR has a runtime change, and an unmapped path fails closed. It does not choose the features; the agent does. `no runtime change` launches no harness unless `--self-test` is requested.
+Read `features/README.md` and the document for every named feature. Path classification computes the features the PR can reach, and an unmapped path fails closed. It does not choose the features; the agent does. `no runtime change` launches no harness unless `--self-test` is requested.
 
 Create detached exact-head candidate checkouts and run-owned temporary/fixture state, only for harnesses with a named feature. Every named feature resolves to a recipe in `features/recipes.ts` before the first session starts: one or more cases, each with a fixture, a prompt, and an assertion the trusted parent evaluates. A feature without a recipe fails as `missing-recipe:<harness>/<feature>`; `assets:codex` fails as `unsupported-native-consumer` until it has a recipe. Each case runs as one fresh headless session, sequentially, and setup never runs alongside anything.
 
@@ -71,10 +75,10 @@ Each headless session exits on its own. Verify any setup restoration before publ
 
 - `scripts/verify.sh doctor --output <fresh-absolute-external-directory>`: parent capability and login-state report, no installation/publication.
 - `scripts/verify.sh doctor --candidate --output <fresh-run-owned-directory>`: candidate-safe self-test probe; no publisher authentication probing.
-- `scripts/verify.sh run --pr <positive-number> --feature <harness>:<feature>... [--self-test] [--runner-route PROVIDER:MODEL@EFFORT]... --output <fresh-absolute-external-directory>`: headless exact-head verification of the named features with machine-checked recipes; no terminal or prompts. The evidence comment lists only the features that ran.
+- `scripts/verify.sh run --pr <positive-number> --feature <harness>:<feature>... [--self-test] [--runner-route PROVIDER:MODEL@EFFORT]... [--wide <reason>] --output <fresh-absolute-external-directory>`: headless exact-head verification of the named features with machine-checked recipes; no terminal or prompts. The evidence comment lists only the features that ran.
 - `features/recipes.ts`: per-feature headless cases and assertions.
 - `bun run test` and `bun run typecheck`: development checks after a separate frozen dependency install, not live proof.
-- `features/registry.json`: maintained path ownership; it decides runtime versus no runtime change, and unknown runtime paths block.
+- `features/registry.json`: maintained path ownership; it decides which features a PR can reach, and unknown runtime paths block.
 
 Read receipts as data, never shell input. Do not put credentials in prompts or public artifacts.
 
@@ -99,3 +103,13 @@ Read receipts as data, never shell input. Do not put credentials in prompts or p
 - scripts/verify.sh
 - scripts/verify.test.ts
 - scripts/verify.ts
+
+## Subscription account routing
+
+When the operator uses the harness account router, pass `--account-router /absolute/path/to/account-router` and one explicit `--native-model HARNESS:MODEL@EFFORT` for each selected harness. On Adam's model sheet these are `claude:opus@high` and `codex:gpt-6-astra@xhigh`. The router must have its matching `pstack-verify-run` launcher installed beside it. Missing support stops the run; never retry native sessions outside the router.
+
+The launcher receives one private request per native case, chooses the account through the router, validates the final isolated configuration against that admitted subscription, and links Codex authentication only for the admitted session. Plugin installation needs no authentication. Each case retains its account and terminal receipts privately; publication contains only their hashes. A failed or uncertain session retains candidate state for inspection. Cancellation asks the router to stop its child and write terminal evidence.
+
+This route supports ordinary single-session recipes with fixed native permissions. Setup, external runner exercises, and agent preload fail before the first session; they need a separate admitted contract. The poteto-mode invocation exercise resolves a supplied model sheet without dispatch. Formal creation and maintenance use the bounded capacity fixture described in `features/skill-invocation.md`.
+
+Routed Claude sessions use the launcher's native permission channel for Write/Edit of the formal fixtures' `.claude/skills/verify-capacity/SKILL.md`. The operator must approve that scoped policy before enabling it. Other permission requests are denied and decisions stay in the private terminal receipt. Use native file tools for that skill; a denied edit fails the case. The maintenance assertion still requires the actual skill's sync commit to advance.

.claude/skills/verify-open-pstack/features/README.md

@@ -1,13 +1,13 @@
 # Maintained feature map
 
-The agent running the verifier picks the features that exercise the PR's changed behavior, passes each as `--feature <harness>:<feature>`, and lists them in the PR body, where review sees them. The run exercises only those features, plus `project-skill` in both harnesses under `--self-test`. A full sweep of every feature the paths touch is never the default. The ownership table below says which surfaces a changed path can affect, to guide that choice; it does not select them.
+The ownership table below says which features a changed path reaches. `SKILL.md` says how to pick the named features from that reach and how `verify.sh run` checks them.
 
-`registry.json` is the machine-readable ownership map. Classification decides whether a PR has a runtime change, which requires at least one `--feature`. `core.ts` supports exact paths and terminal `/**` only. Unknown paths fail closed; rename classification includes both paths. Runtime markdown, references, playbooks, hooks, manifests, and scripts are runtime even when their extension looks documentary.
+`registry.json` is the machine-readable ownership map. Classification turns the changed paths into the reachable `<harness>:<feature>` set; an empty set is `no runtime change`. `core.ts` supports exact paths and terminal `/**` only. Unknown paths fail closed; rename classification includes both paths. Runtime markdown, references, playbooks, hooks, manifests, and scripts are runtime even when their extension looks documentary.
 
 | Ownership | Surfaces a change can affect |
 | --- | --- |
 | `skills` | One `skill-invocation:<name>` exercise per selected skill, in both harnesses |
-| `shared` | All listed skills, setup, runner, and shipped tools in both harnesses; `hook:startup` for `plugins/pstack/hooks/**` |
+| `shared` | All listed skills, setup, runner, shipped tools, and `hook:startup` in both harnesses, and Claude's `agent-preload:poteto-agent`; a version-only manifest change reaches less, as described below |
 | `catalog` | The generated model catalog and native agents, and the registry sources: `catalog`, `setup`, and `runner`, and no skill check |
 | `assets` | Installed UI/resource surface for each actual consumer found in the pinned plugin manifests |
 | `setup` | Installed setup/model configuration with byte-exact daily Claude file restoration before publication |
@@ -16,11 +16,15 @@ The agent running the verifier picks the features that exercise the PR's changed
 | `project` | Native discovery/invocation of this verifier in both harnesses |
 | `nonRuntime` | Explicit ordinary repository documentation, policy, non-shipped assets, and unit-test paths; no plugin harness launch |
 
+A change to `plugins/pstack/.claude-plugin/plugin.json`, `.claude-plugin/marketplace.json`, or `plugins/pstack/.codex-plugin/plugin.json` is version-only when the merge base and the head hold the same regular file with the same mode, both sides parse as JSON objects, at least one version string changed (top-level `version`, or `plugins[].version` in the marketplace), and nothing else differs. A version-only change reaches only `hook:startup`: the two Claude files in Claude, the Codex manifest in Codex. `.agents/plugins/marketplace.json` has no version and always takes the shared expansion.
+
 Asset ownership is consumer-driven, not blanket shared ownership. Inspect the exact candidate's plugin manifests. At present, `plugins/pstack/assets/logo.png` is referenced only by `plugins/pstack/.codex-plugin/plugin.json`, so a logo-only change selects the installed Codex asset surface and does not invent a Claude exercise. New shipped assets must be added to `assets` and must have a real manifest consumer; missing, ambiguous, or unknown consumption fails closed.
 
+A registered skill's `agents/openai.yaml` controls Codex invocation and selects that skill's Codex surface. Other metadata filenames remain unmapped. The formal verification creation and maintenance skills each have their own entry in `registry.json`.
+
 `bootstrap.ts` belongs to `tools`; exercise its actual consumers, `orch` and `watch-pr`, including dependency bootstrapping rather than the unrelated external runner.
 
-Catalog paths take precedence over `shared` and over the skill match, so `references/model-catalog.md` and the generated agents select only `catalog`, `setup`, and `runner`. Each generated agent is listed by exact path; a new one is unmapped until it is added to `catalog`. Skill-owned `SKILL.md`, `references/**`, and `playbooks/**` select their skill. Additional executable paths must be registered explicitly. `core.ts` assigns the Codex transcript resolver, `poteto-mode/scripts/resolve-codex-transcript.ts`, and its launcher, `poteto-mode/scripts/resolve-codex-transcript`, to `reflect` by their exact paths, so a change to it selects `skill-invocation:reflect` rather than the unrelated shipped-tool recipe. Shared consumed mappings select every dependent skill conservatively. The coverage test inventories tracked plugin files; new unmapped files block CI and runs. Deleted skill surfaces cannot silently disappear from evidence: choose a surviving documented entry point demonstrating the intended removal, or report blocked.
+Catalog paths take precedence over `shared` and over the skill match, so `references/model-catalog.md` and the generated agents select only `catalog`, `setup`, and `runner`. Each generated agent is listed by exact path; a new one is unmapped until it is added to `catalog`. Skill-owned `SKILL.md`, `references/**`, and `playbooks/**` select their skill. poteto-mode's `SKILL.md` also reaches Claude's `agent-preload:poteto-agent`, because poteto-agent preloads it. Additional executable paths must be registered explicitly. `core.ts` assigns the Codex transcript resolver, `poteto-mode/scripts/resolve-codex-transcript.ts`, and its launcher, `poteto-mode/scripts/resolve-codex-transcript`, to `reflect` by their exact paths, so a change to it selects `skill-invocation:reflect` rather than the unrelated shipped-tool recipe. Shared consumed mappings select every dependent skill conservatively. The coverage test inventories tracked plugin files; new unmapped files block CI and runs. Deleted skill surfaces cannot silently disappear from evidence: choose a surviving documented entry point demonstrating the intended removal, or report blocked.
 
 The feature documents below define sub-features, user entry points, driving instructions, and gotchas. Review each changed sub-feature in the diff. Record all changed sub-feature actions in the feature's transcript and artifact. Do not run destructive application work in the maintainer checkout.
 
@@ -35,6 +39,6 @@ The feature documents below define sub-features, user entry points, driving inst
 - `recipes.ts`: the headless cases and machine-checked assertions for every selectable feature. A named feature without one fails the run as `missing-recipe` before any session starts. A recipe proves a lookup or a read with a fixture value the model cannot derive from the prompt, such as a per-run `crypto.randomUUID()` marker, compared in the structured result. A command's text can show which tool the parent called, but it never proves what that tool read or produced, so do not add command-text or tool-output pattern checks for that.
 - `agent-preload:poteto-agent` (Claude only): the parent dispatches `pstack:poteto-agent` through the Agent tool and asks it for the first Core principle of the preloaded poteto-mode skill without invoking `Skill` or reading files. The check needs that Agent call, `Laziness Protocol` in the reply the parent writes to `result.md`, and no `Skill` call or `Read` of poteto-mode's `SKILL.md` among the child's own tool calls.
 
-Consumed `AGENTS.md`/`CLAUDE.md` instructions and `tests/skill-collision-repro.sh` select `project-skill`. `.mergify.yml` is explicitly `nonRuntime`. There are no blanket no-runtime exemptions for `.github/**`, `tests/**`, or `scripts/**`: unregistered instruction/enforcement paths fail closed until their ownership is reviewed and mapped.
+Consumed `AGENTS.md`/`CLAUDE.md` instructions, `tests/skill-collision-repro.sh`, `.github/workflows/ci.yml` and the root `package.json`, whose scripts CI runs, select `project-skill`. `.mergify.yml` is explicitly `nonRuntime`. There are no blanket no-runtime exemptions for `.github/**`, `tests/**`, or `scripts/**`: unregistered instruction/enforcement paths fail closed until their ownership is reviewed and mapped.
 
-Explicit non-runtime repository changes are `no runtime change`. Changes to this verifier are runtime changes and must run from the candidate head. `--self-test` adds `project-skill` in both harnesses, deduplicated with a named one, and is mandatory for this skill's delivery PR. Plugin-runtime proof and local CLI proof remain separate.
+Explicit non-runtime repository changes are `no runtime change`. Plugin-runtime proof and local CLI proof remain separate.