Runtime Observability for Heterogeneous Attention Memory

Modern LLMs no longer rely on a single plain KV cache; latent caches, learned sparse selectors, and recurrent states each carry memory in different forms and fail differently under compression. This paper proposes a runtime observability contract that spans all four memory classes using just three operators. The contract is instantiated on six model configurations across five architecture families, and per-stage bounds are composed into an executable request-level risk ledger.

A key design choice is carrying each contract's error metric as a type, so composition is only valid when metrics match. This type-level check rejected the authors' own first composed chain; the repaired chain crosses metrics via two proved bridges, while anything not formally certified falls back to empirical measurement. Every claim is thus certified, partially certified, or empirical, with composition inheriting the weakest tier automatically. Replayed over 12.4M entry reads under eight-way concurrency with per-request budgets and fail-closed identity attribution, the ledger quantifies honest trade-offs and holds its risk budget with zero violations. A fused always-on probe observes a declared one-layer subset under CUDA graphs within the serving noise floor.

Applied to a served DeepSeek-V4 stack with a packed compressed-KV prototype, the machinery localizes a silent corruption to a precise structural boundary — exact in eviction-free, identity-isolated regimes, with every observed failure in an eviction or slot-reuse regime. This result emerged from a machine-adjudicated discrimination campaign that even rejected two of the authors' own confounded inferences. All artifacts, guards, and the Lean development are released on GitHub, and every number in the paper regenerates from shipped artifacts with a single command.