ServeGuard: Verifiable, Bounded-Residual Confinement of Operator-Invisible Channels Without Revealing the Certified Read Factor
Dominik Dahlem, Rui Vieira
cs.CR
Sep 18, 2026 · v1
cs.LG
TL;DR
The kernel-algebra soundness theorems for monitor-typed adapter confinement are formalized in Lean 4 with Mathlib in a sorry-free module, with each theorem mapped to a named Lean declaration.
Abstract
Third-party adapters for open-weight language models ship as opaque weight matrices; a recipient cannot check whether an adapter hides a backdoor without trusting the publisher or inspecting the weights, the publisher's core asset. For one important class (payloads placed where a safety monitor is structurally blind), detection is unsound as a defense: every detector that factors through the declared monitor is invariant on its blind subspace, and honest and backdoored adapters overlap on every blind-subspace statistic we evaluate, because benign adaptation uses that subspace too. Rather than detect this channel, we make it structurally absent and prove that we did. The publisher builds the adapter to read the input only through directions the monitor covers and proves this in zero knowledge, revealing nothing about the read factor it certifies. The certificate is cheap because the expensive part, identifying the monitor's blind spot, is a deterministic function of the public base model, so only one linear identity is proved; the served residual is the base model's own public floor, not a prover-chosen tolerance. The result is ServeGuard, a supply-chain primitive: the publisher ships a proof-carrying adapter whose proof lets a consumer or regulator verify, without the certified read factor and without trusting the publisher, that the adapter carries no hidden channel of this class relative to the declared monitor; an admission-time typing guard binds the guarantee to the adapter bytes admitted at serving time. Across eight checkpoints up to 7B from four families, the monitoring budget is architectural: the measured frontier saturates at the value-path rank on grouped-query checkpoints but not on multi-head ones. On a 0.5B model confinement is nearly free for benign adaptation, making monitor quality the security lever.
Problem
Third-party LoRA adapters for open-weight language models are opaque, so recipients cannot check them for backdoors. Payloads placed in a safety monitor's blind subspace (its kernel) cannot be detected, because every detector that factors through the monitor is invariant on that subspace.
Approach
The publisher builds each adapter monitor-typed, with read factor A = CM, so the adapter reads input only through directions the public monitor covers. Inertness (ker M ⊆ ker V) is proved equivalent to factoring through the monitor. The publisher proves the linear identity A − CM = 0 in zero knowledge over a hiding commitment, and an admission-time guard binds the guarantee to the adapter bytes actually served. The soundness theorems are machine-checked in Lean 4 with Mathlib and depend only on standard classical axioms.
Results
The certificate accepts confined adapters and rejects stealth backdoors, including attacks that pass magnitude, rank and sparsity bounds. Across eight checkpoints up to 7B, the monitoring budget is architectural: the measured frontier saturates at the value-path rank on grouped-query models but not on multi-head ones. On a 0.5B model, confinement costs benign adaptation almost nothing.
| Paper statement | Lean declaration |
|---|
| Theorem 1(a) Channel-absence | attest_sound |
| Theorem 1(b) Factor-through | inert_iff_factors_through |
| Theorem 1(c) Defense | inert_of_factor_through_visible |
| Theorem 2 Typed LoRA | lora_typed_inert |
| Theorem 8 Deficient-basis counterexample | spanning_necessary |
Selected paper statements and their Lean declarations
