A self-verifying, self-improving Place for an AI to live within: an untrusted inhabitant acts through a machine-checked policy envelope whose own verified prover (Candle/HOL Light on CakeML) gates every self-modification — including upgrading the proof-checker itself. Zero cheat tactics; honest, labeled epistemic boundary.