Check whether a lemma still names the current source

Bindings in .proof/lemma-bindings.json record hashes for the target function and the lemma's function-literal body. The verify-stage check recomputes those fingerprints and reports target drift, lemma drift, both, or an unresolved directive. The default severity is warning. An absent or empty binding inventory skips; it does not establish that all production functions have proofs.

Reviewed target: clamp retries into [1, 10]
Current target:  clamp retries into [1, 20]
Bound lemma:    result <= 10
Review issue:   target changed after the recorded binding

The freshness finding says the old correspondence must be revisited. It does not itself say whether the new code is wrong. If the product limit intentionally became 20, the requirement and proof claim also need review. If the limit remains 10, the implementation change may be the defect.

Use the binding inventory to locate the target and lemma. Read both bodies before accepting a refreshed result. Then run the solver against the intended package and inspect its verdict. If the directive was removed accidentally, restore it; if the claim was deliberately retired, remove only its obsolete binding through a reviewed change.

proof bindings
proof verify-lemma --no-cache ./internal/retry
proof audit --check lemma_binding_freshness --verbose

The separate function literal is a trusted description in this binding mechanism. Matching hashes establish that the reviewed artifacts have not changed, not that the literal is semantically equivalent to production code. A weakened lemma can also verify successfully. Preserve the substantive review of the claim. Deleting the whole binding file or editing stored hashes would erase the warning without repairing the evidence, so neither is a valid freshness repair.

Follow the evidence

Review both sides of the first drifted binding and decide which claim is still intended.

Review one changed lemma binding. Bring the target diff and bound claim so we can assess what changed, whether the claim still applies and which analysis needs a fresh run.

Understand source correspondence · Inspect recorded verdicts