Cittela — Verified Isolation Proofs for Multi-Tenant LLM Inference (Lean + Verus)
Cittela — Verified Isolation Proofs for Multi-Tenant LLM Inference (Lean + Verus)
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.
formal verification · Lean · Verus · multi-tenant isolation · LLM inference · tenant isolation · write integrity · geometric rotation
formal verification · Lean · Verus · multi-tenant isolation · LLM inference · tenant isolation · write integrity · geometric rotation
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).0 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!