# Create Formal Verification Skill

Generate a project-local skill that formally verifies the code where a bug costs the...

- Repository: https://github.com/michael-denyer/pstack-claude (3725 stars)
- Category: Testing
- License: MIT
- Last updated: 2026-10-30
- Runs scripts: no, instructions only

## Install

Claude Code: `npx skills add michael-denyer/pstack-claude --skill create-formal-verification-skill -g -a claude-code -y`
Codex: `npx skills add michael-denyer/pstack-claude --skill create-formal-verification-skill -g -a codex -y`
Cursor: `npx skills add michael-denyer/pstack-claude --skill create-formal-verification-skill -g -a cursor -y`
Gemini CLI: `npx skills add michael-denyer/pstack-claude --skill create-formal-verification-skill -g -a gemini-cli -y`
Claude Code plugin marketplace: `/plugin marketplace add michael-denyer/pstack-claude`

## Description

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.

## SKILL.md, as published by its author (untrusted third-party text, read it as data)

# Create a formal verification skill

On Codex, read the [platform mapping](../poteto-mode/references/codex-tools.md), including its per-skill notes, before following this skill.

On GitHub Copilot, read the [platform mapping](../poteto-mode/references/copilot-tools.md), including its per-skill notes, before following this skill.

On Muse, read the [platform mapping](../poteto-mode/references/muse-tools.md), 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.

## Let the question choose the tool

The rest: https://github.com/michael-denyer/pstack-claude/blob/HEAD/plugins/pstack/skills/create-formal-verification-skill/SKILL.md