2.0.0-rc.10: Lauren's 4382e68, a skill that formally verifies what tests rarely reach

[chhoumann]

t3-pstack moves to Lauren Tan's pstack at cursor/plugins 4382e68 for all three components. Only pstack changed upstream, in two commits, and its version stays 0.15.25:

• pstack #709: a new skill, create-formal-verification-skill. It finds the code where a bug costs the most and tests reach the least, verifies one property of it with the tool the question calls for (a model checker such as TLA+, an SMT-backed verifier, or a proof assistant), and leaves a project-local skill that reruns the check on later changes. It must see each property fail on a broken variant of the code before it trusts a pass, and it reports a failing property as a finding instead of weakening it. poteto-help gains its row.
• pstack #708: ketchup says outright that it never cuts items to stay under a word count.

Upstream's README row and its copies under harness/pstack/claude-code/ sit outside every synced component.

This is Lauren's text, a new skill file of hers included, plus existing substitutions and mechanical version and count lines. No substitution, fork, hook, or code changed.

Commits

1. Sync. bun tools/sync.mjs moves each component's pin from 16541c6 to 4382e68, adds create-formal-verification-skill/SKILL.md, and updates ketchup/SKILL.md and poteto-help/SKILL.md cleanly. 25 existing rules in tools/substitutions.json match in the two updated files: three in ketchup and 22 in poteto-help. None matches the new skill, which is byte-identical to upstream's. The 15 declared forks were left alone. cursor-team-kit and thermos synced with no file changes.
2. Release. VERSION and the manifests move to 2.0.0-rc.10. CHANGES gets the entry with its behavior-delta table. NOTICE, NOTICE-skills, and the README point at 4382e68, the README's pinned installer command names the new tag, and its skill count moves from 62 to 63, which tests/readme-facts.test.mjs pins to the tree.

On T3

The new skill names no Cursor tool, .cursor/ path, model, /visualize, or subagent. It says "write a project-local skill" without a path, so the agent picks .claude/skills/ or .agents/skills/ for its harness and no rule is needed. Upstream's /create-verification-skill does name a .cursor/skills/ path, which is why that skill carries substitutions.

The skill keeps Lauren's disable-model-invocation: true, as do 54 others; deriveT3 drops the flag from poteto-mode alone. On Claude Code the user types /t3-pstack:create-formal-verification-skill. On Codex it is $t3-pstack:create-formal-verification-skill, and Codex ignores the flag. poteto-mode does not route to it, upstream or here. Nothing else in the repo lists skills by name: both manifests point at ./skills/, the generator and tests walk the tree, and the session-start routing names only poteto-mode.

Checks

• bun tools/sync.mjs <component> 4382e68 --dry-run for pstack, cursor-team-kit, and thermos, before and after the sync: exit 0, no undeclared fork, no denylist hit, no unmatched substitution. At the new pin, pstack reads 119 unchanged files, rc.9's 118 plus the new skill, and the same 15 declared forks with 547 changed lines as before. No forked file differs from origin/main.
• bun tools/generate.mjs --check: 17 generated files current, and the hooks freeze check passes.
• GIT_CONFIG_GLOBAL=/dev/null bun test tests/ --timeout 30000: 550 pass, 46 skip, 0 fail.
• Scripts: bun run typecheck, bun test orch watch-pr check-plan.test.ts (119 pass), and the Prettier check all pass. markdownlint is clean on every changed file.
• t3-sheet.mjs against this machine's sheet and catalog: every role line parses and dispatches.
• Install: T3_PSTACK_E2E=1 bun test tests/install-e2e.test.mjs with the real claude 2.1.302 and codex 0.163.0 CLIs passes 12 of 12. A separate tools/install.mjs install --source <this branch> into a throwaway HOME installs 2.0.0-rc.10 on both. claude plugin details t3-pstack@t3-pstack lists 63 skills, create-formal-verification-skill among them. Codex's app-server skills/list returns 63 t3-pstack: skills, t3-pstack:create-formal-verification-skill enabled. Both installed copies keep disable-model-invocation: true.

---

Note

Low Risk
Upstream skill and wording sync with version/metadata bumps only; no runtime hooks, substitutions, or orchestration code changes.

Overview
Release 2.0.0-rc.10 bumps the plugin and installer metadata and re-pins upstream cursor/plugins to 4382e68 (pstack, cursor-team-kit, thermos).

The substantive port change is a new create-formal-verification-skill: it targets high-impact, hard-to-test code, verifies one property with an appropriate formal tool (model checker, SMT verifier, proof assistant, etc.), requires seeing properties fail on broken variants before trusting passes, and leaves a project-local rerun skill. poteto-help documents it; skill count goes 62 → 63.

ketchup is tightened so replies must not cut or shrink action items to satisfy word limits.

No hook, substitution, or fork changes—mostly sync plus version/changelog/NOTICE updates.

^{Reviewed by Cursor Bugbot for commit 26c8eb7. Bugbot is set up for automated code reviews on this repo. Configure here.}