Machine-checked Lean and Verus proofs accompanying the paper "1000 Tenants, OneModel, One MacBook: Attacker-Tested Isolation for Multi-Tenant LLM Inference"(Zenodo, DOI 10.5281/zenodo.20727024). Three artifacts establish, for a per-tenantgeometric rotation mechanism: (1) the geometric core in Lean — isometry, matched-keyround-trip, wrong-key composition, and a non-aligning per-tenant key family; (2) tenantisolation with governed cross-tenant operation in Verus; (3) the same plus write-integrity(every cached entry was created by an authorized write). The guarantees are structural,not cryptographic: authorization gates are abstract predicates modelling whereauthorization is required, not unforgeable constructions. See README for scope andreproduction.