ProofKV: Proof-Carrying KV Pages for Exact Greedy Decoding from Lossy Caches

KV-cache compression is now a central systems technique for long-context LLM serving, but existing methods typically treat the compressed cache as an approximation to be trusted empirically. Recent exactness-oriented alternatives either verify compressed drafts against the full cache or certify local attention computations rather than the model's end-to-end next-token decision. We introduce \textsc{ProofKV}, a proof-carrying KV-cache framework for \emph{exact greedy decoding} under lossy KV compression. The key idea is to augment each compressed page with a certificate sidecar that upper-bounds how much the page's missing information could still alter the current next-token decision. Given a compressed forward pass, ProofKV either certifies that the current greedy winner is already invariant to all remaining pagewise uncertainty, or performs only the minimum-cost page refinements needed to re-establish that proof. We prove compositional end-to-end uncertainty bounds, an argmax certificate for exact greedy decoding, and sequence-level exactness under finite monotone refinement. Empirically, on fit-audited, untruncated subsets of SCBench, LongBench v2, LongProc, and BigCodeBench-Hard, ProofKV recovers the exact \textsc{FullKV} greedy trajectory on every entered headline and confirmatory row, with zero observed false certificates, while lossy baselines frequently diverge early and degrade sharply on shared-context reuse, long procedural generation, and execution-sensitive code generation. Theorem-facing ablations show that the full certificate-and-repair ladder is load-bearing, richer sidecars materially tighten the proof, and cost-aware repair substantially improves the repair frontier. These results suggest that compressed model memory can be treated not merely as a weaker approximation, but as a proof-carrying state whose remaining uncertainty is explicit, auditable, and actionable.