Maintain Formal Verification Skill
Bring a project's formal verification back in line with the code after the code...
Install
npx skills add michael-denyer/pstack-claude --skill maintain-formal-verification-skill -g -a claude-code -y- Repository
- michael-denyer/pstack-claude3.7k
- Category
- Engineering
- Updated
- 5d ago
- License
- MIT
- Context cost
- Mediumabout 1,766 tokens
- Runs scripts
- No, instructions only
What it does
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.
Maintain a formal verification skill
On Codex, read the platform mapping, including its per-skill notes, before following this skill.
On GitHub Copilot, read the platform mapping, including its per-skill notes, before following this skill.
On Muse, read the platform mapping, including its per-skill notes, before following this 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 formal verification 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.
