Wrap each native/solver worker in run_bounded with CPU,wall,RSS and output limits; hard total tranche deadline; no solver-internal process portfolios; checkpoint exact inputs, unknowns, solver hits, reconstructed proofs, genuine LLM tokens and fresh HA accepts separately.
Method: structural-check. Induction: none. Risk: high.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.