diff --git a/harness/pstack/claude-code/README.md b/harness/pstack/claude-code/README.md index 723a594e2..f4ee63dad 100644 --- a/harness/pstack/claude-code/README.md +++ b/harness/pstack/claude-code/README.md @@ -150,6 +150,7 @@ to keep [`/poteto-mode`](./skills/poteto-mode/SKILL.md) on across turns, pick it | [`/create-verification-skill`](./skills/create-verification-skill/SKILL.md) | your project has no scripted way to prove app behavior. generates a project-local verify skill with a feature map, for any language or platform. | | [`/maintain-verification-skill`](./skills/maintain-verification-skill/SKILL.md) | your verify skill's feature map has drifted from the app. source wave + one live pass, at most one PR of proven corrections. | | [`/create-formal-verification-skill`](./skills/create-formal-verification-skill/SKILL.md) | tests can't reach the case that breaks a race, retry, state machine, parser, or unsafe code. verifies one property with the tool that fits and generates a project-local skill to recheck it on every change. | +| [`/maintain-formal-verification-skill`](./skills/maintain-formal-verification-skill/SKILL.md) | code your formal verification covers has changed since it was last checked. updates the model, harness, or properties to match the code, reruns, and says whether each failure is drift in the verification or a bug in the code. | | [`/unslop`](./skills/unslop/SKILL.md) | you're cleaning up writing. removes AI tells. | | [`/bro`](./skills/bro/SKILL.md) | you want the last message restated in plain human language, no jargon. | | [`/technical-writing`](./skills/technical-writing/SKILL.md) | layered doc standard (Diátaxis + Google developer style + STE + Global English) for docs, RFCs, readmes, PR descriptions, commit messages. | diff --git a/harness/pstack/claude-code/docs/guide/06-verify-and-ship.md b/harness/pstack/claude-code/docs/guide/06-verify-and-ship.md index 62a0a059b..711b5a92a 100644 --- a/harness/pstack/claude-code/docs/guide/06-verify-and-ship.md +++ b/harness/pstack/claude-code/docs/guide/06-verify-and-ship.md @@ -113,6 +113,8 @@ It verifies one property and shows that property failing on a broken variant of It writes a project-local skill that tells the next agent whether a change touches the verified code, how to run the check with one command, and how to tell a real bug from a modeling error. Before handing it over, the generator follows that skill once on a scratch change that breaks the property, and the check must catch it. The handoff says what was verified, with which tool and bounds, what the check found, and what it doesn't cover. A pass covers the model or the bound, not the whole system. +The skill also records which code each check covers and the commit where the check last matched it. Merges and refactors that skip the skill can leave the check passing on a description of code that's gone. After them, run [`/maintain-formal-verification-skill`](../../skills/maintain-formal-verification-skill/SKILL.md). It updates the verification from the code, reruns it, shows that each updated check can still fail, and tells you whether each failure is drift in the verification or a bug in the code. + ## Open the PR ```text diff --git a/harness/pstack/claude-code/docs/guide/09-make-it-yours.md b/harness/pstack/claude-code/docs/guide/09-make-it-yours.md index 457341aa4..8d1c4b4f9 100644 --- a/harness/pstack/claude-code/docs/guide/09-make-it-yours.md +++ b/harness/pstack/claude-code/docs/guide/09-make-it-yours.md @@ -59,7 +59,7 @@ When you already know the workflow you want to capture: Writing a skill matches the [Authoring or modifying a skill playbook](../../skills/poteto-mode/playbooks/authoring-a-skill.md), which routes through Cursor's built-in `create-skill`, validates the frontmatter and links, and ships the result through the Opening a PR playbook. Agent-facing prose has a higher bar than human prose, because an unhelpful sentence becomes an instruction some future agent follows. Let the playbook hold that bar rather than writing a `SKILL.md` freehand. -Two special cases have their own generators. A skill that must drive your app and prove behavior is a verification skill, so use [`/create-verification-skill`](../../skills/create-verification-skill/SKILL.md) and [`/maintain-verification-skill`](../../skills/maintain-verification-skill/SKILL.md) instead. A skill that checks a property of your code with a model checker, a proof, or another verifier is a formal verification skill, so use [`/create-formal-verification-skill`](../../skills/create-formal-verification-skill/SKILL.md). [Verify and ship](./06-verify-and-ship.md#create-a-project-verification-skill) covers both kinds. +Two special cases have their own generators. A skill that must drive your app and prove behavior is a verification skill, so use [`/create-verification-skill`](../../skills/create-verification-skill/SKILL.md) and [`/maintain-verification-skill`](../../skills/maintain-verification-skill/SKILL.md) instead. A skill that checks a property of your code with a model checker, a proof, or another verifier is a formal verification skill, so use [`/create-formal-verification-skill`](../../skills/create-formal-verification-skill/SKILL.md) and [`/maintain-formal-verification-skill`](../../skills/maintain-formal-verification-skill/SKILL.md). [Verify and ship](./06-verify-and-ship.md#prove-a-property-with-a-formal-verification-skill) covers both kinds. ## Write docs to a standard with `/technical-writing` diff --git a/harness/pstack/claude-code/skills/create-formal-verification-skill/SKILL.md b/harness/pstack/claude-code/skills/create-formal-verification-skill/SKILL.md index 893f6042c..fe72da6d8 100644 --- a/harness/pstack/claude-code/skills/create-formal-verification-skill/SKILL.md +++ b/harness/pstack/claude-code/skills/create-formal-verification-skill/SKILL.md @@ -6,6 +6,8 @@ disable-model-invocation: true # Create a formal verification skill +In Claude Code, read [the Claude Code adapter](../../docs/harness/claude-code.md) once per session before you follow this skill. It maps the Cursor names in pstack skills to Claude Code. + A test checks the cases that someone thought to write. Formal verification checks every case in a stated scope: every order of steps in a model, every input up to a bound, or every input. This skill finds the part of the repo where that matters most, verifies one property of it, and leaves a project-local skill that lets the next agent check a change against that property. Write that skill for an agent who reads it cold, mid-change, and has never seen your work. The user must be able to trust the result and act on it without learning the verification language. ## Choose the target from the code @@ -26,11 +28,11 @@ Pick the tool that answers the question at the lowest cost: a model checker, a p - **Honest about scope.** Say what is verified, under which bounds and assumptions, and what is left out. A pass covers the model or the bound, not the whole system. - **Readable without the tool.** State the property and the harm in one plain sentence each. Tell a counterexample as a short sequence of steps in the code's words. - **Cheap to rerun.** One command, a reproducible tool version, and a run short enough that the next agent will use it on every relevant change. -- **Kept in step with the code.** When verified code changes, something tells the next agent that the verification needs another look. +- **Kept in step with the code.** Record which files and functions each check covers, and the commit at which you last confirmed that the verification describes them. When the covered code changes after that commit, the next agent can see that the verification needs another look. ## Generate the verify skill -Write a project-local skill with frontmatter that names the area and says when to use it. Without frontmatter, the skill never registers. From the skill alone, the next agent must be able to tell whether a change touches the verified code, run the check, tell a real bug from a modeling error, and update the verification when a change is intended. Use this repo's real commands, paths, and nouns, and leave no placeholders. +Write a project-local skill with frontmatter that names the area and says when to use it. Without frontmatter, the skill never registers. From the skill alone, the next agent must be able to tell whether a change touches the verified code, run the check, tell a real bug from a modeling error, and update the verification when a change is intended. Put the coverage record and the sync commit in the skill, and tell the next agent to move the sync commit forward only after it confirms that the verification describes the code at the new commit. Use this repo's real commands, paths, and nouns, and leave no placeholders. ## Prove it before you hand off @@ -38,4 +40,4 @@ Follow the generated skill once, as the next agent would, on a scratch change th ## Hand off -Tell the user what you verified, which tool you used and why, the bounds, what the check found in plain words, how to run it, and what it does not cover. Suggest a second target only if you found a close one. +Tell the user what you verified, which tool you used and why, the bounds, what the check found in plain words, how to run it, and what it does not cover. Suggest a second target only if you found a close one. Point the user at `/maintain-formal-verification-skill` for bringing the verification back in line after changes that did not recheck it. diff --git a/harness/pstack/claude-code/skills/maintain-formal-verification-skill/SKILL.md b/harness/pstack/claude-code/skills/maintain-formal-verification-skill/SKILL.md new file mode 100644 index 000000000..d56ef9ce9 --- /dev/null +++ b/harness/pstack/claude-code/skills/maintain-formal-verification-skill/SKILL.md @@ -0,0 +1,60 @@ +--- +name: maintain-formal-verification-skill +description: "Bring a project's formal verification back in line with the code after the code changes: find the commits that touched verified code, update the model, harness, or properties to describe the code as it is now, rerun, and say whether each failure is drift in the verification or a bug in the code. Use for /maintain-formal-verification-skill, \"is the model still true to the code\", or after merges and refactors that touched verified code without rechecking it." +disable-model-invocation: true +--- + +# Maintain a formal verification skill + +In Claude Code, read [the Claude Code adapter](../../docs/harness/claude-code.md) once per session before you follow this skill. It maps the Cursor names in pstack skills to Claude Code. + +A formal check proves a property of what it describes. When the code changes and the verification does not, the check can keep passing while it describes code that no longer exists. That pass is the dangerous case, because it looks like a proof. This skill is the upkeep loop for a verify skill that `/create-formal-verification-skill` generated, or for any project-local skill that runs a model checker, prover, or code-level verifier against named code. The project-local skill handles a change that an agent makes while it uses that skill. This skill handles the changes that skipped it: merges, edits made without the skill, and drift that builds up across many commits. + +## Outcomes + +Give each check one outcome, and say which: + +- **in sync**: no change since the last sync alters what the check describes, and the check passes. +- **updated**: the code changed, the verification now describes the new code, and the check passes. +- **bug**: the verification describes the current code, and the code breaks the property. This is a finding about the code. It is not drift. +- **blocked**: the check could not be brought back in line or could not run. Say exactly why. + +A check can be both updated and bug: the update makes the verification describe the code again, and then the property fails on it. + +## Edit scope + +Edit only the verification: models, harnesses, property files, and the verify skill itself. Never edit product code during a run, unless the user asks you to. When a property fails on the current code, do not weaken the property or the model to make it pass. Report the failure. + +## Pass + +1. **Find the checks.** A verify skill has no fixed name, so find it by what it does: a project skill that runs a model checker, a prover, or another verifier against named code. Read each one you find, or the one the user named. For each check, collect the property, the code it covers, the bounds and assumptions, the command that runs it, and the commit where it was last confirmed to describe the code. If no verify skill exists, stop and point at `/create-formal-verification-skill`. If the skill does not record a sync commit, use the last commit that changed the verification files, and say that you did. + +2. **Run it as it is.** Run each check once before you change anything, and record the result. A pass here does not tell you that the code is correct. It tells you that the old description still holds. A failure here can be drift or a bug. Do not decide which until step 5. + +3. **Read every change to covered code.** Diff the covered files from the sync commit to the current commit, and read each commit message. Also look for code that moved: a covered function that is renamed, split, or moved to another file is still covered code. Also look for new code that touches the state that a check guards, such as a new function that writes the same fields. For each change, decide which of these it is: + - **No effect.** The change does not alter anything the verification describes, such as formatting, comments, or code paths that the verification does not cover. Check this against the model or harness, not against the commit message. + - **The verification no longer describes the code.** A step that was one indivisible action is now two, a branch was added or removed, a check moved, a new path reaches the guarded state, or a value now has a different range. The model or harness must change. + - **The promise changed on purpose.** The change alters what the code promises, and evidence in the change says that this is intended: the doc comment, the tests, the changelog, or the commit message. The property must change, and you must cite that evidence. + - **The promise may be broken.** The code changed, and no evidence says that the promise changed. Treat a failure that follows as a bug candidate. + +4. **Update from the code, not from the result.** Change the model or harness so that each changed part again points to code that a reviewer can open, and keep one indivisible step in the code as one step in the verification. Write the update from the code before you rerun, and do not shape it by what makes the check pass. Change a property only for a promise that changed on purpose. Write down the old wording, the new wording, and the evidence. Keep the bounds unless the change makes them wrong. If you must reduce a bound, say so in the report. + +5. **Rerun and judge each result.** + - **Pass:** the check can now pass on a description that has lost the ability to fail. Break the new code the way the property guards against, such as removing a new check or reordering a new step, and confirm that the check catches it. Then drop the break. + - **Fail:** replay the counterexample against the real code, step by step. If a step cannot happen in the code, the verification is wrong. Fix the verification, and say what was wrong. If every step can happen, it is a bug. Name the commit that introduced it, tell the counterexample as a sequence of steps in the code's own words, and state the harm in one sentence. If a cheap test or reproduction against the real code shows the bug, add it to the report as evidence. Do not commit it to the product code. + +6. **Update the verify skill.** Update the code that each check covers, the commands, the bounds, the assumptions, and the sync commit. Set the sync commit to the commit that you checked. Do not move the sync commit for a blocked check, and say so in the report. Then follow the verify skill once as the next agent would, so that you know its steps still run. + +## Report + +Tell the user, for each check: + +- the outcome, and the commits that you read; +- what changed in the verification and why, with a short reason for each change: the code changed shape, or the promise changed on purpose (with the evidence); +- the rerun result, and the break that you used to show the updated check can still fail; +- each bug, in plain words: the counterexample as steps in the code's words, the harm, and the commit that introduced it; +- what the verification still does not cover, including new code that it should cover and does not. + +Say outright which failures were drift in the verification and which were bugs in the code. For a check that passed before you updated it and fails after, say that the old pass was on a stale description. + +Put the verification updates in a change of their own, separate from any product fix. diff --git a/harness/pstack/claude-code/skills/poteto-help/SKILL.md b/harness/pstack/claude-code/skills/poteto-help/SKILL.md index fc89d3b53..f9f3587f8 100644 --- a/harness/pstack/claude-code/skills/poteto-help/SKILL.md +++ b/harness/pstack/claude-code/skills/poteto-help/SKILL.md @@ -28,7 +28,7 @@ Check the state that changes the answer, and mention it only when it does: - No `~/.cursor/rules/pstack-models.mdc` means `/setup-pstack` hasn't run for this user, so every role uses its default model. - No `verify-*` skill or other app harness in the project means agents have no scripted way to drive the app. Mention `/create-verification-skill` when the question is about proving a change works. -- No formal verification skill in the project means no property is checked past what tests reach. Mention `/create-formal-verification-skill` when the question is about a race, an invariant, or another case tests rarely hit. +- No formal verification skill in the project means no property is checked past what tests reach. Mention `/create-formal-verification-skill` when the question is about a race, an invariant, or another case tests rarely hit. When one exists and the code it covers changed after the commit it records as last in sync, mention `/maintain-formal-verification-skill` if the question touches that code. When the model rule is missing and it matters, ask whether the user wants to pick a model for each role and a reasoning budget now. It matters when the user is new, the question is about setup or cost, or the answer depends on which models run. Ask at most once per chat. If the need is also unclear, ask both questions together. Offer two choices: @@ -89,6 +89,7 @@ The default answer is `/poteto-mode`, which runs most of the others when its ste | Give agents a scripted way to drive the app and prove behavior | [`/create-verification-skill`](../create-verification-skill/SKILL.md) | | Bring a verification skill and its feature map back in line with the app | [`/maintain-verification-skill`](../maintain-verification-skill/SKILL.md) | | Formally verify a race, invariant, or other property that tests rarely reach | [`/create-formal-verification-skill`](../create-formal-verification-skill/SKILL.md) | +| Bring a formal verification back in line after the code it covers changed, and learn whether a failure is drift or a bug | [`/maintain-formal-verification-skill`](../maintain-formal-verification-skill/SKILL.md) | | Vet a performance number before reporting or acting on it | [`/benchmark-checklist`](../benchmark-checklist/SKILL.md) | | Run a large or cross-cutting change, or one to review after stepping away | [`/figure-it-out`](../figure-it-out/SKILL.md) | | Keep a decision log during a run, and review it afterward | [`/show-me-your-work`](../show-me-your-work/SKILL.md) | diff --git a/harness/pstack/claude-code/skills/poteto-help/references/recipes.md b/harness/pstack/claude-code/skills/poteto-help/references/recipes.md index 2d785761d..c4f60466c 100644 --- a/harness/pstack/claude-code/skills/poteto-help/references/recipes.md +++ b/harness/pstack/claude-code/skills/poteto-help/references/recipes.md @@ -34,7 +34,7 @@ Swap in the real paths, skills, and done checks. Informal wording works. ## Review and ship - `/interrogate the whole branch, but skeptically. don't change anything yet. no nitpicks unless it's a real bug or regression.` Read the dismissals too. -- `/create-formal-verification-skill prove holds in , even when interleave or retry.` +- `/create-formal-verification-skill prove holds in , even when interleave or retry.` After merges or refactors in that code: `/maintain-formal-verification-skill`. - `/swarm check every package under against its check script. one worker per package. one report.` - `/poteto-mode open the pr. small ordered commits, evidence in the description.` - `/poteto-mode babysit this pr. get it green.` For status only: `/poteto-mode check on pr . anything outstanding?` diff --git a/pstack/README.md b/pstack/README.md index 40026a543..8d350cc17 100644 --- a/pstack/README.md +++ b/pstack/README.md @@ -150,6 +150,7 @@ to keep [`/poteto-mode`](./skills/poteto-mode/SKILL.md) on across turns, pick it | [`/create-verification-skill`](./skills/create-verification-skill/SKILL.md) | your project has no scripted way to prove app behavior. generates a project-local verify skill with a feature map, for any language or platform. | | [`/maintain-verification-skill`](./skills/maintain-verification-skill/SKILL.md) | your verify skill's feature map has drifted from the app. source wave + one live pass, at most one PR of proven corrections. | | [`/create-formal-verification-skill`](./skills/create-formal-verification-skill/SKILL.md) | tests can't reach the case that breaks a race, retry, state machine, parser, or unsafe code. verifies one property with the tool that fits and generates a project-local skill to recheck it on every change. | +| [`/maintain-formal-verification-skill`](./skills/maintain-formal-verification-skill/SKILL.md) | code your formal verification covers has changed since it was last checked. updates the model, harness, or properties to match the code, reruns, and says whether each failure is drift in the verification or a bug in the code. | | [`/unslop`](./skills/unslop/SKILL.md) | you're cleaning up writing. removes AI tells. | | [`/bro`](./skills/bro/SKILL.md) | you want the last message restated in plain human language, no jargon. | | [`/technical-writing`](./skills/technical-writing/SKILL.md) | layered doc standard (Diátaxis + Google developer style + STE + Global English) for docs, RFCs, readmes, PR descriptions, commit messages. | diff --git a/pstack/docs/guide/06-verify-and-ship.md b/pstack/docs/guide/06-verify-and-ship.md index 62a0a059b..711b5a92a 100644 --- a/pstack/docs/guide/06-verify-and-ship.md +++ b/pstack/docs/guide/06-verify-and-ship.md @@ -113,6 +113,8 @@ It verifies one property and shows that property failing on a broken variant of It writes a project-local skill that tells the next agent whether a change touches the verified code, how to run the check with one command, and how to tell a real bug from a modeling error. Before handing it over, the generator follows that skill once on a scratch change that breaks the property, and the check must catch it. The handoff says what was verified, with which tool and bounds, what the check found, and what it doesn't cover. A pass covers the model or the bound, not the whole system. +The skill also records which code each check covers and the commit where the check last matched it. Merges and refactors that skip the skill can leave the check passing on a description of code that's gone. After them, run [`/maintain-formal-verification-skill`](../../skills/maintain-formal-verification-skill/SKILL.md). It updates the verification from the code, reruns it, shows that each updated check can still fail, and tells you whether each failure is drift in the verification or a bug in the code. + ## Open the PR ```text diff --git a/pstack/docs/guide/09-make-it-yours.md b/pstack/docs/guide/09-make-it-yours.md index 457341aa4..8d1c4b4f9 100644 --- a/pstack/docs/guide/09-make-it-yours.md +++ b/pstack/docs/guide/09-make-it-yours.md @@ -59,7 +59,7 @@ When you already know the workflow you want to capture: Writing a skill matches the [Authoring or modifying a skill playbook](../../skills/poteto-mode/playbooks/authoring-a-skill.md), which routes through Cursor's built-in `create-skill`, validates the frontmatter and links, and ships the result through the Opening a PR playbook. Agent-facing prose has a higher bar than human prose, because an unhelpful sentence becomes an instruction some future agent follows. Let the playbook hold that bar rather than writing a `SKILL.md` freehand. -Two special cases have their own generators. A skill that must drive your app and prove behavior is a verification skill, so use [`/create-verification-skill`](../../skills/create-verification-skill/SKILL.md) and [`/maintain-verification-skill`](../../skills/maintain-verification-skill/SKILL.md) instead. A skill that checks a property of your code with a model checker, a proof, or another verifier is a formal verification skill, so use [`/create-formal-verification-skill`](../../skills/create-formal-verification-skill/SKILL.md). [Verify and ship](./06-verify-and-ship.md#create-a-project-verification-skill) covers both kinds. +Two special cases have their own generators. A skill that must drive your app and prove behavior is a verification skill, so use [`/create-verification-skill`](../../skills/create-verification-skill/SKILL.md) and [`/maintain-verification-skill`](../../skills/maintain-verification-skill/SKILL.md) instead. A skill that checks a property of your code with a model checker, a proof, or another verifier is a formal verification skill, so use [`/create-formal-verification-skill`](../../skills/create-formal-verification-skill/SKILL.md) and [`/maintain-formal-verification-skill`](../../skills/maintain-formal-verification-skill/SKILL.md). [Verify and ship](./06-verify-and-ship.md#prove-a-property-with-a-formal-verification-skill) covers both kinds. ## Write docs to a standard with `/technical-writing` diff --git a/pstack/skills/create-formal-verification-skill/SKILL.md b/pstack/skills/create-formal-verification-skill/SKILL.md index 893f6042c..b97609fd2 100644 --- a/pstack/skills/create-formal-verification-skill/SKILL.md +++ b/pstack/skills/create-formal-verification-skill/SKILL.md @@ -26,11 +26,11 @@ Pick the tool that answers the question at the lowest cost: a model checker, a p - **Honest about scope.** Say what is verified, under which bounds and assumptions, and what is left out. A pass covers the model or the bound, not the whole system. - **Readable without the tool.** State the property and the harm in one plain sentence each. Tell a counterexample as a short sequence of steps in the code's words. - **Cheap to rerun.** One command, a reproducible tool version, and a run short enough that the next agent will use it on every relevant change. -- **Kept in step with the code.** When verified code changes, something tells the next agent that the verification needs another look. +- **Kept in step with the code.** Record which files and functions each check covers, and the commit at which you last confirmed that the verification describes them. When the covered code changes after that commit, the next agent can see that the verification needs another look. ## Generate the verify skill -Write a project-local skill with frontmatter that names the area and says when to use it. Without frontmatter, the skill never registers. From the skill alone, the next agent must be able to tell whether a change touches the verified code, run the check, tell a real bug from a modeling error, and update the verification when a change is intended. Use this repo's real commands, paths, and nouns, and leave no placeholders. +Write a project-local skill with frontmatter that names the area and says when to use it. Without frontmatter, the skill never registers. From the skill alone, the next agent must be able to tell whether a change touches the verified code, run the check, tell a real bug from a modeling error, and update the verification when a change is intended. Put the coverage record and the sync commit in the skill, and tell the next agent to move the sync commit forward only after it confirms that the verification describes the code at the new commit. Use this repo's real commands, paths, and nouns, and leave no placeholders. ## Prove it before you hand off @@ -38,4 +38,4 @@ Follow the generated skill once, as the next agent would, on a scratch change th ## Hand off -Tell the user what you verified, which tool you used and why, the bounds, what the check found in plain words, how to run it, and what it does not cover. Suggest a second target only if you found a close one. +Tell the user what you verified, which tool you used and why, the bounds, what the check found in plain words, how to run it, and what it does not cover. Suggest a second target only if you found a close one. Point the user at `/maintain-formal-verification-skill` for bringing the verification back in line after changes that did not recheck it. diff --git a/pstack/skills/maintain-formal-verification-skill/SKILL.md b/pstack/skills/maintain-formal-verification-skill/SKILL.md new file mode 100644 index 000000000..5d2f7f222 --- /dev/null +++ b/pstack/skills/maintain-formal-verification-skill/SKILL.md @@ -0,0 +1,58 @@ +--- +name: maintain-formal-verification-skill +description: "Bring a project's formal verification back in line with the code after the code changes: find the commits that touched verified code, update the model, harness, or properties to describe the code as it is now, rerun, and say whether each failure is drift in the verification or a bug in the code. Use for /maintain-formal-verification-skill, \"is the model still true to the code\", or after merges and refactors that touched verified code without rechecking it." +disable-model-invocation: true +--- + +# Maintain a formal verification skill + +A formal check proves a property of what it describes. When the code changes and the verification does not, the check can keep passing while it describes code that no longer exists. That pass is the dangerous case, because it looks like a proof. This skill is the upkeep loop for a verify skill that `/create-formal-verification-skill` generated, or for any project-local skill that runs a model checker, prover, or code-level verifier against named code. The project-local skill handles a change that an agent makes while it uses that skill. This skill handles the changes that skipped it: merges, edits made without the skill, and drift that builds up across many commits. + +## Outcomes + +Give each check one outcome, and say which: + +- **in sync**: no change since the last sync alters what the check describes, and the check passes. +- **updated**: the code changed, the verification now describes the new code, and the check passes. +- **bug**: the verification describes the current code, and the code breaks the property. This is a finding about the code. It is not drift. +- **blocked**: the check could not be brought back in line or could not run. Say exactly why. + +A check can be both updated and bug: the update makes the verification describe the code again, and then the property fails on it. + +## Edit scope + +Edit only the verification: models, harnesses, property files, and the verify skill itself. Never edit product code during a run, unless the user asks you to. When a property fails on the current code, do not weaken the property or the model to make it pass. Report the failure. + +## Pass + +1. **Find the checks.** A verify skill has no fixed name, so find it by what it does: a project skill that runs a model checker, a prover, or another verifier against named code. Read each one you find, or the one the user named. For each check, collect the property, the code it covers, the bounds and assumptions, the command that runs it, and the commit where it was last confirmed to describe the code. If no verify skill exists, stop and point at `/create-formal-verification-skill`. If the skill does not record a sync commit, use the last commit that changed the verification files, and say that you did. + +2. **Run it as it is.** Run each check once before you change anything, and record the result. A pass here does not tell you that the code is correct. It tells you that the old description still holds. A failure here can be drift or a bug. Do not decide which until step 5. + +3. **Read every change to covered code.** Diff the covered files from the sync commit to the current commit, and read each commit message. Also look for code that moved: a covered function that is renamed, split, or moved to another file is still covered code. Also look for new code that touches the state that a check guards, such as a new function that writes the same fields. For each change, decide which of these it is: + - **No effect.** The change does not alter anything the verification describes, such as formatting, comments, or code paths that the verification does not cover. Check this against the model or harness, not against the commit message. + - **The verification no longer describes the code.** A step that was one indivisible action is now two, a branch was added or removed, a check moved, a new path reaches the guarded state, or a value now has a different range. The model or harness must change. + - **The promise changed on purpose.** The change alters what the code promises, and evidence in the change says that this is intended: the doc comment, the tests, the changelog, or the commit message. The property must change, and you must cite that evidence. + - **The promise may be broken.** The code changed, and no evidence says that the promise changed. Treat a failure that follows as a bug candidate. + +4. **Update from the code, not from the result.** Change the model or harness so that each changed part again points to code that a reviewer can open, and keep one indivisible step in the code as one step in the verification. Write the update from the code before you rerun, and do not shape it by what makes the check pass. Change a property only for a promise that changed on purpose. Write down the old wording, the new wording, and the evidence. Keep the bounds unless the change makes them wrong. If you must reduce a bound, say so in the report. + +5. **Rerun and judge each result.** + - **Pass:** the check can now pass on a description that has lost the ability to fail. Break the new code the way the property guards against, such as removing a new check or reordering a new step, and confirm that the check catches it. Then drop the break. + - **Fail:** replay the counterexample against the real code, step by step. If a step cannot happen in the code, the verification is wrong. Fix the verification, and say what was wrong. If every step can happen, it is a bug. Name the commit that introduced it, tell the counterexample as a sequence of steps in the code's own words, and state the harm in one sentence. If a cheap test or reproduction against the real code shows the bug, add it to the report as evidence. Do not commit it to the product code. + +6. **Update the verify skill.** Update the code that each check covers, the commands, the bounds, the assumptions, and the sync commit. Set the sync commit to the commit that you checked. Do not move the sync commit for a blocked check, and say so in the report. Then follow the verify skill once as the next agent would, so that you know its steps still run. + +## Report + +Tell the user, for each check: + +- the outcome, and the commits that you read; +- what changed in the verification and why, with a short reason for each change: the code changed shape, or the promise changed on purpose (with the evidence); +- the rerun result, and the break that you used to show the updated check can still fail; +- each bug, in plain words: the counterexample as steps in the code's words, the harm, and the commit that introduced it; +- what the verification still does not cover, including new code that it should cover and does not. + +Say outright which failures were drift in the verification and which were bugs in the code. For a check that passed before you updated it and fails after, say that the old pass was on a stale description. + +Put the verification updates in a change of their own, separate from any product fix. diff --git a/pstack/skills/poteto-help/SKILL.md b/pstack/skills/poteto-help/SKILL.md index 7e834744b..5ce3a74d8 100644 --- a/pstack/skills/poteto-help/SKILL.md +++ b/pstack/skills/poteto-help/SKILL.md @@ -26,7 +26,7 @@ Check the state that changes the answer, and mention it only when it does: - No `~/.cursor/rules/pstack-models.mdc` means `/setup-pstack` hasn't run for this user, so every role uses its default model. - No `verify-*` skill or other app harness in the project means agents have no scripted way to drive the app. Mention `/create-verification-skill` when the question is about proving a change works. -- No formal verification skill in the project means no property is checked past what tests reach. Mention `/create-formal-verification-skill` when the question is about a race, an invariant, or another case tests rarely hit. +- No formal verification skill in the project means no property is checked past what tests reach. Mention `/create-formal-verification-skill` when the question is about a race, an invariant, or another case tests rarely hit. When one exists and the code it covers changed after the commit it records as last in sync, mention `/maintain-formal-verification-skill` if the question touches that code. When the model rule is missing and it matters, ask whether the user wants to pick a model for each role and a reasoning budget now. It matters when the user is new, the question is about setup or cost, or the answer depends on which models run. Ask at most once per chat. If the need is also unclear, ask both questions together. Offer two choices: @@ -87,6 +87,7 @@ The default answer is `/poteto-mode`, which runs most of the others when its ste | Give agents a scripted way to drive the app and prove behavior | [`/create-verification-skill`](../create-verification-skill/SKILL.md) | | Bring a verification skill and its feature map back in line with the app | [`/maintain-verification-skill`](../maintain-verification-skill/SKILL.md) | | Formally verify a race, invariant, or other property that tests rarely reach | [`/create-formal-verification-skill`](../create-formal-verification-skill/SKILL.md) | +| Bring a formal verification back in line after the code it covers changed, and learn whether a failure is drift or a bug | [`/maintain-formal-verification-skill`](../maintain-formal-verification-skill/SKILL.md) | | Vet a performance number before reporting or acting on it | [`/benchmark-checklist`](../benchmark-checklist/SKILL.md) | | Run a large or cross-cutting change, or one to review after stepping away | [`/figure-it-out`](../figure-it-out/SKILL.md) | | Keep a decision log during a run, and review it afterward | [`/show-me-your-work`](../show-me-your-work/SKILL.md) | diff --git a/pstack/skills/poteto-help/references/recipes.md b/pstack/skills/poteto-help/references/recipes.md index 2d785761d..c4f60466c 100644 --- a/pstack/skills/poteto-help/references/recipes.md +++ b/pstack/skills/poteto-help/references/recipes.md @@ -34,7 +34,7 @@ Swap in the real paths, skills, and done checks. Informal wording works. ## Review and ship - `/interrogate the whole branch, but skeptically. don't change anything yet. no nitpicks unless it's a real bug or regression.` Read the dismissals too. -- `/create-formal-verification-skill prove holds in , even when interleave or retry.` +- `/create-formal-verification-skill prove holds in , even when interleave or retry.` After merges or refactors in that code: `/maintain-formal-verification-skill`. - `/swarm check every package under against its check script. one worker per package. one report.` - `/poteto-mode open the pr. small ordered commits, evidence in the description.` - `/poteto-mode babysit this pr. get it green.` For status only: `/poteto-mode check on pr . anything outstanding?`