# Maintain Formal Verification Skill

Bring a project's formal verification back in line with the code after the code...

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

## Install

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

## 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.

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

# Maintain 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 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.

## Edit scope

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