pstack: add maintain-formal-verification-skill

[poteto]

What

Adds /maintain-formal-verification-skill, the companion to /create-formal-verification-skill. The create skill writes a project-local formal verify skill one time. The maintain skill keeps that verify skill in line with the code after changes that did not recheck it, such as merges, refactors, and edits made without the verify skill.

One pass:

1. Finds the project's formal verify skills by what they do, not by name. The generated skill has no fixed name, and /setup-pstack (from pstack: offer formal verification in setup, sync help and guide #715) finds it in the same way.
2. Runs each check as it is.
3. Reads every change to the covered code since the recorded sync commit, including code that moved and new code that touches the guarded state.
4. Updates the model, harness, or properties from the code, not from the result. A property changes only when evidence shows that the promise changed on purpose.
5. Reruns each check. On a pass, it breaks the new code to show that the check can still fail. On a failure, it replays the counterexample against the code to decide whether the failure is drift in the verification or a bug in the code.
6. Updates the verify skill's coverage record and moves its sync commit forward. It does not move the sync commit for a blocked check, and it says so in the report.

Each check ends as in sync, updated, bug, or blocked. The skill does not edit product code, and it does not weaken a property to make a check pass.

Change to create-formal-verification-skill

The generated skill now records which files and functions each check covers, and the commit where the verification last matched them. The maintain skill reads that record to know what to diff. The naming does not change.

Docs

• README: adds a row for the new skill.
• poteto-help: adds a routing-table row, and adds the skill to the formal verification state check and recipe.
• Guide page 6: adds one paragraph at the end of the formal verification section.
• Guide page 9: names the skill in the sentence on special cases, and points the "covers both kinds" link at the formal verification section on page 6 instead of the app-verification section.

node scripts/check-pstack-docs.mjs reports 0 problems, node scripts/validate-plugins.mjs passes, and node scripts/generate-pstack-harness-trees.mjs --check reports the harness tree up to date.

Eval

The eval was preregistered. It had 54 sealed offline runs: 3 cases × 3 arms × 3 models (Claude Opus 5.5, GPT-5.6 Sol, Grok 4.7, all at xhigh) × 2 replicates. A blind Gemini 4 Argon High judge scored each run.

• Cases. Real upstream histories with a formal suite that drifted:
  • x/sync/semaphore with TLA+, where the stale model still passes.
  • The same history with a missing wakeup added.
  • cachetools with a Python model check, where the stale check fails on an intended change.
• Arms. The verify skill without a coverage record (B0). The verify skill with the record that this PR adds to the create skill (B1). B1 plus this skill (M).

Results:

• Correctness: no real gain. Correct runs of 18: B0 16, B1 14, M 16. M is 2 runs above B1, which meets the preregistered ship rule. But most failures were runs that found a real, older bug in the semaphore code that the case key did not include, or runs that added checker trace files to .gitignore. With those two corrections, all three arms score 18 of 18. On these cases, the models already keep the verification in sync without the skill.
• The skill makes runs prove that the updated check can still fail. In runs where the final check passed, every M report showed a deliberate break and the check that caught it (11 of 11). B0 did this in 5 of 10 runs, and B1 in 4 of 10. M reports also separated drift from bugs in 18 of 18 runs.
• The record makes runs update the sync commit. B1 and M updated the sync commit in 18 of 18 runs. B0 did so in 4 of 18.
• No harm found. No M run changed product source, weakened the NoStrandedWaiter violation, or called the intended cachetools change a bug. One M run edited .gitignore, and one made its breaks in the product file and then restored the file.

Follow-up: blocked check. Bugbot found that step 6 moved the sync commit even for a blocked check, which the runs above never produced. The fix adds one sentence to step 6 and corrects a step number in step 2. A second preregistered test (one case where one check cannot run, old text against new text, the same three models, 3 runs each, 18 sealed runs, blind judge) gave: new text 9/9 runs kept the blocked check's sync commit and reported it as blocked, and old text 0/9. With the old text, 7 runs moved the shared sync commit to HEAD.

This PR does not bump the pstack version.

  

---

Note

Low Risk
Documentation and agent skill definitions only; no runtime product code, auth, or data paths change.

^{Reviewed by Cursor Bugbot for commit 011ef53. 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 3 potential issues.

^{❌ 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 4078be5. Configure here.}