/maintain-formal-verification-skill

name: maintain-formal-verification-skill
description: "Re-sync an existing formal verification skill after the covered code changed: re-check every assumption, update cited lines, rerun the tool; formally-verified only after a green rerun."
aliases: []
metadata:
  credits:
    verification-maintenance: pstack
    author: Lauren Tan
    url: "https://github.com/cursor/plugins/tree/main/pstack"
    port: pstack-claude
    port-author: Michael Denyer
    port-url: "https://github.com/michael-denyer/pstack-claude"

Maintain Formal Verification Skill

A formal spec that cites lines that no longer exist is stale, and a stale spec's green is worthless. This skill re-syncs an existing `verify-formal-*` project skill (created by `create-formal-verification-skill`) to the code it models.

When to use

• the modeled protocol, arithmetic, or invariant changed shape
• cited file:line anchors drifted after refactors
• before trusting a green run that predates recent changes to the covered

code

Workflow

1. **Inventory the model's bindings**: every cited file:line, every named function, every assumption on the skill's assumption list. 2. **Re-check each binding against current code**: does the cited line still contain the modeled step? Does the assumption still hold (pid reuse, atomicity, integer width, timing)? A binding that no longer matches is drift; record it, do not silently absorb it. 3. **Update the model** where drift is real: move citations, adjust steps to the new protocol shape, and rewrite the assumption list to match reality. The property itself does not weaken — if the new code violates the property, that is a finding to report, not a model edit. 4. **Rerun the tool** (`TLC`/`apalache`, `lake build`, `cargo kani`) and capture real output. 5. **Update the project skill** in place: new citations, new assumption list, same run command — and record the resync through the ledger's locked writer (`appendLedgerEntry` and `defaultLedgerPath` from the installed package's `dist/features/verification-ledger/index.js`; `babysit`'s ledger step demonstrates the exact invocation — never append raw rows): `formally-verified` with the rerun command as evidence only when the rerun is green; a counterexample during resync records `verifier-failed` with the counterexample as evidence and is reported before any model change.

Rules

• A counterexample found during resync is reported before any model change;

verify whether the code shares the flaw.

• Never mark a resync done with an unrerun tool; the rerun is the resync.
• If more than half the bindings drifted, say so — the model may have been

modeling an implementation that no longer exists, and regeneration via `create-formal-verification-skill` is the honest path.