feat(pstack): add /create-formal-verification-skill

[poteto]

Why

A test checks the cases that someone thought to write. Races, retries, state machines, parsers, and unsafe code often break on a case that nobody wrote. pstack already has /create-verification-skill, which proves app behavior with scripted runs. It has no skill that checks a property across every case in a stated scope.

What the skill does for you

Call /create-formal-verification-skill in your repo. If you name an area or a bug, the skill starts there. The skill then does these steps in order:

1. It chooses the strongest target in the repo, not the easiest one to verify. A good target is a promise the code makes, where a break harms users and tests rarely reach the case that breaks it.
2. It picks a verification tool for that question and tells you why.
3. It verifies one property and shows that property fail on a broken variant of the code, such as a removed check or a reordered step.
4. It writes a project-local skill. From that skill alone, the next agent can tell whether a change touches the verified code, rerun the check with one command, and tell a real bug from a modeling error.
5. It follows the new skill once on a scratch change that breaks the property, confirms that the check catches the break, and then drops the change.

At handoff, the skill tells you what it verified, which tool it used and why, the bounds, what the check found, how to rerun it, and what it does not cover. If the current code breaks the property, you get the counterexample as a short sequence of steps in the code's words. The skill does not weaken the property or the model to get a pass, and it does not change product code unless you ask.

Why the skill stays goal-level

The skill says what a good result looks like. It leaves the choice of tool and model design to the agent, because the right choice depends on the question and the repo. A question about events in a bad order usually suits a model checker over a small model of the design. A question about the code for every input, such as memory safety or overflow, usually suits a verifier that runs on the code. A property that must hold at every size can need a proof. The tool must also be one that the repo's developers can install and run.

One prescribed tool or model shape fits some repos and gives the wrong check in the others. So the skill names the tool families, suggests TLA+ as a common start for concurrent and distributed designs, and asks the agent to explain its choice. What the skill fixes is the bar that every result must meet, whatever the tool:

• Each part of the model or proof points to code that a reviewer can open.
• The agent must see each property fail on a broken variant of the code before it trusts a pass.
• The handoff states the bounds, the assumptions, and what the check leaves out.
• The check reruns with one command and a reproducible tool version.
• When verified code changes, something tells the next agent to look at the verification again.

What changed

• The new skill in pstack/skills/create-formal-verification-skill/SKILL.md. It sets disable-model-invocation: true, so it runs only when you call it by name.
• One row for the skill in pstack/README.md and one line in pstack/skills/poteto-help/SKILL.md.
• The regenerated copies of these three files under harness/pstack/claude-code/.

Blast radius

This PR changes only prompt text and docs. No script, runtime code, or existing skill changes.

Verification

• node scripts/validate-plugins.mjs, node scripts/check-pstack-docs.mjs, and node scripts/generate-pstack-harness-trees.mjs --check pass on the head commit and on a merge with current main.
• The skill file under pstack/ and its copy under harness/pstack/claude-code/ are identical.
• The docs check reports 0 problems. It notes that pstack/docs/guide does not name the new command yet. Three existing commands get the same note.
• An eval tested this exact SKILL.md on six open-source repos that it never saw: timgit/pg-boss, vercel/swr, brettwooldridge/HikariCP, kubernetes/client-go, DaveGamble/cJSON, and bluss/arrayvec. It compared the skill with an earlier draft that prescribed TLA+ and came with file templates and a worked example. Blinded judges scored each attempt out of 30 on six criteria, such as target choice, tool fit, and checks.
  • On the four repos with a concurrency or distribution shape, the skill's mean was 29.0 and the draft's was 26.5. On cJSON and arrayvec, the means were 26.0 and 22.0. Two hand corrections to judge scores move the skill's means to 28.75 and 26.25. On every repo, the skill scored the same as the draft or higher when both used the same model.
  • On cJSON and arrayvec, where TLA+ fits poorly, the skill chose a verifier that runs on the code in 4 of 4 runs: CBMC on cJSON and Kani on arrayvec. The draft chose TLA+ on both repos.
  • The skill was weaker on one criterion. On cJSON and arrayvec, its checks score was 3.75 and the draft's was 4.5. One run did not confirm that its CBMC loop bounds were large enough, and another had no single run command.
  • The sample is small: n = 1 run per repo and version, and n = 2 for the skill on cJSON and arrayvec. Treat a one-run gap as a lead, not a finding.

  

---

Note

Low Risk
Docs and prompt text only; no runtime, scripts, or changes to existing skills.

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

[cursor]

Cursor Bugbot has reviewed your changes using high effort and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, have a team admin enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit feaf2fd. Configure here.}