Codex mapping

Use the selected repository's project-local skill location, preferring .agents/skills/ for Codex. Keep generated verification files and scratch mutations inside that repository or a disposable copy. Follow native permissions for tool installation and external access. The existing proof-orchestrator selects the proof path; model-capability-router owns any model choice. A model check proves its stated model and bounds, not unexamined product code. Do not alter product code or weaken a property to obtain a pass.

Maintain a formal verification 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 verify skill that /cursor-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.