Reject altered premises/targets, missing natural guards, swapped variables, forged unsat, unsupported proof steps, DNE, truncated logs and stale caches; independently check identical accepted native bundle bytes in Lean.
Method: structural-check. Induction: none. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.