A new tool tells LLM serving systems, mid-request, whether the memory-saving compression they're using is quietly wrecking the answer.
Researchers built WitCert, a runtime checker for KV-cache quantization - the technique inference servers use to shrink the memory footprint of the cache of past-token data models rely on to avoid redoing work. Until now, that compression was validated with offline benchmark averages, which say nothing about whether it's damaging the specific request being served right now. WitCert instead computes a per-layer, per-step upper bound on how far compressed attention drifts from the uncompressed version, with the underlying math machine-checked in a formal proof assistant called Lean 4. It plugs into the SGLang serving framework and can gate on its own risk signal, catching trouble instead of just logging it.
That gating pulled a badly compressed fp8 cache from a RULER benchmark score of 22.8 back up to 79.7, within a fraction of a point of the uncompressed baseline. It also surfaced an uncomfortable finding: aggressive compression schemes look fine in aggregate because errors cancel out across layers, not because any individual layer is clean - across 28 layers, none alone tanked the score. The certified INT8 version still packed 1.88x more KV tokens into the same memory as an uncompressed cache.
Benchmark averages have quietly served as the entire safety case for a technique now running under real production traffic. A meter that flags trouble per request, rather than per leaderboard, is a modest fix for a gap that arguably shouldn't have existed this long.