mcpField
M
maintain-formal-verification-skill

maintain-formal-verification-skill

github.com/yeachan-heoOther40.7k8 installsUpdated today
Repository

About maintain-formal-verification-skill

Maintain Formal Verification Skill is a skill for syncing an existing formal-verification project skill with the code it models. It checks citations and assumptions, updates the model when needed, reruns the verifier, and records the resync without weakening the property.

Key features

  1. 01Audits code citations and assumptions
  2. 02Detects model drift
  3. 03Updates steps and assumptions to match code
  4. 04Reruns the verification tool
  5. 05Records results through the ledger

Use cases

  1. 01Refreshing a model after protocol or invariant changes
  2. 02Checking citations after refactoring
  3. 03Revalidating a green run against recent code
  4. 04Deciding when model regeneration is needed

Install

Copy the command and run it in a terminal.

$npx skills add https://github.com/yeachan-heo/oh-my-claudecode --skill maintain-formal-verification-skill

After installing, type/maintain-formal-verification-skillin Claude Code to confirm it loaded.

Details

From the project README

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.

Comments

Markdown supported