We closed the cross-tenant KV-cache leak to zero.

Twelve prompts, one A100, every tenant's own reuse intact. And the floor is machine-checked: zero-leak sharing costs at least T·n bits of state.

Try the Verifier View Artifacts

Measured on an NVIDIA A100, 24 July 2026. The run

1,852Lean 4 theorem and lemma declarations in this codebase: none left unproved, none resting on an axiom of our own, none decided by running compiled code
19.645%proven ceiling on the hit rate of any demand-fetch cache on the public Mooncake production trace
32 = OPTpooled KV placement hits the certified optimum; an independent Google OR-Tools solver proves no placement does better
11results whose checking program was shown to catch a deliberately planted defect

What the technology does

We do not tune heuristics. We map the mathematical limits of multi-tenant inference: what isolation must cost, what any cache can hit, and where pooling is optimal — then show the leak and the fix on real GPUs.

Served to the tenant who cached it

Served to a different tenant, no salt

Served to a different tenant, salted: nothing, on any prompt

Every prompt of the live run on an NVIDIA A100, left to right. The middle row is the leak: a different tenant was served exactly what the first tenant had cached. The bottom row is the same run with a per-tenant salt bound at admission. Nothing, on every prompt, while the top row is unchanged. The run

The leak, reproduced
On an NVIDIA A100 serving Qwen2.5-7B, one tenant was served another tenant's cached prompt blocks on every one of 12 distinct prompts — 544 to 784 tokens each — through the engine's shared prefix cache.
The run
Closed to zero
With a per-tenant cache salt bound to the tenant at admission, cross-tenant reuse fell to 0 on all 12 prompts while each tenant's own reuse was preserved exactly. On an L4, an adversary who knew the salt scheme read 0 tokens on all 24 prompts under a keyed salt, while the same attack on an unkeyed salt still recovered 544 — so the zero is not vacuous.
The run
Method, not magic
The salting mechanism is vLLM's own (merged April 2025). What we bring is the method: reproduce the leak before claiming the fix, run controls that could have failed, refuse unsalted requests at admission, and prove the state any correct design must carry.
Proven limits
Lean 4 theorems fix what isolation costs (T·n bits), what any cache can hit on a given trace, and when pooling is optimal.

Zero-Trust Verification

Do not trust our marketing. Drag and drop a .json certificate or receipt below to verify our claims locally in your browser. No network requests are made.

It hashes the file you hand it, in this tab.
It looks that hash up in the list of every file this site publishes, which is already on the page.
It reads the theorem names the document claims and checks each one against the same list.

Green only if the bytes are a file we published and every theorem the document names is one we published. Anything else is red.

Stranger Verifier · runs in this tab

$ Drop a .json certificate or receipt anywhere on this panel.

SHA-256 runs in WebAssembly in this tab. Every published file and all 34 theorem names are already on the page.

or try a sample

The T·n bits certificateDownload
The live-GPU leak-and-closure runDownload
A tampered copy of the first oneDownload

Theorems & Bounds

Three statements about multi-tenant inference that hold for every design, not just ours. Each one is a limit a buyer can hold a vendor to.

