Maintain a formal verification skill

Maintain the verification artifacts and project-local instructions, preserving the property's intended promise. Edit only models, harnesses, property files, and verification instructions; change product code only within an existing grant. When a property fails on the current code, report the failure and keep the property and model as the code requires; weakening either to pass hides the finding. Use isolated scratch copies for deliberate faults.

Give each check one outcome:

• in sync: no change since the sync commit alters what the check describes, and it passes.
• updated: the verification now describes the changed code, and it passes.
• bug: the verification describes the current code, and the code breaks the property. This is a code finding, not drift.
• blocked: the check could not be brought back in line or run; name the reason.

A check can be both updated and bug.

1. Resolve the checks and comparison

Find project-local skills that run a model checker, prover, or code-level verifier against named code, including drafts and generated-input fallbacks produced by /pstack-create-formal-verification-skill. Read the user's named target, or every matching skill. If none exists, tell the user to invoke /pstack-create-formal-verification-skill and stop this path. Preserve the distinction between generated-input testing and formal proof.

For each check, record the property, covered files and functions, source correspondence, bounds, assumptions, tool version, command, and last confirmed sync commit. Resolve the target commit and included uncommitted or untracked changes. If a sync commit is absent, use the last commit changing the verification as a provisional baseline and disclose the uncertainty; unavailable history leaves the comparison blocked.