Paper deep dive
WitCert: Sound Runtime Risk Observability and Gating for KV-Cache Quantization
Fanzhe Wei, Li Liu
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 87%
Last extracted: 8/3/2026, 2:07:11 AM
Summary
The paper introduces WitCert, a runtime observability and gating system for KV-cache quantization in large language models. It proposes a 'meter' that provides a provably sound upper bound on the total variation between exact and compressed attention. The system features two tiers: a deterministic, position-invariant bound for black-box quantizers (Tier A) and a tighter probabilistic sub-Gaussian certificate for controlled INT8 quantizers (Tier B). Implemented within SGLang, WitCert enables live monitoring and risk-ranked gating, demonstrating that aggressive quantization schemes can be safely deployed by leveraging cross-layer error cancellation, significantly improving throughput without sacrificing quality.
Entities (15)
Relation Signals (9)
WitCert → implements → Runtime Risk Observability
confidence 95% · WitCert: Sound Runtime Risk Observability and Gating for KV-Cache Quantization
WitCert → implements → Gating
confidence 95% · WitCert: Sound Runtime Risk Observability and Gating for KV-Cache Quantization
WitCert → integrateswith → SGLang
confidence 95% · the meter enters SGLang through an env-guarded patch
WitCert → outperforms → Offline Benchmark Averages
confidence 90% · KV-cache quantization is validated today by offline benchmark averages; a deployed system cannot tell whether compression is damaging the request it is serving right now.
Band-norm-witness bound → provides → Deterministic Bound
confidence 90% · a deterministic band-norm-witness bound, sound for any cache-preserving black-box quantizer
WitCert → uses → Lean 4
confidence 90% · core theorems machine-checked in Lean 4
Subtractive dither → enables → Probabilistic Certificate
confidence 85% · tighter probabilistic certificate for a controlled subtractively-dithered INT8 quantizer
WitCert → handles → RoPE
confidence 85% · modern caches store keys after the RoPE rotation... witness must be invariant to position
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:KV-cache quantization is validated today by offline benchmark averages; a deployed system cannot tell whether compression is damaging the request it is serving right now. We give it a provably sound runtime meter, a "DTrace for KV quantization": a per-(layer, head, step) upper bound on the total variation between exact and compressed attention. The meter has two tiers: a deterministic band-norm-witness bound, sound for any cache-preserving black-box quantizer and for any query (adaptive-safe, worst-case Cauchy-Schwarz plus RoPE band-unitarity), and a tighter probabilistic certificate for a controlled subtractively-dithered INT8 quantizer under an explicit request-level failure budget (stated for non-adaptive queries; core theorems machine-checked in Lean 4). Three results. Observability: the meter enters SGLang through an environment-guarded patch, and any scheme registered as one tensor function is measured in live serving. Repair: meter-driven gating, risk-ranked where the witness is saturated and certified where it is informative, empirically restores the quality floor at benchmark scale. For example, raw-cast FP8 improves from 22.8 back to 79.7 on hard RULER tasks, with the difference from uncompressed bounded at [+0.0, +0.8] by a paired test. Analysis: aggressive schemes survive on cross-layer error cancellation, not per-step fidelity. In a 28-layer sweep, no single layer's pollution alone loses anything (0/28), and the certified INT8 cache serves 1.88 times more KV tokens at the same memory in SGLang.
Tags
Links
- Source: https://arxiv.org/abs/2607.28699v1
- Canonical: https://arxiv.org/abs/2607.28699v1
Trouble viewing inline? Open PDF directly →
Full Text
128,218 characters extracted from source content.
Expand or collapse full text
WitCert: Sound Runtime Risk Observability and Gating for KV-Cache Quantization Fanzhe Wei whyer1@gmail.com Metask Lab (https://metask.ai) Li Liu muriel092611@gmail.com Metask Lab (https://metask.ai) (July 30, 2026) Abstract KV-cache quantization is validated today by offline benchmark averages; a deployed system cannot tell whether compression is damaging the request it is serving right now. We give it a provably sound runtime meter—a “DTrace for KV quantization”: a per-(layer, head, step) upper bound on the total variation between exact and compressed attention. The meter has two tiers: a deterministic band-norm-witness bound, sound for any cache-preserving black-box quantizer and for any query (adaptive-safe, worst-case Cauchy–Schwarz plus RoPE band-unitarity), and a tighter probabilistic certificate for a controlled subtractively-dithered INT8 quantizer under an explicit request-level failure budget (stated for non-adaptive queries; core theorems machine-checked in Lean 4). Three results. Observability: the meter enters SGLang through an env-guarded patch, and any scheme registered as one tensor function is measured in live serving. Repair: meter-driven gating—risk-ranked where the witness is saturated, certified where it is informative—empirically restores the quality floor at benchmark scale, e.g. raw-cast fp8 from 22.8 back to 79.7 on hard RULER tasks with the difference from uncompressed bounded at [+0.0,+0.8][+0.0,+0.8] by a paired test. Analysis: aggressive schemes survive on cross-layer error cancellation, not per-step fidelity—in a 28-layer sweep, no single layer’s pollution alone loses anything (0/28)—and the certified int8 cache serves 1.88×1.88× more KV tokens at the same memory in SGLang. 1 Introduction Autoregressive decoding requires caching keys and values for every past token; beyond 32k context a 7B-class model spends gigabytes on the KV cache, and at 128k the cache exceeds the weights themselves. (Our quality evaluation spans 4–32k contexts; the memory account is measured to 128k; see the scope statement of Sec. 6.4.4.) The four established compression routes—token eviction (H2O [44], SnapKV [24]), channel/frequency pruning (ThinK [42], RAP [41]), low-rank factorization (Palu [6], KQ-SVD [21]), and quantization (KIVI [27], KVQuant [15])—share one defect: they are open loop; dynamic sparsity (Quest [37]) selects at run time but is likewise validated only offline. The policy is fixed offline or heuristically, and the error actually incurred on the current input is neither observable nor controllable. We observed the extreme form of this defect: under a query-agnostic protocol (the regime studied by the query-agnostic compression line [18]), SnapKV drops from 100 to 1.1–65 on RULER [16] needle tasks while the serving system emits no signal whatsoever (Sec. 6.3.3). Turning compression from open loop into closed loop requires a runtime-computable error bound. Runtime-Certified Quantized Attention [5] first supplied such certificates, but its bound is worst-case (TV≤tanh(max|ε|)TV≤ ( | |), data independent): we measured that at every practical threshold (τ≤0.2τ≤ 0.2) it authorizes zero compression—the certificate holds, but is too conservative to be useful. Our starting point is therefore: for a certificate to authorize compression, it must be data dependent. Two obstacles follow. First, a data-dependent bound needs the per-token error magnitude, yet the error depends on a query that has not yet arrived. Second, modern caches store keys after the RoPE rotation [35], so any witness must be invariant to position or it must be recomputed per position. Our answer is the residual witness (Sec. 4.1): the band-wise norms of the quantization residual solve both at once—they are query independent, computable once at write time, and position invariant because RoPE acts unitarily within a frequency band (Lemma 1). Terminology. We call the runtime quantity the meter: a sound upper bound on the attention total variation, reported as min(1,⋅) (1,·) since TV≤1TV≤ 1 always. The stored per-token summary it is computed from is the witness. When the meter is below saturation it is a certificate—a mathematically valid guarantee; above saturation its raw value remains an empirically discriminative risk score but guarantees nothing. Gating experiments are labelled certified (τ<1τ<1) or risk-ranked (τ≥1τ≥ 1) accordingly. Contributions: (1) a sound, position-invariant universal meter: the band-norm witness theorem for black-box cache-preserving schemes (Sec. 4.1), plus a cautionary counterexample, its sound replacement bound, saturation-aware min(1,⋅) (1,·) reporting, and a two-sided companion bound whose measured non-benefit we report (Secs. 3, 4.3); (2) a uniform sub-Gaussian runtime certificate for a controlled quantizer, with an explicit request-level failure budget and no witness storage, plus two negative controls on bound selection (Sec. 4); (3) a mechanism finding that benchmarks cannot produce: the observable failure of aggressive schemes is cross-layer accumulation, not per-step infidelity—in a 28-layer sweep no single layer’s pollution alone loses anything (0/28)—which explains both why aggressive schemes survive and why per-step bounds are intrinsically conservative (Sec. 6.4.1); (4) a system implementation in which the meter is structurally cheap and CUDA-graph capturable; the certify–fallback loop is closed and validated in our standalone harness (head- and block-granular paging, Secs. 6.3.4, 6.3.5) and, in live SGLang [45] serving, through the observatory pool at benchmark scale (Sec. 6.3.9); the packed certified cache in SGLang has certificate computation, storage, telemetry and fallback integrated, and its gated end-to-end quality is validated in Sec. 6.3.10; the remaining systems cost is repeated page-in without a request-level repair cache. 2 Related Work Low-rank. Palu [6] and STAR-KV [4] both compress the pre-RoPE representation and reconstruct at decode time, because RoPE blocks weight absorption on the key side (Palu: “the non-linear nature of these positional embeddings prevents the matrix fusion”). Palu itself prices this cost: 2.91×2.91× attention speedup with RoPE versus 6.17×6.17× without. KQ-SVD [21] gives a closed-form optimal low-rank factorization with a global Lipschitz bound on the attention output, but has no margin or per-row analysis and does not discuss RoPE at all. No prior work performs certified compression of post-RoPE keys. Sketching. BalanceKV [19] provides an end-to-end attention-output guarantee with a matching lower bound, but its constant e2r2/de^2r^2/ d is roughly e39.8e^39.8 at measured norms, and RoPE is never mentioned—the theory implicitly treats keys as position independent. Compactor [7] bounds the spectrum of the pre-RoPE K⊤K K and concedes that its experimental parameters violate its own theorem’s conditions. RoPE-aware compression. RAP [41] prunes RoPE column pairs and proves commutation with rotation—the rigidity proposition of Appendix C supplies the converse completeness—but requires LoRA distillation to recover. EliteKV [46] and KV-Latent [34] perform frequency selection or resampling, both requiring retraining and offering no bound. Block-GTQ [25] is the closest neighbour on the quantization axis (RoPE-aware bit allocation, real packed path) but provides no runtime certificate. Certified compression. Runtime-Certified Quantized Attention [5] is our primary interlocutor; we borrow its two-term decomposition and telemetry framing. The difference is that its softmax bound is a worst-case tanh(Δ) ( ) with Δ determined by the quantization step and query norm, independent of the per-token error actually incurred. We compare both against that propagation bound (verified sound by our own adversarial testing) under identical witnesses and against a full-system reproduction from the paper specification (Sec. 6.3.10). The latter includes block-level precision escalation, INT4 values, CPU backing storage and a two-pass scan; because no public implementation is available, we declare every reproduction deviation and report fidelity checks. The bound-shape comparison is deliberately two-sided: the det-tanh gate is cheaper in the loose-witness regime, whereas ours is tighter for the controlled-quantizer regime. On the competitive map: RaBitQCache [23] (binary-proxy score with a proven error bound, no TV certificate), Block-GTQ [25] (RoPE bit allocation, real packed path, no runtime certificate), KVQuant [15] (dense-and-sparse per-vector outliers, pre-RoPE), and KVarN [28]/CommVQ [22] (extreme low-bit baselines); the minimax analysis of [32] likewise argues for budgeting compression against the observed query distribution. A rigidity proposition (stated and proved in Appendix C) characterizes static RoPE-equivariant linear compression as exactly frequency-pair selection with per-frequency scalars; it explains the field’s current split—the RoPE-structure-aware methods carry no guarantee, and the methods that carry a guarantee route around RoPE—and justifies handling outliers at pair granularity. Conformal prediction and distribution-free UQ. Our request-level failure budget δreq _req and its union-bound allocation speak the language of distribution-free uncertainty quantification [39, 2], so a natural question is why we do not simply calibrate a split-conformal quantile of the true TV. The two guarantees are not interchangeable. Split conformal yields marginal coverage—averaged over requests exchangeable with a calibration set—whereas the meter is a per-request, conditional statement: it holds for the request being served, with no calibration set and no exchangeability assumption. The distinction matters precisely because compression fails out of distribution: the silent needle collapses of Sec. 6.3.3 occur exactly where a calibration set drawn from typical traffic stops being representative. Conformal calibration would also need the true TV as its conformity score, i.e. one uncompressed forward pass per calibration point—the cost the runtime meter avoids. The two are complementary rather than competing: calibrating the gate threshold τ conformally on live traffic is attractive future work. 3 A Plausible but Unsound Certificate, and its Sound Replacement Setup and notation. Fix one (layer, head, decode step). Let p and p~ p be the softmax attention distributions over the S cached tokens computed from exact and compressed keys respectively, εt _t the logit error of token t, and ct≥|εt|c_t≥| _t| any per-token error bound. We meter the total variation TV(p,p~)=12∑t|pt−p~t|TV(p, p)= 12 _t|p_t- p_t|. TV is the right target for two reasons: it is the operational quantity—the amount of attention mass that moves, so a silently dropped needle token is by definition a TV event—and it propagates linearly to the attention output: ‖y−y^‖≤2TVmaxt‖vt‖+∑tp~tρtv\|y- y\|≤ 2\,TV _t\|v_t\|+ _t p_tρ^v_t, where ρtv:=‖v^t−vt‖ρ^v_t:=\| v_t-v_t\| is token t’s value reconstruction error (Sec. 4), so a TV budget is an output-error budget. All norms are Euclidean; we write TVKTV_K when the value side is also in scope. Since TV≤1TV≤ 1 holds trivially, any upper bound is informative only below 11; the meter is therefore reported as min(1,⋅) (1,·) throughout. The flawed certificate. With c¯=p~[c] c=E_ p[c] and cmax=maxtctc_ = _tc_t, a natural-looking bound is TV(p,p~)≤?12e2cmax(p~[|c−c¯|]+c¯(ecmax−1)),TV(p, p)\; ?≤\; 12e^2c_ (E_ p [|c- c| ]+ c\,(e^c_ -1) ), (1) whose intuition is “errors are attention weighted, so a small dispersion of the bound implies small TV.” This is wrong: ctc_t constrains only |εt|| _t|. When all ctc_t are equal the first-order term vanishes, yet errors of opposite sign still produce an O(c)O(c) change in TV. Minimal counterexample. Take p~=(12,12) p=( 12, 12), c=(0.1,0.1)c=(0.1,0.1), ε=(0.1,−0.1) =(0.1,-0.1). The true total variation is 0.0498340.049834, while (1) returns 0.0064230.006423—a factor of 7.87.8. Notably, (1) passed 32,25632,256 checks in our own earlier experiments because those checks compared mean TV against mean bound over a batch of queries; per-query checking exposes the violation immediately. We report this as a methodological lesson: certificates must be validated per query and adversarially, never in aggregate. Theorem 1 (Sound replacement). Let A=p~[ec]A=E_ p[e^c]. If |εt|≤ct| _t|≤ c_t for all t, then TV(p,p~)≤12(A2−1)TV(p, p)≤ 12\,(A^2-1). Proof. Since |εt|≤ct| _t|≤ c_t, Cauchy–Schwarz gives p~[ec]p~[e−c]≥1E_ p[e^c]\,E_ p[e^-c]≥ 1 and hence 1/A≤p~[e−ε]≤A1/A _ p[e^- ]≤ A, so |log(pt/p~t)|≤ct+logA | (p_t/ p_t) |≤ c_t+ A and therefore |pt/p~t−1|≤Aect−1|p_t/ p_t-1|≤ Ae^c_t-1. Taking expectation under p~ p gives TV=12p~[|p/p~−1|]≤12(A2−1)TV= 12E_ p [|p/ p-1| ]≤ 12(A^2-1). ∎ The first-order behaviour is c¯ c, the attention-weighted mean of the bound. We validated the replacement with 500,000 adversarial trials (extreme sign patterns, peaked and flat distributions, large c) and froze both the counterexample and the adversarial suite as a regression guard in the repository. Numerically we evaluate A in the log domain and return the trivial bound 11 on overflow; we never truncate the error parameter itself. 4 The Two-Tier Meter: a Universal Witness Bound and a Sub-Gaussian Certificate 4.1 Tier A: a deterministic witness bound for black-box cache-preserving schemes Modern caches store keys after the RoPE rotation, so any stored error summary must be invariant to the (not yet known) query position. Write d for the head dimension and group the d/2d/2 RoPE frequency pairs into B contiguous bands (the system integration uses B=16B=16, i.e. 32 B/tok/head; the offline six-quantizer study of Fig. 1 uses B=8B=8, 16 B; band b spans the coordinates of d/(2B)d/(2B) frequency pairs). Scope. Tier A covers any scheme that, for every cached token, materializes a reconstructed key k^t k_t of the same shape—i.e. arbitrary quantizers and any transform whose output can be written back as a per-token key. Eviction, token pooling/merging, latent caches and recurrent-state compressions store no per-token reconstruction, so no residual exists and Tier A does not apply to them; certifying eviction online is exactly open problem (3) of Sec. 6.4.6. Within this scope, at write time let rt=k^t−ktr_t= k_t-k_t be the residual, and store the witness wt,b=‖rt,b‖,b=1,…,B,w_t,b\;=\;\|r_t,b\|, b=1,…,B, (2) the per-band Euclidean norms of the residual (stored in fp16, 2B=322B=32 bytes per token per head, written B/tok/head below). Lemma 1 (RoPE band unitarity). Let RnR_n be the RoPE rotation at relative position n (we reserve m for the outlier-pair count): block diagonal over frequency pairs, acting on pair j as the 2×22× 2 rotation by angle nθjn _j. Every frequency pair lies inside a single band, so for every band b, every x and every n, ‖(Rnx)b‖=‖xb‖\|(R_nx)_b\|=\|x_b\|. In particular the witness of a post-RoPE residual equals the witness of the corresponding pre-RoPE residual, and is invariant to the query position. Proof. RnR_n restricted to band b is a direct sum of 2×22× 2 rotations, hence orthogonal on the band’s subspace. ∎ Theorem 2 (Sound black-box logit bound). For any query q (post-RoPE, softmax scale 1/d1/ d) and any cached token t with residual rtr_t, |εt|=|q⋅rt|d≤1d∑b=1B∥qb∥wt,b=:ct,| _t|\;=\; |q· r_t| d\;≤\; 1 d _b=1^B\|q_b\|\,w_t,b\;=:\;c_t, by Cauchy–Schwarz applied within each band together with Lemma 1. The bound is computable at decode time from the current query and the stored witness alone, for any cache-preserving scheme, with no assumption on the residual distribution; feeding ctc_t into Theorem 1 yields a sound TV meter for any such scheme. Three remarks. (i) Proof–kernel correspondence: the deployed kernel computes exactly this quantity—witness_of stores the witness (2) at write time and the decode kernel accumulates ct=sm_scale⋅∑b‖qb‖wt,bc_t=sm\_scale· _b\|q_b\|w_t,b—so the theorem and the implementation match term by term. (i) Cost: 32 B/tok/head of storage (12.5%12.5\% of an fp16 key) and one length-B dot product per (query, token), which shares the attention kernel’s data pass (Sec. 6.2.2). (i) Tightness: the bound is tight when the residual concentrates in few bands and is loose when residuals are dense and sign-alternating—1289×1289× loose at 4 bits—which is why the universal meter saturates for 1–2 bit schemes: with the current band-norm witness, per-step certification of such schemes is vacuous—a statement about this witness, not an impossibility proof; whether a better constant-size witness exists below 8 bits is precisely open problem (1) of Sec. 6.4.6. (The cross-layer mechanism of Sec. 6.4.1 explains why any per-step bound, however tight, must be conservative for aggressive schemes.) Figure 1: The universal meter on six black-box quantizers, per-cell diagnostics (n=4480n=4480 cells each, unclamped log-domain values). Left: per-cell scatter—zero points below y=xy=x (soundness); below the saturation line the meter is also informative. Middle: tightness CDF (bound/TV)—8-bit schemes concentrate near 101.510^1.5, 1–2 bit schemes are vacuous by many orders of magnitude; all mass ≥0≥ 0 is soundness again. Right: ROC of the raw bound as a danger classifier (danger == TV>>0.2)—8-bit schemes detect essentially all danger at near-zero false-alarm rate, while sign-1bit tracks the diagonal, i.e. with the current witness its per-step score carries no signal (tightening it is open problem (1)). 4.2 Tier B: a sub-Gaussian certificate for a controlled quantizer Subtractive dither. We quantize with x^=s(round(x/s+ξ)−ξ) x=s\,(round(x/s+ξ)-ξ) where the dither ξ∼[−12,12)ξ [- 12, 12) is regenerated deterministically at read time. That the residual is then independent of the input and uniform per channel is classical dither theory [26, 14]; our contribution is wiring it into a KV-cache kernel under a proof–kernel contract and propagating it to a TV certificate. We choose s=amaxblk/(Q−12)s=amax_blk/(Q- 12), with Q=127Q=127 the top INT8 level (so Q−12=126.5Q- 12=126.5), so that clipping never occurs on non-outlier channels—a prerequisite for the assumption below. Lemma 2 (Uniform sub-Gaussian proxy). For X∼[−a,a]X [-a,a] we have [eλX]=sinh(λa)/(λa)≤eλ2a2/6E[e^λ X]= (λ a)/(λ a)≤ e^λ^2a^2/6. Hence the residual of subtractive dither with step s satisfies [eλX]≤eλ2s2/24E[e^λ X]≤ e^λ^2s^2/24 and is sub-Gaussian with proxy exactly s2/12s^2/12, i.e. equal to its variance. By Lemma 2, the logit error has variance proxy ςt2=1d∑cqc2sc,t2/12 ^2_t= 1d _cq_c^2\,s_c,t^2/12 (the scale sc,ts_c,t is block-constant in t; the same quantity is computed in-kernel as ςh,t2 ^2_h,t in Sec. 6.2.3) and, with probability at least 1−δloc1- _loc jointly over S tokens, |εt|≤ut:=2ςt2log(2S/δloc)| _t|≤ u_t:= 2 ^2_t (2S/ _loc), which is then propagated by Theorem 1 as A=∑tp~teutA= _t p_te^u_t. Crucially, VtV_t is computable from the stored quantization scales and the current query alone: no witness needs to be stored—the price of Tier A’s 32 B/tok/head is paid only by black-box schemes. Request-level budget. We allocate δloc=δreq/(L⋅H⋅T) _loc= _req/(L· H· T) over layers, heads and decode steps, so the guarantee is stated at the request level. Because the dependence is log(1/δ) (1/δ), tightening δ by orders of magnitude is inexpensive—quantified in Sec. 5. Scope of the probabilistic guarantee: non-adaptive queries. The sub-Gaussian argument conditions on the query, i.e. it treats q as statistically independent of the stored dither. That holds exactly for non-adaptive queries: prefill queries over a given text, teacher-forced or otherwise fixed token trajectories, and any evaluation in which the trajectory is not itself a function of the compressed cache. In free-running decoding it does not hold: the query at step t is a continuous function of earlier attention outputs and hence of the very residuals being bounded, an adaptive dependence that no union bound repairs. We state this as an explicit assumption rather than hide it, with three consequences. (i) Tier A is adaptive-safe: the witness bound of Theorem 2 is a worst-case inequality valid for every query, adaptive or not, so the universal meter—and every gating result in Sec. 6.3.9, all of which are driven by Tier-A witnesses—carries no adaptivity caveat. (i) Beyond the fixed-trajectory zero-violation evidence (200-seed request-level counting, the kernel soundness checks), we have now measured adaptive violations directly under free-running decoding (8×8×H200, Qwen2.5-7B, 50 prompts × 20 dither seeds, prefill 4096, decode 64, δreq=10−2 _req=10^-2; at every step the true TV of every (layer, head) cell is computed by a parallel exact forward and compared against the runtime certificate): 0/1000 adaptive requests violated, 0/1000 in the teacher-forced control, over 100,352,000 monitored cells in total (numerical tolerance 10−910^-9; the zero-tolerance residual consists entirely of margins ≤1.8×10−13≤ 1.8× 10^-13, i.e. double-precision rounding, reported as such). Adaptivity was genuinely realized—62.9% of free trajectories diverged from the fp16 baseline (median divergence step 22)—and the worst-case TV-to-bound ratio was 0.536; rule-of-three puts the request-level violation rate below 0.3% at 95% confidence. We state the epistemic status plainly: this is validation, not proof. (i) A martingale-style adaptive analysis, or a randomness-splitting design in which the certificate consumes dither that the generation path never touches, would restore the formal guarantee for free decoding; both remain open (and the same gap is unaddressed in prior runtime-certificate work). Outlier RoPE pairs. A small number of frequency pairs (selected per block by pair scale energy) are kept in FP16 and excluded from the variance term. This costs 16.116.1 B/tok/head, i.e. +6.3%+6.3\% over the FP16 key (256256 B) and +12.5%+12.5\% over the INT8 payload (129129 B), and is the single largest lever on coverage: the ablation shows that without it, sub-Gaussian authorization collapses to nearly zero. Value side and the joint event. Values carry no RoPE and their error propagates linearly, contributing the deterministic term ∑tp~tρtv _t p_tρ^v_t of the output bound above. The joint event is passK∧passVpass_K _V, evaluated per (layer, KV head, position); we report joint coverage rather than inferring it from marginals. On the event EKE_K the joint output bound is ‖y−y^‖≤2TVKmaxt‖vt‖+∑tp~tρtv\|y- y\|≤ 2\,TV_K _t\|v_t\|+ _t p_tρ^v_t. 4.3 Saturation, clamping, and a two-sided tightening Since TV≤1TV≤ 1, the sound meter value is min(1,12(A2−1)) \! (1, 12(A^2-1) ); raw values above saturation carry no guarantee, but remain an empirically discriminative risk score (the fallback experiment of Sec. 6.3.4 shows a 27.6×27.6× error reduction precisely on the cases the raw score selects). This distinction is load bearing for the gating experiments of Sec. 6.3.9 and is marked there explicitly: certified gating operates at τ<1τ<1, risk-ranked gating at τ≥1τ≥ 1. The one-sided e-form is quadratically punished by a single large ctc_t. A second application of the same reasoning gives a companion bound that is linear in that regime: Proposition 1 (Two-sided form). Let A=∑tp~tectA= _t p_te^c_t and A−=∑tp~te−ctA^-= _t p_te^-c_t. If |εt|≤ct| _t|≤ c_t for all t, then TV(p,p~)≤12(A−A−A),TV(p, p)\;≤\; 12 ( AA^-- A^-A ), and the meter min(1,12(A2−1),12(A/A−A−/A)) \! (1,\ 12(A^2-1),\ 12(A/A^--A^-/A) ) is sound. Proof. With Z=∑tp~te−εtZ= _t p_te^- _t we have pt/p~t=e−εt/Zp_t/ p_t=e^- _t/Z and A−≤Z≤A^-≤ Z≤ A, so pt/p~t∈[e−ct/A,ect/A−]p_t/ p_t∈[\,e^-c_t/A,\ e^c_t/A^-\,], an interval containing 11 (because A−≤1≤A^-≤ 1≤ A). Hence |pt/p~t−1|≤(1−e−ct/A)+(ect/A−1)|p_t/ p_t-1|≤(1-e^-c_t/A)+(e^c_t/A^--1), and taking the p~ p-expectation gives TV≤12((1−A−/A)+(A/A−1))=12(A/A−A−/A)TV≤ 12 ((1-A^-/A)+(A/A^--1) )= 12(A/A^--A^-/A). Neither form dominates the other (at A=2A=2, A−=0.6A^-=0.6 the two-sided form is looser), so the minimum is taken. ∎ The point is the massive-activation regime: if one token carries p~ p-mass η with a huge bound C, write M=ηeC≫1M=η\,e^C 1; then A2−1≈M2+2MA^2-1≈ M^2+2M grows quadratically in M while A/A−A−/A≈MA/A^--A^-/A≈ M grows linearly. This is exactly the mechanism that drives the meter to 1.6×1021.6× 10^2 in Sec. 6.3.7 and the regime where the capped det-tanh shape currently wins the traffic comparison (Sec. 6.4.2). Structurally, A−A^- is a softmax-weighted average exactly like A, so it merges across split-KV partitions under the same LSE weights (the argument of Sec. 6.2.2) and would cost one extra accumulator. Measured: the tightening does not materialize on real activations, and we report this negative result as such. We evaluated Proposition 1 offline on the six-quantizer harness of Fig. 1 (n=4480n=4480 cells per scheme; exp/out/p37_twosided_bound.json), including the per-token retention form 12∑tp~tmin(Aect−1,max(ect/A−1, 1−e−ct/A)) 12 _t p_t (Ae^c_t-1,\ (e^c_t/A^--1,\ 1-e^-c_t/A) ), which dominates both aggregates. In the informative regime (rtn-8bit) the aggregate two-sided form is 1.7×1.7× looser at the median and wins on only 1.6–1.7% of cells; the per-token min coincides with the one-sided bound at the median (shrink 1.00×1.00×) and lifts coverage at τ=0.2τ=0.2 only from 0.445 to 0.446. In the saturated regime the raw score shrinks by up to 26,433×26,433× (rtn-2bit median; log-domain evaluation, no truncation of c) yet remains astronomically above 11 (median 1012.510^12.5, maximum 1026610^266), so the reported meter is pinned at saturation either way. The measurement refutes the single-spike picture on real data: massive-activation channels make many ctc_t large simultaneously, so A−=∑tp~te−ctA^-= _t p_te^-c_t collapses toward 0 and A/A−A/A^- explodes. Numerical soundness of the min-form held on all 26,880 cells (0 violations). Consequently we do not add the extra accumulator to the kernel; Proposition 1 remains stated because it is a theorem, and applies to workloads whose residual bounds are genuinely single-spiked. Two negative results on bound selection. (i) Applying a sub-Gaussian tail bound per token and taking a union bound over the maximum is counterproductive: the resulting κ=2log(2SN/δ)≈6κ= 2 (2SN/δ)≈ 6 (with N the number of per-token events) exactly cancels the Pj P_j concentration gain (with PjP_j the attention mass of block j). (i) A Bernstein bound is dominated by its range term (linear in the residual range), which is inflated by massive-value channels; the uniform sub-Gaussian form has no such term and is strictly tighter here. Both mistakes were ours, and both were caught only by measurement. 5 Experiments Unless stated otherwise: Qwen2.5-7B [31], Mistral-7B [17] and Yi-1.5-6B [1], three domains (natural text, code, synthetic retrieval), ∼50 50 documents, 8k context, online block-wise scaling (no whole-sequence statistics), 8-bit K++V, τK=0.2 _K=0.2, τV=0.05 _V=0.05, δreq=10−2 _req=10^-2, statistics at KV-head any-of-G granularity (an unadorned δ always means δreq _req). Risk–coverage curve (main result). Table 1 reports joint K++V step coverage, single run per cell, with the deterministic tanh bound placed at δ=0δ=0. Table 1: Risk–coverage curve: joint K++V step coverage vs. request-level budget δ (single run per cell; the deterministic tanh bound is the δ=0δ=0 reference). Model Domain δ=10−4δ=10^-4 δ=10−2δ=10^-2 δ=5×10−2δ=5×10^-2 tanh (δ=0δ=0) Qwen2.5-7B natural 0.792 0.809 0.814 0.167 Qwen2.5-7B code 0.772 0.796 0.803 0.118 Qwen2.5-7B needle 0.802 0.810 0.815 0.485 Mistral-7B natural 0.792 0.793 0.793 0.520 Mistral-7B code 0.756 0.760 0.760 0.372 Mistral-7B needle 0.649 0.653 0.654 0.513 Yi-1.5-6Ba natural 0.557 0.559 0.559 0.141 Yi-1.5-6Ba code 0.539 0.544 0.545 0.121 Yi-1.5-6Ba needle 0.645 0.648 0.650 0.417 a Yi-1.5-6B is measured at 4k context because its max_position_embeddings is 4096; the other two families are at 8k. The Yi row is our only weakening cross-model result, and we report it in full. Yi’s coverage (54.4–64.8% at δ=10−2δ=10^-2) is markedly lower than Qwen’s (79.6–81.0%) and Mistral’s (65.3–79.3%). This is not explained by the shorter context: the certificate’s logS S dependence means 4k should be more favourable than 8k, so the effect is real rather than an artefact of the measurement. The relative gain still holds—page-in rate falls 39.7–48.7% against tanh, inside the 28.7–77.0% band of the other two families—and δ sensitivity is the lowest of the three (0.22–0.62 p across a 500×500× range). The third family also yields zero violations, a third independent soundness check. The headline coverage range over the nine model×domain cells is therefore 54.4–81.0% at the single working point δ=10−2δ=10^-2 (the earlier two-family range 64.9–81.5% is superseded; we do not quote a cross-δ envelope). The mechanism is not a property of the model but an interaction of block-level scaling with Yi’s diffuse channel energy; it is identified experimentally in Sec. 6.4.3 and disappears under the per-token scaling used in deployment, where Yi is in fact easier than Qwen. Reading: (a) the relative reduction in page-in rate is 28.7–77.0% and holds across all three model families and all three domains; (b) tightening δ by 500×500× costs at most 3.2 p of coverage (median 0.47 p over the nine model × domain cells)—the slope of the curve answers directly the objection that the gain is merely bought by relaxing the failure probability; (c) heterogeneity is reported honestly: the deterministic bound fares better on Mistral, and four of the nine cells exceed our 30% page-in target, all on the two weaker families (Mistral needle 34.7%; Yi 35.2–45.6% across its three domains). Certificate-formula head-to-head (global scaling, identical quantizer and outlier handling): the deterministic bound authorizes 15.14 raw bits with a 44.4% KV-head page-in rate; ours authorizes 11.71 raw bits (11.98 physical, including outliers) at 22.0%. Stated precisely: under an explicit 1%1\% request-level risk budget, the probabilistic certificate halves the page-in rate and authorizes compression 3.43 bits/dim deeper (15.14→11.7115.14→ 11.71 raw bits). The two guarantees are of different strength and we do not claim equivalence. Joint K++V (Qwen2.5-1.5B, frozen early setting). Marginals passK=89.1%pass_K=89.1\%, passV=97.1%pass_V=97.1\%; the measured joint is 86.7%86.7\%, inside the interval [86.2%,89.1%][86.2\%,89.1\%] implied by the marginals. KV-head joint page-in is 27.6%; the idealized amortized effective width is 10.39 bits, charging page-in steps at full FP16 price. Violations (scope limited). Across the first two model families (the third family adds its own zero-violation run, reported above), three domains, all δ levels, both certificates, and 200 independent dither seeds counted at request granularity (single text, 64 scattered query positions, all layers and all heads, 8-bit setting), we observed no violations; the rule-of-three 95% upper bound is 1.5%, consistent with δreq=1% _req=1\%. Soundness follows from the theorems and their assumptions; zero observed violations is validation, not proof. Real memory saving (measured, not computed). Our earlier byte account was computed. We now build the real packed store (int8 payload ++ FP16 scale ++ int16 index ++ FP16 outliers, with the dither reconstructed from Philox and therefore stored at zero cost) and measure it with torch.cuda.memory_allocated: at S=32768S=32768, d=128d=128, one KV head, the packed store occupies 4,753,4084,753,408 B versus 8,388,6088,388,608 B for FP16, a real 43.3%43.3\% saving. As a control, the “dequantize back to bf16” simulated setting measures a saving of 0.0%, confirming the red-team’s objection. The full chain (packed store → attention kernel → certificate) runs end to end: at τ=0.2τ=0.2 the coverage is 0.7920.792 and the relative output error 9.0×10−39.0\!×\!10^-3. The saving is independent of context length (43.3%43.3\% at 8k, 32k and 128k alike). Ablations appear where they are used: the outlier-pair count m (Secs. 6.3.6, 6.2.5), scale granularity (Sec. 6.2.3), and bound shape (Secs. 4.3, 6.4.2); the deterministic witness-storing variant cert_D is subsumed by Tier A. Limitations. The certificate is a per-layer, per-head local guarantee (the value-side bound is deterministic given p~ p, so the joint passK∧passVpass_K _V event consumes no additional probabilistic budget beyond the K side); the Tier-B probabilistic guarantee is stated for non-adaptive queries only (Sec. 4.2)—free-running decoding is outside the theorems, and Tier A is the adaptive-safe tier; certificate aggregation under multi-GPU / tensor parallelism is unverified; model coverage is three 6–7B-class GQA families for the risk–coverage evidence (systems experiments are Qwen-only). Limitations now lifted: “no real packed cache” is lifted by the measurement above; “PCIe traffic is a simulated bill” is lifted by Sec. 6.3.4 (real page-in loop) and Sec. 6.3.5 (block-level paging, 128×128× less traffic); “paired significance testing pending” is lifted by Sec. 6.3.3. 5.1 Long chain-of-thought workloads (model self-generated, not human-written text) A reasonable objection is that coverage was measured on human-written documents, whereas the long CoT of a reasoning model has a different attention structure (self-generated, repetitive patterns, possibly sharper distributions), so the certificate might collapse there. We generated 4 real long CoT traces with DeepSeek-R1-Distill-Qwen-7B [11] (1724–4096 tokens, 12,432 tokens in total) and measured: Table 2: Coverage on model-generated long CoT (DeepSeek-R1-Distill-Qwen-7B; n=4n=4, a no-collapse check, not a significance result). Sample Generated length Coverage (query head) Coverage (KV head) Attention entropy 0 4096 0.857 0.800 3.79 1 2617 0.857 0.800 3.66 2 1724 0.857 0.800 3.50 3 3995 0.858 0.798 3.66 Mean KV-head coverage is 0.800, on par with the 0.792 full-chain coverage of Sec. 5 on ordinary long text, and no collapse was observed; the variance across the four samples is very small. Note n=4n=4: this is a “no collapse observed” statement, not a significance result. 5.2 Long-context scaling to 128k The introduction motivates with long context, so we measure how coverage itself scales with S, on the one model that fits full-activation capture at 128k on our GPU (Qwen2.5-1.5B-Instruct; two concatenated domain streams, natural and needle; the Sec. 5 configuration at δreq=10−2 _req=10^-2; the model’s own rotary cos/sin / are hooked, so YaRN and non-YaRN runs are exactly faithful to the forward pass). Joint K++V step coverage: 63.7–64.5% at 8k, 57.3–60.0% at 32k, and 26.6–41.3% at 128k, the last under the vendor’s official YaRN [30] factor-4 long-context configuration since the native window is 32k. Two readings, both honest. (i) The reviewer-friendly prediction “coverage will hold because the radius grows as logS S” is not confirmed: the radius grows only ∼5% 5\% from 32k to 128k, yet coverage drops by up to half—the decline is a property of long-context attention statistics under YaRN, not of the certificate mathematics, and we report it as such. (i) The relative picture strengthens: the deterministic tanh reference collapses to at most 0.2% coverage at 128k, while the probabilistic certificate still authorizes 26.6–41.3% of steps. Zero violations at all three lengths (a fourth independent soundness check). On a native long-context model the decline does not reproduce (same protocol, 8times8\\ timesH200). Re-running with Llama-3.1-8B-Instruct, whose native window is 131,072 (no YaRN extrapolation of any kind), joint coverage on the needle domain is 77.0 / 77.1 / 77.0% at 8k/32k/128k and 71.7/73.8/71.4% on natural—flat in sequence length, with zero violations at every length, while the tanh reference still collapses (natural 0.399→0.1370.399→ 0.137). Read together, the two experiments localize the cause: the 128k decline above is a property of YaRN-extrapolated attention statistics (small model, extended window), not of long context per se; native long-context models show no such decline. 6 System Implementation and On-Device Results This section is organized in four parts: architecture (6.1), implementation (6.2), evaluation (6.3), and analysis (6.4). The loop being implemented is: The meter loop (one decode step, one layer, one KV head). Write path (once, at cache write): quantize k→k^k→ k with any scheme; Tier A stores the witness wt,b=‖rt,b‖w_t,b=\|r_t,b\| (32 B/tok/head); Tier B (dithered INT8) stores payload and scales only. Read path (fused into decode attention, shared data load): accumulate A=∑tp~tectA= _t p_te^c_t with ctc_t from Theorem 2 (Tier A) or the sub-Gaussian radius utu_t (Tier B); merge across KV splits under the LSE weights; meter =min(1,12(A2−1))= \! (1, 12(A^2-1) ). Gate (per (layer, head) or per request): if the meter (or, above saturation, the raw risk score) exceeds τ, page in the top-contributing blocks (6.3.5) or the whole head from the exact backing store, recompute, write back, zero the witness; otherwise serve the compressed path. Figure 2: The WitCert observatory. Any scheme’s residual leaves a witness at write time; the decode kernel computes output and meter in one fused data pass (LSE-merged across KV splits); the gate repairs at block granularity from the exact backing store and zeroes the repaired witnesses; SGLang integration is a bit-identical-when-off env-guarded patch. 6.1 Architecture The meter loop above is the design; Fig. 2 shows where it lives in a serving engine. The rest of this section is organized as implementation (6.2), evaluation (6.3) and analysis (6.4). 6.1.1 Why the meter is structurally cheap by design Scales are block wise (BLK=256BLK=256) and the tile width divides the block width, so within a tile ς2 ^2 is token independent; the certificate accumulator therefore collapses from a [BLOCK_M,BLOCK_N][BLOCK\_M,BLOCK\_N] matmul to one scalar per query times the softmax row sum. The dither PRNG is likewise shared by the BLOCK_MBLOCK\_M queries in a tile, amortizing its cost by a factor BLOCK_MBLOCK\_M. (The read side uses the same five-tuple Philox as the write side; an early version used tl.rand, was therefore not the same random stream as the write side, and was flagged as a violation by the contract test. It has been fixed.) The marginal cost of the certificate itself, measured in two places. (i) In our research-grade kernel it already falls into the noise, −1.3%-1.3\% (the latency difference between certificate on and off; see docs/active_block_policy.md). (i) Inside the SGLang 0.5.9 production decode kernel it is +11.9%+11.9\% (Sec. 6.2.2). The two are not in conflict: our kernel’s latency is dominated by dither reconstruction (77.9%77.9\% of it), so the certificate is a small quantity in its shadow, whereas the SGLang kernel has no dither reconstruction and is tightly tuned for occupancy, so one extra accumulator shows up directly as +11.9%+11.9\%. We adopt the latter as the external figure—it is the number a production system will see. 6.2 Implementation 6.2.1 Research kernels and the proof–kernel contract The write kernel implements x^=s(round(x/s+ξ)−ξ) x=s\,(round(x/s+ξ)-ξ) with the dither ξ drawn by Philox4x32-10 [33] from a five-tuple counter (request, layer, KV head, token, channel), so the random stream is invariant to batch scheduling and CUDA-graph replay and can be reconstructed exactly at read time. The scale s=amaxblk/126.5s=amax_blk/126.5 (i.e. Q−12Q- 12) guarantees strictly no clipping on non-outlier channels, which is the premise of the sub-Gaussian assumption. Two implementation facts turned out to be load bearing. First, quantization must use the stored FP16 scale: quantizing with an fp32 scale while storing FP16 breaks |ε|≤s/2| |≤ s/2 (we measured 1639 violations) and with it the sub-Gaussian assumption—a concrete case of a kernel detail deciding whether a theorem holds. Second, Triton’s uint32 multiply/broadcast semantics diverged from our reference at round two of Philox; we moved both sides to int64 with explicit masking, trading throughput for semantic certainty. The read kernel performs INT8 dequantization, Philox dither reconstruction and certificate accumulation in a single kernel, sharing one data load with attention. Acceptance (nine items, 8/9 complete). Elementwise agreement between the CPU reference and the GPU kernel (int8 disagreement 1/262,1441/262,144, asserted to fall on a 0.5 rounding tie, where both rounding directions satisfy |err|≤s/2|err|≤ s/2; attention output max|Δo|=2.9×10−6 | o|=2.9\!×\!10^-6, certificate max|Δ|=8.9×10−8 | |=8.9\!×\!10^-8); five-tuple stream uniqueness; CUDA-graph replay bit identical to eager execution with five interleaved replays agreeing exactly (the seed is unaffected by scheduling), and a certificate produced at every graph-captured decode step—this closes the gap left by a Python-level probe, which CUDA graph rejects precisely because of its host synchronization; zero clipping on non-outlier channels; measured kernel error fed directly to the certificate with zero violations; the physical byte account exact to the byte; overhead reported as three separate items; and the quad report. The tiled kernel is covered by a separate contract test (Δo=9.8×10−6 o=9.8\!×\!10^-6, Δcert=6.0×10−7 =6.0\!×\!10^-7, zero violations). Not complete: production-grade kernel optimization (warp specialization, asynchronous prefetch). 6.2.2 The SGLang decode kernel The kernels above are all our own research-grade implementations. To answer “can the certificate go into a real inference engine”, we added the certificate accumulator to the Triton decode attention of SGLang 0.5.9 [45] (the grouped two-stage kernel of decode_attention.py), a 500-line diff, in integration/witcert_sglang.patch. Key structure: the certificate shares the split-KV reduction with the output. SGLang uses a flash-decoding-style [9] two-stage structure (descended from FlashAttention [8]): stage 1 emits per-split local (acc/esum,lse)(acc/e_sum,lse), and stage 2 merges them with LSE weights. But the certificate A=∑tp~teutA= _t p_te^u_t is itself a softmax-weighted average, so the per-split As=∑t∈sp~teut/esum,sA_s= _t∈ s p_te^u_t/e_sum,s, merged under the same LSE weights, yields exactly the global A—no extra synchronization, no second scan. This is not a coincidence: the certificate and the attention output are both linear functionals of p~ p. To be compatible with token-granularity paging, this integration uses one scalar scale per token (rather than the per-block, per-channel scale of the main text). The certificate formula is unchanged, and since ut=αhstu_t= _h\,s_t is linear in the token scale sts_t (with αh _h a per-(query, head) constant), the square root can be hoisted out of the loop entirely. Table 3: Acceptance of the SGLang decode-kernel integration. Acceptance item Result Certificate off vs upstream kernel bit identical (max|Δ|=0 | |=0) ⇒ zero intrusion Certificate vs torch reference (shuffled paged slots, 8-way split) max relative error 5.06×−5.06\!×\!10^-6 Overhead +11.9%+11.9\% Attributing the overhead (discriminative experiment). Keeping the accumulator but removing the scale load and the exponential still costs +11.77%+11.77\%; inlining the scale into the K row (saving one memory transaction) reduces it by only 0.6%; and aligning quantization blocks to pages so that u is constant within a tile (reducing the number of exponentials from BLOCK_H×BLOCK_NBLOCK\_H×BLOCK\_N to BLOCK_HBLOCK\_H) yields no gain. So this 11.9% is almost entirely the register/occupancy cost of “one more accumulator”, and has nothing to do with the certificate’s arithmetic. This does not contradict the noise-level (−1.3%-1.3\%) certificate cost of our own kernel in Sec. 6.1.1: that kernel’s latency is dominated by dither reconstruction (77.9% of it), whereas the SGLang kernel has no dither reconstruction and is tightly tuned for occupancy, so any new accumulator shows up immediately. The external figure should be +11.9%+11.9\%—that is the number a production system will see. At this stage only certificate computation is integrated; storage is the subject of the next subsection. 6.2.3 Storage side: a paging-compatible certified KV cache Computing the certificate is not enough: its soundness requires subtractive dithering, and SGLang’s existing fp8 KV cache uses deterministic rounding, which violates the theorem’s hypothesis. This is exactly what the proof–kernel contract is for—one cannot bolt a certificate onto a kernel that does not produce the assumed error distribution. A certified deployment must therefore bring its own storage. The scale granularity has to be re-chosen. The body of this paper uses per-256-token-block, per-channel scales. SGLang’s pool is paged at token-slot granularity (in the PagedAttention style [20]): slots are assigned arbitrarily by the allocator, consecutive tokens of a request need not be contiguous, and during decoding a page fills incrementally, so when token t is written the later tokens do not exist and no block amax can be computed. We therefore scale per token, per group of GcG_c channels—a granularity that depends only on the current token and is fully decoupled from slot assignment. On Qwen2.5-7B real activations (8k, 8-bit K++V, no outlier bypass): Table 4: Scale granularity on real activations (Qwen2.5-7B, 8k, 8-bit K++V, no bypass; real-V output error; single run). Scheme Rel. output error vs. ours K++V B/tok/head Saved Paging-safe block × channel (paper body) 2.449×10−22.449\!×\!10^-2 1.00×1.00× 258 49.6% no token × 16-channel groups 1.821×−1.821\!×\!10^-2 0.74×0.74× 288 43.8% yes token × 32-channel groups 2.131×10−22.131\!×\!10^-2 0.87×0.87× 272 46.9% yes token scalar 3.720×10−23.720\!×\!10^-2 1.52×1.52× 260 49.2% yes This is not a compromise—it is more accurate. Per-token scaling tracks the very-large-magnitude tokens (the massive-activation effect discussed above), which a 256-token block scale smooths away. Paging-safety and quality point the same direction here. We take Gc=32G_c=32 as the default. The dither counter uses the slot, not the sequence position. The Philox five-tuple is (layer, kv_head, slot, channel). Slots are stable in the cache—paging, prefix sharing and retraction never change the contents of a written slot, so the read side can always reconstruct the dither ξ used at write time; sequence positions are not stable (under prefix sharing the same token appears at different positions in different requests). Validation (RTX 4090, S=4096S=4096, batch 2, 28 query / 4 KV heads, 8-way split): Triton dither vs. the torch reference is bit-identical; residuals satisfy |err|≤s/2|err|≤ s/2 with zero violations (max ratio 1.0000); in-kernel dequantisation matches the reference to 6.43×10−46.43\!×\!10^-4 (the fp16 baseline itself is 2.17×10−42.17\!×\!10^-4); the in-kernel certificate matches to 4.59×10−44.59\!×\!10^-4; soundness holds with 0/56 violations (true TV 10−310^-3–10−210^-2 against certificates 0.119–0.170, median tightness 22.2×22.2×); coverage at τ=0.2τ=0.2 is 1.000; end-to-end quality cost 1.62×10−21.62\!×\!10^-2; latency fp16 → quantised 5.47×5.47× → quantised++certificate 5.49×5.49×; measured memory 136 B/tok/head per side (K++V total 272 B, matching the Gc=32G_c=32 row of Table 4), 46.9% saved. Structural finding: the certificate’s marginal cost collapses once storage is quantised. The same certificate costs +11.9% on the fp16 storage path but only +0.35% on the quantised path, because ςh,t2=(sm_scale2/12)∑cqh,c2sc,t2 ^2_h,t=(sm\_scale^2/12) _cq_h,c^2\,s_c,t^2 is exactly one [BLOCK_H,d]×[d,BLOCK_N][BLOCK\_H,d]×[d,BLOCK\_N] tl.dot whose s was already loaded for dequantisation—the certificate rides along with zero extra memory traffic. This resolves the apparent tension with the “nearly free” claim earlier: the +11.9% was measured on a kernel that needs no scales at all. The certificate’s cost should not be priced separately; it and the quantisation are two uses of the same load. 6.2.4 End-to-end in the serving process Source patching is required; monkeypatching does not work. SGLang’s scheduler runs in a spawned subprocess, so parent-process patches never reach it (the subprocess simply exits with EOFError). Our patch is 327 lines across three sites (integration/witcert_sglang_serving.patch), all guarded by an environment variable so that the disabled path is bit-identical to upstream: the pool constructor, get_cell_size_per_token, and forward_decode. The middle site is easy to miss, and missing it zeroes the benefit. Our first version changed only the pool and the backend; KV capacity did not move, because SGLang still sized it from kv_cache_dtype and the saved memory sat idle. Byte savings become serving capacity only if the scheduler is told about them. 6.2.5 Fixed-channel outlier bypass: two steps that must both be taken The body of the paper selects m outlier RoPE pairs per block. Under token-granular paging there are no blocks, but measurement shows a per-(layer, kv-head) fixed channel set suffices: the massive-activation RoPE pairs are highly stable across tokens—the top-8 pairs chosen from the first half of a sequence match those from the second half with Jaccard 0.940 (Qwen2.5-7B) and 0.880 (Yi-1.5-6B), minimum 0.750 / 0.500. A fixed set removes the need for per-token indices: only the 2m2m fp16 values are stored (16 B at m=4m=4). Bypassing alone is not enough—the bypassed channels must also be excluded from the group amax. Otherwise the other 31 channels of the group still pay for the very large channel that is already bypassed, the scale does not drop, and the certificate barely improves. A controlled experiment (4 injected massive RoPE pairs): Table 5: Bypass alone is not enough: the bypassed channels must also leave the group amax (controlled experiment, 4 injected massive RoPE pairs). Treatment Median meter Max meter Coverage (τ=0.2τ=0.2) No bypass 1.0311 2.378 0.000 Bypass, amax unchanged 0.9608 2.177 (−8%-8\%) 0.000 Bypass + excluded from amax 0.0620 0.0731 (32×32× lower) 1.000 Coverage-versus-budget on real activations (S=4096S=4096, τ=0.2τ=0.2, amax exclusion applied): Table 6: Coverage vs. outlier budget on real activations (S=4096S=4096, τ=0.2τ=0.2, amax exclusion applied; single run). m Qwen2.5-7B Yi-1.5-6B B/tok/head Saved 0 0.525 0.907 136 46.9% 2 0.818 0.999 144 43.8% 4 0.843 1.000 152 40.6% 8 0.929 1.000 168 34.4% 16 0.980 1.000 200 21.9% Prefix reuse (radix cache) is supported. The extend/prefill kernel received the same in-kernel dequantisation treatment (155-line diff): bit-identical to upstream when disabled, and matching a “dequantise then run upstream” reference to 9.34×10−69.34\!×\!10^-6 when enabled. Across requests sharing a long prefix, outputs track the fp16 baseline closely (2 of 4 answers bit-identical, the rest semantically equivalent). The write path must also be a kernel. Our first working version reached only 63.7 tok/s because quantisation on write was still in torch: ten rounds of int64 Philox tensor ops, inside a 28-layer per-step loop, generate a great many kernel launches. Moving it to Triton (bit-identical to the torch reference, 82×82× faster per call) raised this to 575.9 (single development-milestone run; the final median-of-3 figure is Table 17’s 511.8). Offline validation of the read path alone misses this bottleneck entirely. Certificate telemetry in production. Each decode step emits certificates, aggregated on the GPU and flushed by sampling. One full-sample run (1.5B, no bypass, request-level allocation): 249,312 (layer, query-head) certificates, coverage 81.2% at τ=0.2τ=0.2, with a few heads far above threshold (massive activation). An operator therefore learns directly that 18.8% of (layer, head, step) triples carry no guarantee at the current threshold—the deployed form of the runtime observability layer proposed in the introduction. The telemetry itself has three traps we hit in practice (single diagnostic measurements, used for localisation rather than quantification): a per-layer .item() sync dropped throughput from ∼560 560 to 409.9; a .float().contiguous() copy of the whole scale buffer inside the certificate branch brought it to 423.7; and even with both fixed, per-layer reductions still cost enough that we moved to sampling (stride 32). With those fixed, an isolated measurement puts the telemetry at 287.6 (off) vs. 284.1 (on) on 7B—1.2%, meaning the 6.4%/16.2% certificate cost above is essentially all kernel, not telemetry. Observation code can easily cost more than what it observes and must be an order of magnitude cheaper than what it measures. When the certificate overflows fp32 its value is +∞+∞. This is still sound—infinity is a valid upper bound, meaning “no guarantee for this head”—and is counted as over-threshold; means and maxima are taken over finite values only and the overflow fraction is reported separately. Boundary (stated plainly). Covered: both the decode and extend/prefill paths, page_size 1 and 16, model scales 1.5B and 7B, radix cache on and off. Not covered: the FlashInfer [43] backend (this is a Triton-side contribution; FlashInfer is a separate CUDA kernel family needing its own implementation); multi-GPU / tensor parallelism is unverified. 6.3 Evaluation 6.3.1 Quad report and same-framework comparison (S=32768S=32768, nq=24n_q=24, τ=0.2τ=0.2, δreq=10−2 _req=10^-2; synthetic K) Table 7 compares four methods on four axes. Table 7: Quad report, synthetic K, single run (S=32768S=32768, nq=24n_q=24, τ=0.2τ=0.2). RTN-INT8a is the base form of KVQuant/KIVI. Method Cert. coverage Fallback Latency B/tok/head Rel. output error fp16 — — 1.593 ms (1.00×1.00×) 256 2.7×10−42.7\!×\!10^-4 RTN-INT8a none — 1.575 ms (0.99×0.99×) 129 (−49.6%-49.6\%) 8.5×10−38.5\!×\!10^-3 RTN-INT4 none — 1.508 ms (0.95×0.95×) 65 (−74.6%-74.6\%) 1.6×10−11.6\!×\!10^-1 WitCert-INT8 79.2% 75% (any-of-6) 8.627 ms (5.41×5.41×) 145.1 (−43.3%-43.3\%) 9.0×−9.0\!×\!10^-3 Three readings. (a) No measurable quality cost from the certificate: WitCert and RTN-INT8 are at the same error level (9.0×10−39.0\!×\!10^-3 vs 8.5×10−38.5\!×\!10^-3), and the extra memory is the 16.116.1 B/tok/head FP16 outlier bypass (+12.5%+12.5\% over the 129129 B of RTN-INT8, +6.3%+6.3\% over the 256256 B FP16 key), bought in exchange for a runtime TV upper bound. (b) The 5.41×5.41× latency comes from the contract-compliant dequantization path (two non-exclusive ablation deltas: Philox 77.9%77.9\%, IEEE precision 30.4%30.4\%; already improved 2.7×2.7× by four-output reuse, with a further 1.48×1.48× available from a TF32 knob), while the marginal cost of the certificate itself is within the noise (−1.3%-1.3\%); the near-zero overhead of the RTN path shows that memory traffic is already saturated and the dither PRNG is pure added compute, so the path to production is clear. (c) RTN-INT4 saves 74.6%74.6\% but incurs an error of 1.6×10−11.6\!×\!10^-1 (∼19× 19× worse than RTN-INT8) while the system remains entirely unaware—which is exactly the risk visibility WitCert can supply to any compression scheme. 6.3.2 Quad report on real activations, and 32k (replacing synthetic K) The quad report of Sec. 6.3.1 uses synthetic (random Gaussian) K; this section redoes the same measurement on post-RoPE K activations of Qwen2.5-7B over real documents in three domains (every fourth layer, all GQA query heads). S=8192S=8192, 7 documents across three domains, τ=0.2τ=0.2, δreq=10−2 _req=10^-2: Table 8: Quad report on real Qwen2.5-7B activations (S=8192S=8192; error column is the K-side proxy; single run). Method Cert. coverage Fallback (any-of-6) B/tok/head Rel. output error fp16 — — 256.0 — RTN-INT8 none — 129.0 (−49.6%-49.6\%) 4.27×10−24.27\!×\!10^-2 RTN-INT4 none — 65.0 (−74.6%-74.6\%) 4.64×10−14.64\!×\!10^-1 WitCert-INT8 80.6% 23.0% 145.1 (−43.3%-43.3\%) 2.38×−2.38\!×\!10^-2 The fallback column is measured any-of-6 (the harness groups six query heads per KV head), not inferred from per-head coverage: on synthetic K the per-head exceedances are nearly independent (75%≈1−0.792675\%≈ 1-0.792^6, the quad report), whereas on real activations they are strongly correlated within a KV group (23.0%≪1−0.8066=72.6%23.0\% 1-0.806^6=72.6\%)—correlation that itself reflects the channel-concentrated structure of real keys. Dither is quality neutral (2×22× 2 ablation). Measured with real V on real attention output (quantizer × outlier, Qwen2.5-7B, 8k, 7 documents across three domains, 8-bit K++V); an earlier “1.71.7–1.8×1.8× better than RTN” claim rested on a K-side proxy and is retracted (Appendix B): Table 9: 2×22× 2 ablation with real V: dither is quality neutral; the quality gain belongs to the outlier bypass. Configuration Rel. output error K++V B/tok/head RTN 2.751×10−22.751\!×\!10^-2 258.0 RTN ++ outlier 1.995×10−21.995\!×\!10^-2 290.1 dither 2.717×10−22.717\!×\!10^-2 258.0 dither ++ outlier 1.951×10−21.951\!×\!10^-2 290.1 In this ablation both K and V carry outlier pairs (hence 290.1 B/tok/head), unlike the RULER configuration where only K does. Decomposition: the gain from dither itself is only 1.01×1.01×, i.e. quality neutral; the entire 1.38×1.38× gain comes from the outlier bypass, at a cost of +12.4%+12.4\% memory. So the correct conclusion is not “guarantee and quality move together”, but rather: subtractive dither is quality neutral relative to same-bit-width RTN, and it is a necessary condition for the probabilistic certificate ⇒ the probabilistic certificate is obtained at zero accuracy cost; the quality gain comes from the outlier bypass, is unrelated to the certificate, and is an independently selectable knob. This conclusion is weaker than the original, but defensible. The 32k long-context setting (same configuration, 4 documents across three domains): Table 10: The 32k long-context setting (same configuration as Table 8; K-side proxy error). Method Cert. coverage Fallback B/tok/head Rel. output error RTN-INT8 none — 129.0 (−49.6%-49.6\%) 3.93×10−23.93\!×\!10^-2 RTN-INT4 none — 65.0 (−74.6%-74.6\%) 4.33×10−14.33\!×\!10^-1 WitCert-INT8 79.3% 24.5% 145.1 (−43.3%-43.3\%) 2.31×−2.31\!×\!10^-2 From 8k to 32k (4×4× the context), coverage moves 80.6%→79.3%80.6\%→ 79.3\% and fallback 23.0%→24.5%23.0\%→ 24.5\%—under native RoPE up to 32k, long-context degradation is very slow, a structural advantage of the probabilistic certificate over deterministic bounds whose max -type structure worsens as S grows. (This observation must not be extrapolated: the 128k YaRN measurement of Sec. 5.2 shows the decline steepens beyond the native window for activation-statistical reasons, even though the radius itself grows only ∼5% 5\%.) Note: as in Sec. 6.3.1, the “relative output error” column of Tables 8 and 10 is a K-side proxy (y=p(K)⋅Ky=p(K)· K) and is only meaningful for within-table comparison. Do not use it to compute “how many times lower WitCert is than RTN”—that is exactly the scope error retracted above. The real attention-output error is given by the 2×22× 2 ablation (dither is quality neutral, 1.01×1.01×). 6.3.3 End-to-end benchmark comparison (RULER-4k, Qwen2.5-7B, 1300 samples) The quad report measures four kernel-level axes; this section answers “on a real model and a real task, what happens to quality?” Each method is evaluated at its own customary budget, stated in its own units (bytes for quantization, tokens for eviction; the two are not directly comparable—see note b), and we compare against production-grade press implementations (NVIDIA kvpress [29]; SnapKV [24], KnormPress [13]); results are in Table 11. Table 11: RULER-4k, Qwen2.5-7B, 1300 samples, single run. Budgets are stated in each method’s own unit (bytes vs. tokens) and are not comparable across rows; see notes a/b in the text. Method Budget cut (unit) Mean Needle class qa_1 / qa_2 Guar. Full FP16 0% 94.30 all green 88.24 / 52.22 — WitCert quant. configa bytes 46.5% 94.42 all green 90.20 / 52.22 noa Expected Attentionb tokens 40.1% 93.88 all green 85.29 / 48.89 no Expected Attention tokens 25% 94.09 all green 86.27 / 50.00 no SnapKV tokens 25% 55.02 collapse (1.1–65) 89.22 / 48.89 no KnormPress tokens 25% 39.14 collapse 63.73 / 28.89 no The WitCert row uses the deployment-grade quantization configuration (online block-wise scaling ++ in-block outlier pairs, 8-bit K/V); Expected Attention [12] (EA) is the strongest method on the kvpress leaderboard. Per task, EA at its 40.1% token budget loses −2.95-2.95 on qa_1, −3.33-3.33 on qa_2 and −0.92-0.92 on niah_single_2 relative to full FP16 (mean −0.42-0.42), with all remaining needle tasks green (multikey_3 changes by 0.000.00). a Scope clarification. This table measures “the task quality of simulated dither-INT8 plus outlier quantization”; it is not a certified-deployment result. The press used for evaluation applies 8 bits uniformly to all layers, does not read the certificate’s per-layer table, does not use a packed cache, computes no online certificate and performs no fallback; tensors are dequantized back to floating point, so the real runtime memory saving is zero. The byte account is K 145.1 B ++ V 129 B == 274.1 B versus 512 B for FP16, i.e. 46.5%. (An earlier figure of 48.1% came from converting the key-side profile alone and has been corrected.) b The two budget columns are not the same quantity and must not be juxtaposed as “same budget”. WitCert’s 46.5% is a byte budget (quantization; the token count is unchanged), whereas Expected Attention drops tokens: its configuration compression_ratio=0.401 means discarding 40.1% of the tokens. Labelling the EA row as 46.5% too has no basis, and we have restored its true budget. Because the two budgets have different units, this table may only be read as “the quality each method attains at its own customary budget setting”, never as a strict same-budget comparison. Paired significance test. Using per-sample predictions (predictions.csv, 1089 paired samples after deduplication by (task, question)), we ran a paired bootstrap (10410^4 resamples) and McNemar’s test between WitCert and EA: the two methods give the same verdict on 99.4% of samples (McNemar: 5 vs 1), and the 95% CI of the difference is [+0.00,+0.83][+0.00,+0.83] with p≈0.12p≈ 0.12—not significant. Scorer scope (important). That test used our own independently implemented strict-prefix string_match, under which the absolute scores are 59.32% (WitCert) vs 58.95% (EA), which are not comparable in absolute value to the 94.42 / 93.88 produced by the official kvpress scorer (the two scorers differ in strictness). What is tested is the paired difference on the same set of predictions, so the “not significant” conclusion applies equally to the +0.53+0.53 of Table 11; but the reader should not conflate 59.32/58.95 with 94.42/93.88. Hence the apparent +0.53+0.53 lead cannot be claimed as a statistically significant quality advantage; the correct statement is “no quality degradation observed, and the difference from the strongest baseline is within noise”. This does not weaken our thesis—our thesis is the runtime guarantee, not a quality lead. Reading: (a) the WitCert quantization configuration maintains quality at a 46.5% byte budget (94.42 vs 94.30 for full FP16, no degradation observed), while the strongest baseline EA scores 93.88 at its own 40.1% token budget (a gap of +0.53+0.53 from unrounded scores—the rounded table entries differ by 0.54—not significant, and on a different budget basis; see note b); (b) SnapKV and KnormPress collapse silently under the query-agnostic protocol—direct evidence for this paper’s motivation: when compression fails, the system emits no signal; (c) these are single runs (limited statistical power), and maintained quality is not lossless quality (INT8 is inherently lossy). Cross-task robustness: LongBench-E with length buckets. RULER is dominated by synthetic retrieval, so we also run LongBench-E [3], whose length buckets (0–4k / 4–8k / 8k+) expose how quality moves with context length. Protocol matches the RULER setting above (Qwen2.5-7B, full split). Budget, verified by re-running. On the WitCert side both K and V are 8-bit block-dithered with FP16 outlier pairs on K: K 145.1 B ++ V 129 B == 274.1 B against FP16’s 512 B, i.e. 46.5% saved; EA’s compression_ratio=0.401=0.401 drops 40.1% of tokens. The units differ (see the earlier note), so no “tighter/looser budget” claim is made in either direction; we simply state both configurations. (Verification: re-running hotpotqa_e with the current press reproduces 59.92/58.25/51.6359.92/58.25/51.63 bit-for-bit, confirming the archived results came from the K++V version rather than an earlier key-only configuration.) Results are in Table 12. Table 12: LongBench-E by length bucket (Qwen2.5-7B, full split, single run). ΔW _W/ΔEA _EA are vs. the uncompressed column; budgets as in the text. Task Bucket Uncompr. WitCert ΔW _W EA ΔEA _EA 2wikimqa_e 0–4k 51.89 51.08 −0.81-0.81 48.51 −3.38-3.38 2wikimqa_e 4–8k 50.35 47.12 −3.23-3.23 42.56 −7.79-7.79 2wikimqa_e 8k+ 30.50 30.16 −0.34-0.34 28.92 −1.58-1.58 gov_report_e 0–4k 35.13 34.98 −0.15-0.15 35.19 +0.06+0.06 gov_report_e 4–8k 34.93 34.68 −0.25-0.25 34.98 +0.05+0.05 gov_report_e 8k+ 33.01 33.09 +0.08+0.08 34.11 +1.10+1.10 hotpotqa_e 0–4k 58.71 59.92 +1.21+1.21 58.56 −0.15-0.15 hotpotqa_e 4–8k 58.15 58.25 +0.10+0.10 56.53 −1.62-1.62 hotpotqa_e 8k+ 51.00 51.63 +0.63+0.63 55.36 +4.36+4.36 multifieldqa_en_e 0–4k 56.20 55.88 −0.32-0.32 56.49 +0.29+0.29 multifieldqa_en_e 4–8k 45.04 44.98 −0.06-0.06 46.00 +0.96+0.96 multifieldqa_en_e 8k+ 48.71 48.66 −0.05-0.05 49.79 +1.08+1.08 passage_retr_en_e 0–4k 99.00 99.00 +0.00+0.00 99.00 +0.00+0.00 passage_retr_en_e 4–8k 99.67 100.00 +0.33+0.33 100.00 +0.33+0.33 passage_retr_en_e 8k+ 100.00 100.00 +0.00+0.00 100.00 +0.00+0.00 Reading: (a) 14 of 15 buckets hold quality (|Δ|≤1.3| |≤ 1.3); the one material drop is 2wikimqa_e at 4–8k (−3.23-3.23), where EA drops −7.79-7.79, 2.4×2.4× ours. (b) Counting buckets losing more than 1 p: WitCert 1/15 versus EA 4/15, consistent with the RULER finding that quantisation degrades more uniformly than token dropping. (c) Two buckets favour the baseline and we report them: EA gains +4.36+4.36 on hotpotqa_e 8k+ and +1.10+1.10 on gov_report_e 8k+, clearly better than ours—dropping tokens helps there, plausibly by removing distracting context; these are not noise-level differences. (d) One task is missing: all three lcc_e runs failed, so this is 5 tasks rather than the 6 planned. Boundary: single run; the two budget columns are different units; five tasks do not establish general cross-task robustness. The defensible statement is that no systematic degradation appears over these 5 tasks and 15 length buckets, and that degradation is more uniform than the strongest baseline at its own customary budget. 6.3.4 The closed loop at head granularity (S=32768S=32768, 8 heads, 32 steps) A certificate that only raises an alarm without driving an action is still after-the-fact prayer. Here we close the loop: when the certificate exceeds τ, that KV head is paged back in from an FP16 backup on the CPU side and recomputed exactly. Table 13: The certify–fallback closed loop (S=32768S=32768, 8 heads, 32 steps; single run). Quantity Value GPU packed / fp16 36.27 MiB / 64.00 MiB Fallback rate (any-of-G) 27.3% Fast-path error 8.06×10−38.06\!×\!10^-3 Fallback cases: before → after 9.18×−→3.32×−9.18\!×\!10^-3→ 3.32\!×\!10^-4 (27.6×27.6× reduction) Gated effective width 10.96 bits/dim ⇒ net saving 31.5% The key reading: the fallback fires where it should. If the certificate were uncorrelated with the true error, the 27.3% of cases it selects would not have a markedly higher error than average, and the error would not drop 27.6×27.6× after fallback. This is direct experimental evidence that the certificate is discriminative, not merely sound—soundness guarantees no missed detection, discriminative power guarantees no vacuous alarms. The price is that the effective width rises from 8 to 10.96 bits, so the externally defensible claim is a net saving of 31.5%, not 43.3%. 6.3.5 Block-level paging: two orders of magnitude off the fallback cost The paging in Sec. 6.3.4 is at whole-KV-head granularity (17.5 MB per step). But the certificate is block decomposable: with A=∑tp~teutA= _t p_te^u_t, replacing block j by its exact values reduces A by exactly massj(euj−1)mass_j\,(e^u_j-1), where uju_j is the block’s shared radius. One can therefore page in blocks in decreasing order of their contribution to the excess, recomputing A after each, until the value falls back below τ. Measured over the 9 fallback cases among 32 steps (S=32768S=32768, nb=128n_b=128 blocks): the median case needs only 1 block paged in to fall below τ. Paging traffic drops from 72.0 MB to 0.5625 MB, a reduction of 128×128×. This turns fallback from “recompute the whole head” into “page in a few named pages”, bringing the worst-case latency of a certified deployment under control. 6.3.6 Design space: a branch rejected by data, and a zero-fallback operating point (a) The stochastic-rounding branch is rejected. The proof–kernel contract requires the kernel to produce the error distribution assumed by the theorem. Subtractive dither requires PRNG reconstruction on the read side (77.9% of the kernel), so the natural question is whether stochastic rounding (SR) could be used instead—it is equally unbiased and needs no random numbers on the read side. We implemented and measured it: SR’s certificate coverage is identically 0.000 at every outlier budget. The reason is that the sub-Gaussian proxy of the SR residual is 3 3 times larger than that of uniform dither, and the proxy enters the certificate inside an exponential, so exponential amplification overwhelms a linear difference in variance. Table 14: Stochastic rounding is rejected by data: its certificate coverage is identically zero at every outlier budget (offline harness, synthetic K). m (outlier pairs) B/tok/head Saving Cov. (dither) Cov. (SR) Error (dither / SR) 4 145.1 43.3% 0.762 0.000 8.02×10−38.02\!×\!10^-3 / 1.17×10−21.17\!×\!10^-2 8 161.1 37.1% 0.926 0.000 7.81×10−37.81\!×\!10^-3 / 1.10×10−21.10\!×\!10^-2 16 193.3 24.5% 1.000 0.000 7.03×10−37.03\!×\!10^-3 / 1.02×10−21.02\!×\!10^-2 (The m=4m=4 dither coverage here, 0.762, differs from the 0.792 of Table 15 because Table 14 is the offline harness on synthetic K and Table 15 the on-device kernel; settings are otherwise identical, and the two harnesses’ index layouts differ in the last digit of the byte account—161.1 vs 161.2 at m=8m=8.) This negative result carries a meaning beyond implementation: it shows that unbiasedness alone does not support a certificate—the constant in the proxy is what matters. It also explains why our kernel overhead cannot be tuned away: the PRNG cost is algorithmic, not an implementation defect (parameter tuning left only a 1.7% margin in measurement). (b) A zero-fallback operating point. Table 14 also reveals a setting we had not anticipated: at m=16m=16 coverage reaches 1.000, i.e. the certificate never exceeds the threshold, so the entire fallback machinery (CPU backup, paging, recomputation) becomes unnecessary. The on-device kernel reproduces this point: Table 15: On-device outlier-budget sweep (synthetic K; a separate run from the quad report). m B/tok/head Saving Coverage Cert. median Cert. max Latency Fallback needed 4 145.1 43.3% 0.792 0.1883 0.2126 8.80 ms yes 8 161.2 37.0% 0.958 0.1783 0.2014 9.88 ms yes (4.2%) 16 193.3 24.5% 1.000 0.1596 0.1804 11.71 ms no (This sweep is a separate run from the quad report, whence the m=4m=4 latency reads 8.80 ms there and 8.627 ms here.) The price is that the compression ratio falls from 43.3% to 24.5%; the reward is that deployment complexity collapses to “quantization plus one read-only risk indicator”, with no tiered cache. This is the simplest form of the “DTrace-style observability layer” proposed in Sec. 1. But the margin at the zero-fallback point differs greatly between the two kinds of data, and the two must be stated separately. Table 15 uses synthetic Gaussian K, where the m=16m=16 certificate maximum of 0.1804 leaves only a 1.11×1.11× margin to τ=0.2τ=0.2—an operating point that hugs the threshold, and would lose the zero-fallback property under a slight change of distribution. On real Qwen2.5-7B activations, by contrast, Sec. 6.3.7 measures a maximum of 0.086, a 2.3×2.3× margin. The direction of the difference is as expected: synthetic Gaussian K has uniform channel energy, so the outlier bypass can rescue only a small fraction, whereas real activations concentrate heavily in a few channels that m=16m=16 happens to cover. Conclusion: the zero-fallback point is robust on real models and marginal in the synthetic worst case; a production deployment should profile the real distribution before choosing m, rather than copying 16. 6.3.7 End-to-end validation: the meter inside a real generation loop All the experiments above are of the form “capture activations offline, then compute errors”. To rule out the optimistic bias of that form itself, we wired the packed store, the active-block tail policy and the write-path kernel into the HuggingFace Cache interface and ran real autoregressive generation on Qwen2.5-7B (all 28 layers active, prefill 2048 ++ decode 32), computing the certificate from the real query vectors captured by a hook (after RoPE)—rather than using K as a proxy for the query. Quality is measured by teacher forcing: we feed the baseline’s own token sequence and compare logits step by step. Free greedy decoding is unsuitable as a quality metric—once any step diverges the trajectories separate permanently, so a “text agreement rate” reflects chaos rather than compression quality (we measured free greedy diverging at step 1, whereas under teacher forcing the top-1 agreement rate is 93.8%). Table 16: Real autoregressive generation via the HF Cache interface: teacher-forced quality, certificates from real hooked queries. m top-1 top-5 KL(base∥ours)KL(base\,\|\,ours) saving Coverage (real q) Max meter 4 0.938 0.925 2.31×10−22.31\!×\!10^-2 42.7% 0.867 1.6×1021.6\!×\!10^2 8 0.969 0.956 7.51×10−37.51\!×\!10^-3 36.5% 0.949 4.7 16 0.938 0.981 4.16×−4.16\!×\!10^-3 24.1% 1.000 0.086 Three observations. 1. The zero-fallback setting holds in real generation. (Packed savings here run ∼0.5 0.5 p below the on-device table—42.7 vs. 43.3%—because this harness holds the active-block tail in fp16.) At m=16m=16, all 196 (layer, query head) samples—one GQA group of 7 query heads per layer, 28 layers—have certificates ≤τ=0.2≤τ=0.2, with a maximum of 0.086, still 2.3×2.3× below the threshold. This is the third independent piece of evidence for that operating point (offline, on-device kernel, real decoding), and the three agree. 2. The certificate correctly identifies “massive activation” heads. At m=4m=4 the maximum certificate value reaches 1.6×1021.6\!×\!10^2—a few attention heads have channels of extreme magnitude (massive activations / attention sinks [36, 40]), and their quantization error is amplified exponentially by softmax. The certificate does not hide this; it exposes it explicitly as a threshold violation, which is precisely its design intent. As m grows (bypassing those channels in FP16), the maximum collapses monotonically: 1.6×102→4.7→0.0861.6\!×\!10^2→ 4.7→ 0.086. 3. KL improves monotonically while top-1 agreement does not (0.938/0.969/0.9380.938/0.969/0.938): the latter is noise at n=32n=32; KL and top-5 overlap are the metrics with power, and both improve monotonically with m. Boundary (stated honestly). The read path of this harness goes “dequantize → standard attention” (the HF Cache interface requires returning FP16 tensors), so the fused kernel is not inside this loop and its correctness rests on the independent contract tests; moreover the dequantized result of a full block is cached, so this experiment does not constitute independent evidence of runtime memory saving—that is supplied by the torch.cuda.memory_allocated measurement in Sec. 5. 6.3.8 Serving end to end Results are in Table 17 (capacity and throughput: median of 3 runs per cell—a single measurement is easily fooled by run-to-run noise: our first reading suggested the certificate was free in production, and repeating it showed that was noise). Table 17: SGLang serving end to end (RTX 4090, batch 16 × 64 tokens, page_size=16=16; capacity/throughput are medians of 3 runs, coverage is a full-sample single run under the request-level δ allocation). Model Configuration KV capacity Tok/s Coverage (τ=0.2τ=0.2) 1.5B fp16 650,368 686.8 — 1.5B WitCert int8 1,224,240 (1.88×1.88×) 511.8 (0.75×0.75×) 0.812 1.5B + outlier bypass m=4m=4 1,095,360 (1.68×1.68×) 436.1 (0.64×0.64×) 0.940 7B fp16 114,128 421.7 — 7B WitCert int8 214,832 (1.88×1.88×) 347.8 (0.82×0.82×) 0.753 7B + outlier bypass m=4m=4 192,224 (1.68×1.68×) 311.5 (0.74×0.74×) 0.946 Coverage is reported under the request-level allocation δloc=δreq/(L⋅H⋅T) _loc= _req/(L· H· T) with T=256T=256, δreq=10−2 _req=10^-2 (full-sample telemetry, single run). An earlier implementation allocated only over tokens and the current batch (log(2Snq/δ) (2S\,n_q/δ)), without amortizing layers and steps; those figures—up to 5 p higher on 1.5B—could only be called local-certificate coverage and are retired (Appendix B). Capacity and throughput are unaffected (the allocation only changes a scalar constant). (a) 1.88×1.88× more KV tokens at the same memory budget (1.68×1.68× with the bypass), identical at both scales. (b) Quantisation alone costs 0.75–0.82×0.82× in throughput, far better than the 5.5×5.5× seen at kernel level; kernel-level ratios such as the 5.41×5.41× reported earlier badly overstate deployment cost (Appendix B). (c) The outlier bypass lifts production certificate coverage from 0.812/0.753 to 0.940/0.946, at the cost of capacity (1.88×→1.68×1.88×→ 1.68×) and a further ∼0.1 0.1 drop in the throughput ratio—a clear operator knob: capacity and speed, or a guarantee almost everywhere. (d) The certificate’s marginal cost is +6.4% (1.5B) / +16.2% (7B) without the bypass and +2.4% / +11.8% with it. This does not contradict the +0.35% measured at kernel level, but the two must not be conflated: that came from an S=4096S=4096 microbenchmark where per-tile work is amortised over 128 tiles, whereas these requests are about 50 tokens long and the cost grows with query-head count (12 for 1.5B, 28 for 7B). The certificate is close to free on long sequences and a real 2–16% cost on short-sequence decoding. page_size=16=16 is faster than page_size=1=1 (1.5B, single-run A/B: 549.8 vs. 477.6 tok/s; Table 17’s 511.8 is the later median-of-3): with larger pages the slots are contiguous and the halved int8 traffic starts to pay off. Figure 3: Meter-guided repair of a broken fp8 KV cache (24-prompt needle task). Four configurations are tried in sequence—raw fp8, ++scaling, ++top-8 outlier bypass, and K=int8/V=fp8—and the meter’s coverage (line, computable online without labels) ranks every attempt in the same order as ground-truth accuracy (bars): the diagnosis is available before any evaluation is run. Figure 4: Sound, not clairvoyant: meter coverage at τ=0.2τ=0.2 (online, no ground truth) against needle accuracy (ground truth) for nine configurations. High coverage implies safety (zero missed dangers across all schemes); low coverage guarantees nothing in either direction—KIVI-2bit survives on average yet hides a 1/24 silent tail failure. Figure 5: Meter gating at benchmark scale (labels per Sec. 4.3: risk-ranked at τ≥1τ≥1, certified at τ<1τ<1): quality floor empirically restored (left; a benchmark outcome, not a corollary of the TV bound); one-time page-in traffic under incremental persistent repair (right)—the safe scheme pays 3.4×3.4× less than the broken one. 6.3.9 Gated evaluation at benchmark scale The needle-rescue demonstration underlying Figs. 3, 4 and 7 covers 24 prompts. Here we evaluate at benchmark scale (Table 18): the six hard RULER-4096 tasks (niah_multikey_2/3, niah_single_2, niah_multiquery, qa_1, qa_2) × 25 samples == 150 prompts, Qwen2.5-7B, served through the SGLang observatory, with incremental persistent repair (un-repaired slots of an over-threshold request are paged in exactly once, written back to the pool, and their witnesses zeroed): Table 18: Gated evaluation at benchmark scale (six hard RULER-4096 tasks × 25 samples, Qwen2.5-7B via the SGLang observatory, single run; slice-0 of three disjoint slices). Coveragea is always counted at τ=0.2τ=0.2. Configuration avg zero-score coveragea one-time page-in uncompressed 79.3 19 1.000 — fp8 raw 22.8 114 0.019 — fp8 + gate (τ=5τ=5, risk-ranked) 79.7 19 0.537 26.1 GiB kivi-2bit raw 73.7 28 ∼5×10−5 5\!×\!10^-5 — kivi + gate (τ=0.2τ=0.2, certified) 79.3 19 0.978 30.5 GiB rtn-int8 raw 78.7 20 0.207 — rtn-int8 + gate (τ=5τ=5, risk-ranked) 79.3 19 0.485 7.7 GiB a Gated-row coverage is post-repair (paged-in slots have their witnesses zeroed), raw-row coverage is pre-repair; e.g. the kivi pair ∼5×10−5→0.978 5\!×\!10^-5→ 0.978 is a before/after pair of the same quantity, not two measurements of one state. All coverage values are counted at τ=0.2τ=0.2 regardless of the gate threshold. Gate labels follow Sec. 4.3: at τ≥1τ≥ 1 the meter is saturated and acts as a risk score with no TV guarantee; at τ<1τ<1 the gate is certified. Repeatability: Table 18 shows slice 0; two further disjoint 25-sample-per-task slices (450 unique samples in total) replicate every directional conclusion—uncompressed 79.3/87.2/83.4 (mean 83.3), raw fp8 22.8/27.8/28.7 (mean 26.4), gated means within 0.4 of uncompressed, and KIVI’s extra zero-score tail (+9+9 to +12+12) eliminated on every slice. Confidence intervals (per-sample paired bootstrap, 10410^4 resamples). A fresh rerun of all seven configurations with per-sample logging (slice 0; every configuration reproduces within run-to-run noise, largest shift kivi raw 73.7→71.373.7→ 71.3) gives, paired against uncompressed on the same 150 prompts: the gated configurations lose nothing—the int8 and kivi gates score identically to uncompressed on every single sample (paired difference 0.00.0), and the fp8 gate differs by +0.3+0.3 (95% CI [+0.0,+0.8][+0.0,+0.8]; unrounded means—Table 18’s slice difference is +0.4+0.4)—while the raw collapses are statistically significant: fp8 −56.6-56.6 [−64.1,−49.1][-64.1,-49.1], and KIVI’s silent tail is now significant rather than anecdotal, −8.1-8.1 [−13.8,−2.6][-13.8,-2.6]. Data: exp/out/te_ci.json. (a) The quality floor is fully restored at benchmark scale—an empirical result (Fig. 5): all three gated schemes return to the uncompressed level (79.3–79.7); fp8 gains +56.9+56.9 points, and KIVI’s 9 silent zero-score samples (28 vs. 19) are all eliminated—the 1/24 needle tail failure was not an accident but a systematic tail. For fp8 and int8 this is risk-ranked gating: at τ=5τ=5 the meter carries no TV guarantee and acts as an empirical ranking signal, whose discriminative power is established independently by the 27.6×27.6× fallback-error drop of Sec. 6.3.4; the kivi gate (τ=0.2τ=0.2) operates in the certified regime. (b) Selectivity holds at scale: the safe scheme (int8) pays 7.7 GiB of page-in, 3.4×3.4× less than the broken one. (c) Incremental persistent repair is essential engineering: naive whole-request re-paging reaches 1267 GiB on gated fp8 (each newly written token’s witness re-fires the gate); filtering already-repaired slots by witness-nonzero brings it to 30.9 GiB, a 41×41× reduction (both measured at the certified τ=0.2τ=0.2 gate; the τ=5τ=5 row of Table 18 pays 26.1 GiB). (d) Boundary: 150 samples, single run; a second faithful replica of a published method (kvquant4: per-channel 4-bit ++ top-1% sparse outliers, coverage 0.00066) also shows “perfect average, ∼0 0 coverage” on needle (cf. Fig. 6)—corroborating with KIVI that real aggressive schemes hold the mean through structure, admit no informative per-step certificate from the current witness, and rely on the gate for the tail. 6.3.10 Scale and cross-generation evaluation (8×8×H200) The systems results above were produced on a single Ada GPU (RTX 4090). This section ports the same patch and protocols to 8×8×H200 (143 GB each, Hopper) and answers four questions: do the structural numbers reproduce across GPU generations, do they hold up the scale ladder, how does the system compare in-frame against a full certified-serving baseline, and where is the real cost frontier of certification. Cross-generation consistency and the scale ladder. The capacity ratio is determined by the data layout, and measurement confirms it: 1.882× (no bypass) is bit-identical across 7B/14B/32B single-GPU, 7B tp2/tp4, and 70B tp4 (70B tp4: witcert capacity 2,183,776 tokens vs. fp16 1,160,128; throughput ratio 0.79×); with outlier bypass, 1.684× is likewise invariant. The four request-level-δ coverage cells (1.5B/7B × with/without bypass) match the 4090 values within 0.3 p, with the 7B-with-bypass cell (0.9457) bit-identical. The δ risk–coverage protocol of Sec. 5 extends to 14B/32B with zero violations at every δ and coverage in the same band as 7B; 72B coverage is 25.5–29.8% (three domains, zero violations)—markedly below the 54–81% of 7–32B, a second weakening result after Yi, reported as such (same-type conjecture: interaction of block-wise scaling with that model’s activation statistics). Tensor parallelism: the packed pool shards per rank with no code change; at tp2, witcert overtakes fp16 (338 vs. 287 tok/s—in the communication-bound segment the smaller KV read becomes an advantage), and tp8 is structurally infeasible for 28-head Qwen-7B (28∤828 8), so the 8-GPU rung is carried by 64-head Llama-70B. In-frame against the Runtime-Certified full system. Answering the fourth review round, we reproduce the complete system of [5] from its paper description (INT8-key/INT4-value two-tier store, two-pass pipeline, adaptive top-K∗K^* promotion at τcov=0.995 _cov=0.995, value promotion, ranking-consistency fallback, FP16 originals pinned in CPU RAM; no public code exists, and our specification notes declare every deviation—HF/SDPA level, bf16 weights, our corpus). Fidelity checks pass: its Rung-3 trigger rate is 1.02% of head-steps (same order as the original), K∗=117K^*=117 sits near the cap exactly as its short-context saturation predicts, and the reproduced fast path is bit-identical to dense in ppl. In-frame results (Llama-3.1-8B, 8 paired windows at ctx 8192): Δ RC +0.0059 / WitCert +0.0123, both quality-neutral; on 7 RULER-4096 tasks all three systems tie at 0.9924. The architectural difference is what separates them: RC’s fast path pages promoted FP16 keys from CPU on every step—measured at 264 MB per request (RULER-4096)—and requires a permanently resident 100% FP16 CPU copy, whereas WitCert’s certified mode pages in nothing and holds no CPU replica; page-in occurs only when the gate fires. In a unified per-token ledger (same memory pool, normalized): relative GPU bytes fp16 1.0 / witcert 0.531 / witcert+bypass 0.594 / RC tier-1 0.563; CPU replica 0/0/0/1.0; steady-state PCIe 0/0/0/264 MB⋅·req-1. Packed gated closed loop end to end (closing contribution 4). The packed real store (int8 + dither + outlier bypass) without gating scores 78.83 vs. fp16 78.67 on RULER 6 hard tasks × 25—the first end-to-end quality measurement of the packed path, quality-neutral; with the τ=0.2τ=0.2 certificate-gated closed loop (full-pool CPU backing, request-level repair) it scores 78.83, identical to ungated. Our first run collapsed to 2.0: the packed pool never wrote its CPU backing (allocated but forever zero), so repair paged back all-zero KV; instrumented cross-checking (|kk|=0|k|=0 while the recomputation matched an fp32 reference exactly) localized it, a one-line fix restored full quality—a bug that is itself a working argument for runtime verification, since the original smoke test (“no crash, bytes moved”) was green while moving zeros. The gating cost is reported honestly: per-request page-in P50/P95 = 2.81 / 3.58 GiB (serial differencing over 150 requests)—the intrinsic cost of non-persistent packed repair (the pool stays quantized, so the certificate re-fires each step); a request-level repair cache is the identified optimization, and this distribution is exactly its upper bound. Long-context serving and the cost frontier. On Llama-8B (paired, CUDA graphs on): witcert median TTFT ratio 1.84×→×→ 1.89× and TPOT 1.47×→×→ 1.49× from 8k to 32k inputs—the cost ratio is flat in S, which corrects our earlier “long sequences are nearly free” inference to “the cost ratio is constant.” The concurrency–throughput frontier (7B, 1024-in/256-out, c=1→512c=1→ 512): fp16 203 → 14,324 tok/s, witcert 155 → 6,207; the most adverse operating point (short requests at high concurrency, where attention dominates step time and the capacity advantage is idle) is 0.43×, single-stream is 0.78×, and tp2 reverses the sign—we publish both full curves and state plainly that witcert’s home turf is the capacity-limited long-context/multi-session segment, not short-request high concurrency. 70B on 2 GPUs (tp2) serving 128k requests: fp16 capacity 339,216 tokens with a 16×12716× 127k-request benchmark on record (witcert under the same protocol; its extend-kernel prefill cost at 128k is significant and is itemized in the overhead summary). 6.4 Analysis What the certificate does and does not guarantee. The formal object is a local bound: per-(layer, head, step) attention TV (and, through the value term, that step’s attention output). End-task quality additionally passes through residual streams, MLPs, normalization, later layers and sampling, and Sec. 6.4.1 itself shows the map from local fidelity to task quality is not one-to-one (single-layer pollution is fully absorbed, 0/28). Consequently every “quality floor restored” statement in this paper is an empirical benchmark result about gating driven by the meter—never a corollary of the TV bound. The formal guarantee and the empirical outcome are deliberately reported side by side and must not be conflated. Figure 6: Aggressive schemes survive on structure, not per-step fidelity: per-step danger rate (fraction of steps with true TV >0.2>0.2; red) against end-task needle accuracy (blue). KIVI-2bit distorts 21.9% of steps yet retrieves 95.8%, and its one silent failure is exactly what the gate rescues; naive rtn-2bit distorts more and collapses. Figure 7: The gate is selective and tunable: one-time page-in traffic (24 requests) as the gate threshold sweeps τgate∈0.2,1,5 _gate∈\0.2,1,5\. Raising the threshold cuts traffic 4.4×4.4× with no accuracy loss (all bars remain 24/24), and the safe scheme (rtn-int8) triggers 22–3×3× less than the broken one (fp8) at every threshold. 6.4.1 Mechanism: the failure is cross-layer accumulation There is no critical layer. Polluting a single layer with kivi2 while keeping all others exact, swept over all 28 layers, loses nothing: 0/28 layers show any degradation (accuracy 1.0 each), while polluting all layers gives 0.958. Single-layer distortion is fully absorbed downstream; the observable failure is purely accumulative. This explains why per-step sound certificates are “too strict” for aggressive schemes—they must assume worst-case accumulation while the real network cancels heavily across layers—and it motivates both request-level (rather than per-layer) gating and the open problem of tighter multi-layer composed certificates. 6.4.2 Bound shapes across witness regimes System-level comparison with the Runtime-Certified bound shape (same witness, same harness, same τ=0.99τ=0.99). We implemented the competitor’s deterministic shape tanh(maxtΔt) ( _t _t) inside the same kernel (max-merged across splits) and gated the same RULER task. Both shapes empirically restore the quality floor (79.3–80.1), but in the loose Tier-A witness regime the det-tanh gate is 2.52.5–5.2×5.2× cheaper in traffic (fp8: 12.1 vs. 30.8 GiB; int8: 5.3 vs. 27.3 GiB)—tanh is capped while the e-form’s ∑p~ecΣ p\,e^c is exponentially amplified by a single large c. This does not contradict the e-form’s dominance for the controlled dithered quantizer (coverage 54.4–81.0% vs. 11.8–52.0% at δ=10−2δ=10^-2): the right bound shape depends on the witness-tightness regime, and the framework accommodates both behind an environment switch. (At τ=0.99τ=0.99 both gates sit just inside the certified regime, but the Tier-A witness is loose there, so the comparison is of risk-score behaviour near saturation.) We report this partially competitor-favouring result as is. 6.4.3 The Yi anomaly, resolved This also resolves the Yi anomaly reported earlier. There, Yi-1.5-6B’s coverage (54.4–64.8%) was markedly below Qwen’s (∼80% 80\%) and we speculated, without verification, that its rope_theta=5×106=5×10^6 was responsible. The measured answer is different: the effect comes from block-level scaling, not from the model. Yi’s channel energy is less concentrated (top-4 RoPE pairs carry 41.2% of the energy versus Qwen’s 54.3%), and a block scale—one value covering 256 tokens—is dragged down by the worst channel in the block; per-token scaling adapts, and under it Yi is in fact easier than Qwen (0.907 vs. 0.525 at m=0m=0). The phenomenon is an interaction between the model’s energy distribution and the scale granularity, and it disappears under the per-token group scaling actually used in deployment. We retract the rope_theta conjecture. 6.4.4 Regime statement This work does not enter the pure compression-ratio contest. The regime in which we claim leadership is delimited by three quantifiable conditions: 1. Guarantee dimension: deployments requiring per-(layer, head, step) error upper bounds with an explicit failure-probability budget. The only existing methods in this regime are the Runtime-Certified family [5] (deterministic tanh ); at δreq=10−2 _req=10^-2 we cut the KV-head page-in rate from 44.4% to 22.0% and authorize compression 3.43 bits/dim deeper (Qwen2.5-1.5B, 2k context, global scaling), with a 28.7–77.0% relative reduction in page-in rate across three model families and three domains (6–7B class, 4–8k context, online block-wise scaling). 2. Workload: decode-bound long context (S≥8S≥ 8k, small nqn_q), memory-traffic limited; the marginal overhead of the certificate has been measured in this regime (−1.3%-1.3\% in our kernel, +11.9%+11.9\% in the SGLang production kernel). Prefill-heavy and training scenarios are out of scope. 3. Hardware and scale: one to eight GPUs across two generations (single RTX 4090, Ada; 8×8×H200, Hopper—the structural numbers, capacity ratios and coverage, reproduce bit-identically across generations, Sec. 6.3.10); δ curves span 1.5B–72B, serving spans 7B–70B (tp1/2/4) plus 70B on two GPUs at 128k; native-128k coverage is measured on Llama-3.1-8B (Sec. 5.2). Under tensor parallelism the packed pool shards per rank and works unchanged; cross-rank certificate aggregation (an any() gate across ranks) remains unverified. Dimensions on which we do not lead (stated honestly): absolute compression ratio (RTN-INT4 and the 1-bit families save more), absolute latency (our unoptimized kernel is 5.41×5.41× an fp16 baseline in Sec. 6.3.1; 0.43× throughput at the short-request high-concurrency extreme, Sec. 6.3.10), and pure-throughput scenarios that need no guarantee. The certificate-telemetry path is currently incompatible with CUDA-graph capture (a host synchronization); cert-on deployments must disable graph capture or await a kernel-side fix. 6.4.5 Every overhead and byte-saving figure in one place; choosing τ and δ The meter’s overhead and the byte savings were each measured several times in this paper, under deliberately different conditions. To prevent the reader from carrying six numbers, the two tables below list every figure with its configuration; each is discussed at its point of measurement. Table 19: Every overhead figure in this paper, with its configuration. Overhead Kernel / path Setting What is measured −1.3%-1.3\% research kernel (dither-dominated) S=32768S=32768 micro cert on/off latency delta (6.1.1) +11.9%+11.9\% SGLang decode kernel, fp16 store S=4096S=4096 micro one extra accumulator (6.2.2) +0.35%+0.35\% SGLang decode kernel, quantized store S=4096S=4096 micro cert shares the scale load (6.2.3) +6.4%+6.4\% / +16.2%+16.2\% serving 1.5B / 7B, no bypass batch 16 × 64-tok end-to-end throughput (6.2.4) +2.4%+2.4\% / +11.8%+11.8\% serving 1.5B / 7B, m=4m=4 bypass batch 16 × 64-tok end-to-end throughput (6.2.4) 1.2%1.2\% telemetry alone, 7B isolated A/B 287.6 vs. 284.1 tok/s (6.2.4) The external figures to quote: +11.9%+11.9\% at kernel level on an fp16 store, +0.35%+0.35\% once storage is quantized, 2–16% on short-request serving, near free on long sequences. Table 20: Every byte-saving figure in this paper, with its configuration. Saving Scope Configuration How measured 43.3% K side block scale, m=4m=4, packed store, S=32768S=32768 torch.cuda.memory_allocated (5) 46.5% K++V RULER config: K 145.1 B ++ V 129 B vs. 512 B computed, re-verified (6.3.3) 46.9% K++V per-token Gc=32G_c=32 scaling (SGLang store) measured, 136 B per side (6.2.3) 31.5% net effective after gated fallback, 10.96 bits/dim closed-loop account (6.3.4) 24.5% K side m=16m=16 zero-fallback point computed (6.3.6) Choosing τ and δ in practice. In the certified regime the threshold is an output-error budget: by the output bound of Sec. 4, a TV threshold τ admits at most 2τmaxt‖vt‖2τ _t\|v_t\| of attention-side output error, so an operator walks their output tolerance backwards through that inequality; our defaults τK=0.2 _K=0.2, τV=0.05 _V=0.05 came from this exercise. In the risk-ranked regime (τ≥1τ≥ 1) no such translation exists; there τ is a traffic knob, and the principled procedure is to profile the raw score’s distribution on a handful of requests and set τ at the quantile whose page-in budget the deployment affords (Fig. 7); the τ=5τ=5 of Sec. 6.3.9 was chosen this way. On δ: the union-bound allocation is conservative but enters only through log . The offline main experiments allocate over Ncell=L⋅H⋅SN_cell=L· H· S (layers × query heads × tokens; 28⋅28⋅8192≈6.4×10628· 28· 8192≈ 6.4× 10^6 at 7B/8k), which inflates the radius utu_t by log(2SNcell/δreq)/log(2S/δreq)≈1.45 (2SN_cell/ _req)/ (2S/ _req)≈ 1.45 at δreq=10−2 _req=10^-2—a ∼45% 45\% price. A deployment that instead allocates over its actual decode-step budget (the SGLang path uses T=256T=256 by default: L⋅H⋅T≈2.0×105L· H· T≈ 2.0× 10^5) pays ≈1.36≈1.36. Either way the δ sweep of Sec. 5 shows the conservatism is cheap to carry: 500×500× tighter δ costs at most 3.2 p of coverage. 6.4.6 Open problems Three problems remain open and we state them as such. (1) Tightening the universal witness below 8 bits. The deterministic band-norm witness is vacuous for 2–4 bit schemes (1289×1289× loose at 4-bit); candidate directions are second-moment witnesses, finer bands, and calibration-assisted hybrid bounds. Until then, selective gating is limited to the 8-bit-class regime and coarser schemes fall back to always-on tiered repair. (2) Multi-layer composed certificates. Our layer-pollution sweep shows the observable failure of aggressive schemes is purely cross-layer accumulation (0/28 single layers matter), so a per-step per-layer bound is intrinsically conservative; a sound certificate that composes across layers would close much of the gap, and nothing in our framework forbids it. (3) Certifying eviction online. The exact distortion of token dropping equals the dropped attention mass and separates methods cleanly offline, but every per-block constant-size witness we tried is vacuous online due to logit cancellation; whether a cheap sound online witness exists for eviction is open. Distinct from these theory questions, the engineering ledger: the packed path’s end-to-end quality and gated closed loop are now measured and closed (Sec. 6.3.10); newly opened are a request-level repair cache (the gated page-in distribution bounds its benefit), a CUDA-graph-safe certificate telemetry path (eliminating the host synchronization), and the anomalous cert-on long-context decode amplification on the 4-KV-head 7B configuration (TPOT 9×9× at 30k inputs, asymmetric to Llama-8B’s 1.49×; reproduced, not yet dissected). 7 Reproducibility Four independent implementations, cross-checked. The numerical correctness of the certificate is jointly guaranteed by four mutually independent implementations: (i) the Triton kernel; (i) a PyTorch reference; (i) a 50-digit mpmath golden specification; and (iv) a fourth implementation rewritten from the theorem statement alone, without reading the code of the other three (tests/test_independent_crosscheck.py). The role of the fourth is to rule out the failure mode “three implementations share one misunderstanding”—the first three are one author’s three encodings of the same formula, whereas the fourth follows only the definitions as stated in the paper. The three and the fourth agree to 40 digits of precision. The formal development builds on Lean 4 [10] and Mathlib [38]. Lean verifies the stated theorems; whether the deployed loop satisfies their hypotheses is exactly what the proof–kernel contract tests and the non-adaptive-query scope of Sec. 4.2 delimit—machine-checking does not substitute for either. Code: https://github.com/wayfind/witcert (private; to be opened at publication). All numbers are recomputable from the raw JSON and logs under exp/out*/ and exp/m2a_provenance/. • Theory regression: tests/test_certificates.py (two-token counterexample guard ++ 500k adversarial trials). • Kernel acceptance: tests/test_kernel_match.py (elementwise agreement / no clipping / stream uniqueness / round-trip), tests/test_attn_cert.py (kernel vs reference ++ soundness). • Experiments: exp/p12–p21 (certificate evolution, cross-model δ curves, the M3 design gate, the quad report, CUDA graph). • SGLang integration: exp/sglang_witcert_telemetry.patch (54 lines, revertible) plus the raw 3×33× 3 A/B logs; the production decode-kernel certificate of Sec. 6.2.2 is integration/witcert_sglang.patch (500 lines). Environment: RTX 4090 / CUDA 12.4 / PyTorch 2.6.0 / Triton 3.2; SGLang 0.5.9 with PyTorch 2.9.1 (cu128). Randomness is fully specified by the Philox five-tuple counter, with seeds recorded in the result JSON metadata. 8 Conclusion A sound runtime meter turns KV-cache compression from an open-loop bet into an observable, gateable system quantity: any cache-preserving scheme can be measured in live serving, broken schemes are repaired at benchmark scale by meter-driven gating (fp8 restored from 22.8 to 79.7, paired difference +0.3+0.3 [+0.0,+0.8][+0.0,+0.8] against uncompressed), and analysis with the meter shows that what keeps aggressive schemes alive is cross-layer cancellation rather than per-step fidelity. On the certified tier, trading an explicit request-level risk budget for coverage is what turns the certificate from decoration into a tool: the sub-Gaussian certificate reduces the page-in rate of a sound deterministic tanh bound by 28.7–77.0% relative, with very weak dependence on δ, and subtractive dither—the quantizer that makes it valid—is quality neutral against same-bit-width RTN, so the guarantee costs no accuracy. We also report, as first-class results, a plausible certificate that is unsound (with its minimal counterexample and sound replacement), a tightening that a theorem promises and measurement declines to deliver, and every retraction made along the way; the counterexample–repair–adversarial-validation methodology (Appendix B) and all raw data are released with the code. Appendix A Machine-checked theorem statements (compiled, not transcribed) This section is compiled from the Lean development: formal/Export.lean walks the environment, prints each theorem’s elaborated type with Lean’s own pretty-printer, and lists the axioms each proof actually depends on via collectAxioms; for the pdflatex toolchain, non-ASCII symbols are mechanically transliterated (ℝ→RR , ℕ→NatN , etc.). Nothing here is transcribed by hand, so a statement that is not proved cannot appear. Twice in this project’s history a certificate formula was falsified by external review, and in both cases the root cause was that the statement on paper and the statement that holds were not the same object. The development proves 4 core theorems—the results cited in the body—plus 26 supporting lemmas, many of which are typeclass boilerplate of the dependency-free layer and are listed compactly below only so that the axiom audit covers the whole development; every proof depends only on propext, Classical.choice and Quot.sound (or on nothing at all), and none on sorryAx. A.1 Mathlib layer (reals / measure theory) L4: proof-kernel refinement (blockwise = per-token) Source: formal/WitCert/Refinement.lean:38; axioms: propext, Quot.sound, Classical.choice. forall iota : Type u_1 beta : Type u_2 [inst : Fintype iota] [inst_1 : DecidableEq beta] (p : iota -> R) (blk : iota -> beta) (wB : beta -> R) (B : Finset beta), (forall (t : iota), blk t in B) -> WitCert.A_blockwise p blk wB B = WitCert.A_perToken p fun t => wB (blk t) L3: request-level union budget Source: formal/WitCert/RequestBudget.lean:23; axioms: propext, Classical.choice, Quot.sound. forall Omega : Type u_1 [inst : MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) n : Nat (E : Fin n -> Set Omega) (deltaloc deltareq : ENNReal), (forall (i : Fin n), mu (E i) <= deltaloc) -> n * deltaloc <= deltareq -> mu (Union i, E i) <= deltareq L2 core: sub-Gaussian proxy of uniform dither Source: formal/WitCert/UniformDither.lean:57; axioms: propext, Classical.choice, Quot.sound. forall (x : R), 0 <= x -> Real.sinh x <= x * Real.exp (x 2 / 6) L1 main theorem: e-form TV bound for softmax perturbation Source: formal/WitCert/SoftmaxTV.lean:127; axioms: propext, Quot.sound, Classical.choice. forall iota : Type u_1 [inst : Fintype iota] (p ptilde eps c : iota -> R), (forall (t : iota), 0 <= ptilde t) -> Sum t : iota, ptilde t = 1 -> (forall (t : iota), 0 <= c t) -> (forall (t : iota), |eps t| <= c t) -> 0 < WitCert.Znorm ptilde eps -> (forall (t : iota), p t = ptilde t * Real.exp (-eps t) / WitCert.Znorm ptilde eps) -> WitCert.TV p ptilde <= 1 / 2 * (WitCert.Acert ptilde c 2 - 1) WitCert.Acert_ge_one Source: formal/WitCert/SoftmaxTV.lean:34; axioms: propext, Quot.sound, Classical.choice. forall iota : Type u_1 [inst : Fintype iota] (p c : iota -> R), (forall (t : iota), 0 <= p t) -> Sum t : iota, p t = 1 -> (forall (t : iota), 0 <= c t) -> 1 <= WitCert.Acert p c WitCert.Znorm_le_Acert Source: formal/WitCert/SoftmaxTV.lean:82; axioms: propext, Quot.sound, Classical.choice. forall iota : Type u_1 [inst : Fintype iota] (ptilde eps c : iota -> R), (forall (t : iota), 0 <= ptilde t) -> (forall (t : iota), -eps t <= c t) -> WitCert.Znorm ptilde eps <= WitCert.Acert ptilde c WitCert.deltaLocal_budget Source: formal/WitCert/RequestBudget.lean:36; axioms: propext, Classical.choice, Quot.sound. forall (deltareq : R) (L H T : Nat), 0 < L * H * T -> (L * H * T) * WitCert.deltaLocal deltareq L H T = deltareq WitCert.one_le_Acert_mul_Znorm Source: formal/WitCert/SoftmaxTV.lean:52; axioms: propext, Quot.sound, Classical.choice. forall iota : Type u_1 [inst : Fintype iota] (ptilde eps c : iota -> R), (forall (t : iota), 0 <= ptilde t) -> Sum t : iota, ptilde t = 1 -> (forall (t : iota), eps t <= c t) -> 1 <= WitCert.Acert ptilde c * WitCert.Znorm ptilde eps WitCert.pointwise_ratio_bound Source: formal/WitCert/SoftmaxTV.lean:90; axioms: propext, Classical.choice, Quot.sound. forall (a z A b : R), 0 < z -> 0 < b -> 1 <= A -> a <= b -> 1 / b <= a -> 1 <= A * z -> z <= A -> |a / z - 1| <= A * b - 1 WitCert.six_pow_mul_factorial_le Source: formal/WitCert/UniformDither.lean:32; axioms: propext, Classical.choice, Quot.sound. forall (n : Nat), 6 n * n.factorial <= (2 * n + 1).factorial WitCert.uniformProxy_eq_variance Source: formal/WitCert/UniformDither.lean:85; axioms: propext, Classical.choice, Quot.sound. forall (s : R), WitCert.uniformProxy s = s 2 / 12 A.2 Dependency-free layer (seconds-scale CI) Supporting lemmas (axiom-audit completeness only) WitCert.DistribSum.add_assoc (standalone/Refinement.lean:0); WitCert.DistribSum.add_comm (standalone/Refinement.lean:0); WitCert.DistribSum.add_zero (standalone/Refinement.lean:0); WitCert.DistribSum.left_distrib (standalone/Refinement.lean:0); WitCert.DistribSum.mul_zero (standalone/Refinement.lean:0); WitCert.OrdAdd.add_le_add (standalone/Budget.lean:0); WitCert.OrdAdd.add_zero (standalone/Budget.lean:0); WitCert.OrdAdd.le_refl (standalone/Budget.lean:0); WitCert.OrdAdd.le_trans (standalone/Budget.lean:0); WitCert.OrdAdd.zero_le_zero (standalone/Budget.lean:0); WitCert.blockwise_eq_perTokenGrouped (standalone/Refinement.lean:79); WitCert.fact_two_step (standalone/Factorial.lean:25); WitCert.lsum_le_nsmul (standalone/Budget.lean:54); WitCert.perToken_eq_mul_lsum (standalone/Refinement.lean:57); WitCert.psum_mono (standalone/EForm.lean:39); WitCert.request_budget_compose (standalone/Budget.lean:69); WitCert.six_mul_succ_le (standalone/Factorial.lean:16); WitCert.six_pow_mul_fact_le (standalone/Factorial.lean:42); WitCert.sq_add_one_ge_two_mul (standalone/EForm.lean:14). Appendix B Evolution of Conclusions, Retractions, and Reproduction Protocol The bound evolved as follows: the unsound dispersion form of Sec. 3; its two-token counterexample (2026-07-27); the sound e-form; a Bernstein variant dominated by its range term; the uniform sub-Gaussian form; request-level δ allocation; and finally online block-wise scaling with in-block outlier selection. Each step is a separate script in the repository (exp/p12–p17) together with the measurement that motivated it and the regression test tests/test_certificates.py, including the negative results (deterministic rank-one frequency coarsening, in-band random projection, static frequency selection, per-token union bounding, and the stochastic-rounding branch of Sec. 6.3.6) that closed off alternative designs. Beyond the bound itself, four conclusions changed during development. We record them here, once, rather than inline. (i) The claim that WitCert’s output error is 1.71.7–1.8×1.8× lower than same-bit-width RTN is retracted: that experiment used K in place of V (a K-side proxy); the correct statement, from the 2×22× 2 ablation of Sec. 6.3.2, is that dither is quality neutral (1.01×1.01×) and the quality gain belongs to the outlier bypass. (i) The conjecture that Yi’s low block-scaling coverage was caused by its large rope_theta is retracted; the measured cause is the interaction of block-level scaling with diffuse channel energy (Sec. 6.4.3). (i) An early single-run reading suggesting the meter costs nothing in serving was noise; the canonical account is the median-of-3 measurement of Sec. 6.2.4 (+6.4%+6.4\%/+16.2%+16.2\% without bypass). (iv) An early verdict that throughput competitiveness “cannot be claimed” was formed at kernel level (5.41×5.41×) and was too pessimistic: end-to-end, quantisation costs 0.750.75–0.82×0.82× (Sec. 6.2.4). The headline coverage range was also restated from a cross-δ envelope to the single-δ range 54.4–81.0% following external review. (v) The SGLang serving coverage figures were restated under the corrected request-level δ allocation (δloc=δreq/(L⋅H⋅T) _loc= _req/(L· H· T)): the earlier implementation allocated only over tokens and batch, and its figures (0.866/0.987 on 1.5B, 0.759/0.947 on 7B) are retired in favour of 0.812/0.940 and 0.753/0.946. (vi) A latent unbound-variable bug in the packed-cache fallback branch (_wc_ei for _wc_i), found by external review, was fixed and initially only smoke-tested in live serving (the gate fired, paged in 1.4 GiB over 2,015 calls and did not crash). The subsequent end-to-end run exposed a second bug: CPU backing had been allocated but never populated, so repair paged in zeros and quality fell to 2.0. After the one-line write-path fix, packed gating restored the score to 78.83, identical to the ungated packed path (Sec. 6.3.10). The benchmark-scale gating results of Sec. 6.3.9 are unaffected—they run through the observatory pool, whose fallback branch was always correct. Appendix C The Rigidity Proposition for Static Equivariant Compression This proposition predates the certificate line of this paper and survived the audit that retracted the rest of that early version; Related Work uses it to place the static RoPE-aware methods. Setting. (Within this appendix, p, r and c denote the complexified dimension, the sketch rank and an output index—unrelated to the attention notation of the body.) A single head of dimension d, complexified to p=d/2p=d/2 coordinates: RoPE acts at position n as the diagonal unitary Dn=diag(einθj)j≤pD_n=diag(e^in _j)_j≤ p, with the θj _j pairwise distinct and no θj+θj′≡0(mod2π) _j+ _j ≡ 0 2π. Call a real-linear :ℂp→ℂrS:C^p ^r an equivariant sketch (script S, to avoid clashing with the sequence length S) if some position representation Dm′D _m on ℂrC^r satisfies Dn=Dn′SD_n=D _nS for all n∈ℤn —equivariance being what keeps a compressed cache queryable by relative position. Proposition 2 (Rigidity). Every equivariant S is a frequency selection with per-frequency complex scalars: each output coordinate depends on a single input frequency, (z)c=αczj(c)(Sz)_c= _c\,z_j(c). If r<pr<p, then p−rp-r frequencies are necessarily dropped as whole pairs; exact logit preservation additionally forces |αc|=1| _c|=1. Proof. Decompose =+ℬ∘conjS=A+B with A complex linear and ℬB conjugate linear, and diagonalize Dn′=diag(einφc)D _n=diag(e^in _c). Entrywise, commutation gives cj(einθj−einφc)=0A_cj\,(e^in _j-e^in _c)=0 for all n, so cj≠0A_cj≠ 0 only if φc≡θj _c≡ _j; the entries of ℬB would require φc≡−θj _c≡- _j, which the frequency assumption excludes (up to flipping a 2D block’s orientation). Since the θj _j are pairwise distinct, each output row has at most one nonzero entry. ∎ RAP’s whole-pair pruning is the 0,1\0,1\ special case: in the strictly equivariant world there is no cleverer static compression. The proposition’s natural relaxations were rejected experimentally in the retracted early version (deterministic rank-1 spectral coarsening, in-band random projection, static selection), which is what motivated the runtime route taken by this paper. References [1] 01.AI. Yi: Open foundation models by 01.AI. arXiv:2403.04652, 2024. [2] Anastasios N. Angelopoulos and Stephen Bates. A gentle introduction to conformal prediction and distribution-free uncertainty quantification. arXiv:2107.07511, 2021. [3] Yushi Bai, Xin Lv, Jiajie Zhang, Hongchang Lyu, Jiankai Tang, Zhidian Huang, Zhengxiao Du, Xiao Liu, Aohan Zeng, Lei Hou, Yuxiao Dong, Jie Tang, and Juanzi Li. LongBench: A bilingual, multitask benchmark for long context understanding. In ACL, 2024. arXiv:2308.14508. [4] Priyansh Bhatnagar, Ashkan Moradifirouzabadi, Se-Hyun Yang, SeungJae Lee, Jungwook Choi, and Mingu Kang. STAR-KV: Low-rank KV cache compression via soft thresholding for adaptive rank control. arXiv:2606.08382, 2026. [5] Dean Calver. Runtime-certified bounded-error quantized attention. arXiv:2605.20868, 2026. [6] Chi-Chih Chang, Wei-Cheng Lin, Chien-Yu Lin, Chong-Yan Chen, Yu-Fang Hu, Pei-Shuo Wang, Ning-Chi Huang, Luis Ceze, Mohamed S. Abdelfattah, and Kai-Chiang Wu. Palu: Compressing KV-cache with low-rank projection. In ICLR, 2025. arXiv:2407.21118. [7] Vivek Chari and Benjamin Van Durme. Compactor: Calibrated query-agnostic KV cache compression with approximate leverage scores. arXiv:2507.08143, 2025. [8] Tri Dao, Daniel Y. Fu, Stefano Ermon, Atri Rudra, and Christopher Ré. FlashAttention: Fast and memory-efficient exact attention with IO-awareness. In NeurIPS, 2022. arXiv:2205.14135. [9] Tri Dao, Daniel Haziza, Francisco Massa, and Grigory Sizov. Flash-decoding for long-context inference. https://pytorch.org/blog/flash-decoding/, 2023. [10] Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In CADE-28, 2021. [11] DeepSeek-AI. DeepSeek-R1: Incentivizing reasoning capability in LLMs via reinforcement learning. arXiv:2501.12948, 2025. [12] Alessio Devoto, Maximilian Jeblick, and Simon Jégou. Expected attention: KV cache compression by estimating attention from future queries distribution. arXiv:2510.00636, 2025. [13] Alessio Devoto, Yu Zhao, Simone Scardapane, and Pasquale Minervini. A simple and effective L2L_2 norm-based strategy for KV cache compression. arXiv:2406.11430, 2024. [14] Robert M. Gray and Thomas G. Stockham. Dithered quantizers. IEEE Transactions on Information Theory, 39(3):805–812, 1993. [15] Coleman Hooper, Sehoon Kim, Hiva Mohammadzadeh, Michael W. Mahoney, Yakun Sophia Shao, Kurt Keutzer, and Amir Gholami. KVQuant: Towards 10 million context length LLM inference with KV cache quantization. arXiv:2401.18079, 2024. [16] Cheng-Ping Hsieh, Simeng Sun, Samuel Kriman, Shantanu Acharya, Dima Rekesh, Fei Jia, Yang Zhang, and Boris Ginsburg. RULER: What’s the real context size of your long-context language models? In COLM, 2024. arXiv:2404.06654. [17] Albert Q. Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chaplot, et al. Mistral 7B. arXiv:2310.06825, 2023. [18] Jang-Hyun Kim, Jinuk Kim, Sangwoo Kwon, Jae W. Lee, Sangdoo Yun, and Hyun Oh Song. KVzip: Query-agnostic KV cache compression with context reconstruction. In NeurIPS, 2025. arXiv:2505.23416. [19] Ekaterina Kochetkova, Kshiteej Sheth, Insu Han, Amir Zandieh, and Michael Kapralov. Streaming attention approximation via discrepancy theory. arXiv:2502.07861, 2025. [20] Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph E. Gonzalez, Hao Zhang, and Ion Stoica. Efficient memory management for large language model serving with PagedAttention. In SOSP, 2023. arXiv:2309.06180. [21] Damien Lesens, Beheshteh T. Rakhshan, and Guillaume Rabusseau. KQ-SVD: Compressing the KV cache with provable guarantees on attention fidelity. arXiv:2512.05916, 2025. [22] Junyan Li, Yang Zhang, Muhammad Yusuf Hassan, Talha Chafekar, Tianle Cai, Zhile Ren, Pengsheng Guo, Foroozan Karimzadeh, Colorado Reed, Chong Wang, and Chuang Gan. CommVQ: Commutative vector quantization for KV cache compression. In ICML, 2025. arXiv:2506.18879. [23] Wenhao Li, Jinhao Dong, Hailin Zhang, Wenhang Shi, Wei Lu, and Xiaoyong Du. RaBitQCache: Rotated binary quantization for KVCache in long context LLM inference. In ICML, 2026. arXiv:2606.31519. [24] Yuhong Li, Yingbing Huang, Bowen Yang, Bharat Venkitesh, Acyr Locatelli, Hanchen Ye, Tianle Cai, Patrick Lewis, and Deming Chen. SnapKV: LLM knows what you are looking for before generation. In NeurIPS, 2024. arXiv:2404.14469. [25] Fengfeng Liang, Yuechen Zhang, and Jiaya Jia. RoPE-aware bit allocation for KV-cache quantization. arXiv:2606.24033, 2026. [26] Stanley P. Lipshitz, Robert A. Wannamaker, and John Vanderkooy. Quantization and dither: A theoretical survey. Journal of the Audio Engineering Society, 40(5):355–375, 1992. [27] Zirui Liu, Jiayi Yuan, Hongye Jin, Shaochen Zhong, Zhaozhuo Xu, Vladimir Braverman, Beidi Chen, and Xia Hu. KIVI: A tuning-free asymmetric 2bit quantization for KV cache. In ICML, 2024. arXiv:2402.02750. [28] Lorenz K. Muller, Philippe Bich, Chiara Boretti, Hyun-Min Chang, Jiawei Zhuang, and Lukas Cavigelli. KVarN: Variance-normalized KV-cache quantization mitigates error accumulation in reasoning tasks. arXiv:2606.03458, 2026. [29] NVIDIA. kvpress: LLM KV cache compression made easy. https://github.com/NVIDIA/kvpress, 2024. [30] Bowen Peng, Jeffrey Quesnelle, Honglu Fan, and Enrico Shippole. YaRN: Efficient context window extension of large language models. In ICLR, 2024. arXiv:2309.00071. [31] Qwen Team. Qwen2.5 technical report. arXiv:2412.15115, 2024. [32] The risk of KV cache compression. arXiv:2607.01520, 2026. https://arxiv.org/abs/2607.01520. [33] John K. Salmon, Mark A. Moraes, Ron O. Dror, and David E. Shaw. Parallel random numbers: As easy as 1, 2, 3. In SC, 2011. [34] Luohe Shi, Zuchao Li, Lefei Zhang, Guoming Liu, Baoyuan Qi, and Hai Zhao. KV-Latent: Dimensional-level KV cache reduction with frequency-aware rotary positional embedding. In ACL, 2025. arXiv:2507.11273. [35] Jianlin Su, Yu Lu, Shengfeng Pan, Ahmed Murtadha, Bo Wen, and Yunfeng Liu. RoFormer: Enhanced transformer with rotary position embedding. arXiv:2104.09864, 2021. [36] Mingjie Sun, Xinlei Chen, J. Zico Kolter, and Zhuang Liu. Massive activations in large language models. arXiv:2402.17762, 2024. [37] Jiaming Tang, Yilong Zhao, Kan Zhu, Guangxuan Xiao, Baris Kasikci, and Song Han. Quest: Query-aware sparsity for efficient long-context LLM inference. In ICML, 2024. arXiv:2406.10774. [38] The mathlib Community. The Lean mathematical library. In CPP, 2020. [39] Vladimir Vovk, Alexander Gammerman, and Glenn Shafer. Algorithmic Learning in a Random World. Springer, 2005. [40] Guangxuan Xiao, Yuandong Tian, Beidi Chen, Song Han, and Mike Lewis. Efficient streaming language models with attention sinks. In ICLR, 2024. arXiv:2309.17453. [41] Jihao Xin, Tian Lyu, David Keyes, Hatem Ltaief, and Marco Canini. RAP: KV-cache compression via RoPE-aligned pruning. arXiv:2602.02599, 2026. [42] Yuhui Xu, Zhanming Jie, Hanze Dong, Lei Wang, Xudong Lu, Aojun Zhou, Amrita Saha, Caiming Xiong, and Doyen Sahoo. ThinK: Thinner key cache by query-driven pruning. arXiv:2407.21018, 2024. [43] Zihao Ye, Lequn Chen, Ruihang Lai, et al. FlashInfer: Efficient and customizable attention engine for LLM inference serving. arXiv:2501.01005, 2025. [44] Zhenyu Zhang, Ying Sheng, Tianyi Zhou, Tianlong Chen, Lianmin Zheng, Ruisi Cai, Zhao Song, Yuandong Tian, Christopher Ré, Clark Barrett, Zhangyang Wang, and Beidi Chen. H2O: Heavy-hitter oracle for efficient generative inference of LLMs. In NeurIPS, 2023. arXiv:2306.14048. [45] Lianmin Zheng, Liangsheng Yin, Zhiqiang Xie, Chuyue Sun, Jeff Huang, Cody Hao Yu, Shiyi Cao, Christos Kozyrakis, Ion Stoica, Joseph E. Gonzalez, Clark Barrett, and Ying Sheng. SGLang: Efficient execution of structured language model programs. In NeurIPS, 2024. arXiv:2312.07104. [46] Yuhao Zhou, Sirui Song, Boyang Liu, Zhiheng Xi, Senjie Jin, Xiaoran Fan, Zhihao Zhang, Wei Li, and Xuanjing Huang. EliteKV: Scalable KV cache compression via RoPE frequency selection and joint low-rank projection. arXiv:2503.01586, 2025.