Checked by the Lean 4 kernel
$\forall σ : Auth_{T \times n} \to Fin s, (\forall M, c : serve (σ M, c) = M_{c}) ⟹ 2^{T n} \leq s and T \cdot n \leq lo g_{2} s$
$\forall σ : Auth_{T \times n} \to Fin s, (\forall M, c : serve (σ M, c) = M_{c})$ $⟹ 2^{T n} \leq s and T \cdot n \leq lo g_{2} s$
The price of zero-leak cache sharing
No GPU memory manager can share cached prompts across T tenants and n blocks with zero leakage and full reuse using fewer than T·n bits of isolation state. Below that floor a design either leaks or refuses a reuse it was entitled to — there is no third option and no clever encoding.
Certificate
Checked by the Lean 4 kernel
$\forall P \in DemandStep, \forall r : hits_{P} (r) + distinct (r) \leq ∣ r ∣;$ $Mooncake: \frac{21069 - 16930}{21069} = 19.645%$
$\forall P \in DemandStep, \forall r :$ $hits_{P} (r) + distinct (r) \leq ∣ r ∣;$ $Mooncake: \frac{21069 - 16930}{21069} = 19.645%$
No cache beats the traffic
No cache that fetches only what it is asked for can hit more often than the repeats in the traffic allow. On the public Mooncake production trace that ceiling is 19.645%; simulated LRU reaches 5.5% and an optimal offline policy reaches the ceiling — so the headroom is in the policy, and no vendor can promise more than the trace permits.
Certificate
Certified optimal by CP-SAT
$misses (pooled) = 32 = OPT (CP-SAT: OPTIMAL, bound 32);$ $\forall routings, policies, traces : misses \geq wall$
$misses (pooled) = 32 = OPT$ $(CP-SAT: OPTIMAL, bound 32);$ $\forall routings, policies, traces : misses \geq wall$
Pooled KV placement is optimal
On the committed serving instance, a pooled KV cache reaches the proven minimum number of misses and per-instance caching structurally cannot; an independent Google OR-Tools solver certifies the optimum. At 16 hosts the pooled cache keeps a 93.75% hit rate while per-instance caching falls to 34%.
Certificate

Artifacts & Open Source

Reproducible science and open artifacts. The measurements behind this page are published as datasets, the tools that make them are public, and every uninterpretable row is kept and marked rather than dropped.

13open artifacts. Every one of them answered when this page was built. The datasets were downloaded 141 times in the last month.

Datasets

Live demos

Open-source code

Read from the Hugging Face and GitHub interfaces when this page was built.

Intellectual Property

The diligence room, on the home page. One filed provisional covers the admission layer this company is built on, claim by claim.

727 claimsProvisional filed. Counted from the numbered claim set of the filing itself, not recalled.

Technology Genus	Claims	Status	Validation Engines
Proof-carrying admission for AI inference infrastructure: tenant-rights capability engines and partition-key binding for shared KV caches, cross-instance reuse, memory zeroization, exactly-once state migration, and interconnect, power and scheduling admission gates (2 genera, 87 mechanism groups)	727	Provisional filed	Lean 4 proofs, CP-SAT optimality certificates, live-GPU reproductions

Independent claim sets

Mechanism groups

Two independent claim sets and eighty-seven mechanism groups, one bar each, counted from the numbered claims of the filing itself. The count

Operational Envelope & Disclosures

Isolation, not speed: the isolation layer runs at 0.874× native vLLM prefix-cache throughput (0.931× against LMCache).
Leak and closure are single-GPU runs on open models (A100 / Qwen2.5-7B, 12 prompts; L4 / Qwen2.5-1.5B, 24 prompts). With 0 cross-tenant hits in 12, the 95% upper bound on the residual rate is 0.25, not zero.
The salt is a namespace separator, not encryption: a request without a correct tenant-bound salt falls back to the engine's shared cache and must be refused at admission.
The T·n floor is for arbitrary shared-read rights; if every block belongs to one tenant, the floor is n·log2 T bits.
The optimality certificate covers one committed, uncapacitated serving instance, not a fleet benchmark; cache ceilings are per trace.
All patent filings are provisional. No patent has been granted.

Evidence state of every figure on this page

All 11 figures on this page are in one state: backed by a served file whose bytes hash to the record printed beside them. None of the twelve states below applies to any figure here; each is listed with the rule that would put one there.

loadinga figure read in the browser before its file has loaded
unsearcheda question this page has never checked
searched none founda question checked with nothing found
no data availablea file that exists but holds no value for the row
search faileda figure whose served file is missing or no longer hashes to its record
unresolved identitytwo files that disagree about which object a figure describes
underpowereda sample too small for the claim, printed with its n
contradictorytwo files that give different values for one quantity, both shown
license restricteda file that cannot be published, shown by path and hash only
stalea measurement older than seven days, printed with its age
not applicablea question that does not apply to this page
analysis faileda measurement whose generator errored

We closed the cross-tenant KV-cache leak to zero.

What the technology does

The leak, reproduced

Closed to zero

Method, not magic

Proven limits