Confidence in Confinement: An Axiom-Free, Mechanized Verification [pdf](doerrie.us)