Create Formal Verification Skill
Generate a project-local skill that formally verifies the code where a bug costs the...
Install
npx skills add michael-denyer/pstack-claude --skill create-formal-verification-skill -g -a claude-code -y- Repository
- michael-denyer/pstack-claude3.7k
- Category
- Testing
- Updated
- 5d ago
- License
- MIT
- Context cost
- Lightabout 1,458 tokens
- Runs scripts
- No, instructions only
What it does
Generate a project-local skill that formally verifies the code where a bug costs the most and tests reach the least, in any language, with whichever verification tool fits. Use for /create-formal-verification-skill, \"model-check this race\", \"prove this invariant\", or when concurrency, retries, state machines, parsers, or unsafe code need more than tests.
Create 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 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
Answer from the codebase, and ask the user only what you cannot observe. If the user named an area or a bug, start there.
A good target is a promise the code makes, where a break harms users and tests rarely reach the case that breaks it. Choose the strongest such target in the repo, not the one that is easiest to verify.
