arXiv CSopen access

ServeGuard: Verifiable, Bounded-Residual Confinement of Operator-Invisible Channels Without Revealing the Certified Read Factor

· arxiv_cs

arXiv CS · Papers · License: Open Access

cryptography cybersecurity privacy security

cryptography, security, privacy, cybersecurity

arXiv:2609.21515v1 [cs.CR] 18 Sep 2026

ServeGuard: Verifiable, Bounded-Residual Confinement of Operator-Invisible Channels Without Revealing the Certified Read Factor Dominik Dahlem*

Rui Vieira

Red Hat AI [email protected]

Corresponding author.

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.

Introduction

Third-party model components ship as weights, and the supply chain that moves them (fine-tuning services, model hubs, vendor releases, and the regulators who must vet them) has no way to check what those weights carry. A fine-tuning service returns an adapter; a model hub serves a checkpoint; a vendor delivers a quantized release. The recipient runs the artifact inside a safety pipeline and wants assurance that it carries no hidden backdoor; the recipient’s own stakeholders (consumers, regulators, auditors) may require that assurance without direct access to the model. Three options exist today, and each fails. Benchmark scores say nothing about a payload that activates only on a 1

trigger. Full weight disclosure exposes the publisher’s intellectual property, and even then a weight matrix is not human-interpretable the way source code is. Third-party audit under non-disclosure relocates trust to the auditor rather than removing it. The recipient is left to trust the publisher. What can hide. We study one precisely characterized channel class. In a transformer attention layer, each token’s representation passes through three learned projections: the query and key maps, which determine which tokens attend to which, and the value map, which determines what information is read. Deployed safety monitors read the internal state through a fixed linear feature map: a probing classifier scores the residual stream through learned weights [3], a representationengineering defense watches the projection onto a declared refusal or harmfulness direction [2, 50], and an attention-pattern monitor such as Attention Tracker [25] post-processes the query/key features of selected heads. The post-processing may be nonlinear; what the certificate is defined against is the linear feature map, which is public once the operator declares what it watches, and a payload in the feature map’s kernel leaves every downstream statistic unchanged. A monitor that inspects only the query/key side has a blind subspace: perturbations it maps to zero and therefore cannot distinguish from no perturbation at all. Such a perturbation is invisible to every test that queries only the monitor’s output, at every payload strength, yet the value path reads it. The channel is invisible by construction, not by stealth, and it can be shipped as a LoRA adapter (a small, low-rank weight update added to a pretrained model). The security-relevant property is thus not the harm a particular payload causes but the invisibility: no detector that factors through the declared monitor can observe a kernel payload, and blind-space occupancy is not a sound reference-free discriminator of benign from payload-carrying adapters (Section 7), so the principled defense is to make the channel structurally absent, not to bound the payload in hand. Why detection fails. The first instinct is to detect the channel from the released weights. It is uninformative. The monitor’s blind subspace occupies most of the residual stream (the hidden-state vector passed between layers; 640 of 768 dimensions on GPT-2 [37]), so any low-rank adapter places the bulk of its computation there by geometry alone: a trained honest adapter and a backdoored one are indistinguishable on every kernel-activity statistic we evaluate (Section 7). This is not an artifact of a weak test: backdoors can be planted so as to be provably undetectable from the weights under explicit hardness assumptions [10, 18], with latent-space constructions resisting the known defenses [15]; absent a declared reference direction, weight-space detection has no sound target. Crucially, the no-go forbids distinguishing a backdoored model from a clean one without a reference; it does not forbid certifying a structural relation relative to a public, declared monitor. That distinction is the opening. The pivot: build it out and prove it. Rather than try to detect the channel, the publisher builds the adapter so the channel cannot exist and proves it. A LoRA adapter is a product of two small matrices: a read factor that selects which directions of the input the adapter accesses and a write factor that produces the output. If the read factor is constrained to access the input only through what the monitor exposes, then no input in the monitor’s blind subspace can reach the adapter at all, and the channel is absent by construction, regardless of what the publisher intended. This is the model-world analogue of proof-carrying code [32]: a property you build in and then prove you followed. The identity is exact, certifying that the adapter adds no blind-subspace read whatsoever rather than less than a threshold, so the served model’s residual exposure is the base model’s own public floor and not a prover-chosen tolerance. It is proved over fixed-point weights with the typed factors constructed on that encoding lattice (Section 6), so quantization adds no

slack, and it is cheap for a structural reason: the expensive part, identifying the blind subspace, is a deterministic function of the public base model, so it happens in the clear and the publisher proves one identity that is linear in the committed secret against a public matrix. The consumer checks static per-layer certificates once rather than monitoring every inference. Contributions. • A typed confinement defense, certified and cost-matched (Sections 3 to 5): rather than test a released adapter, the publisher builds a monitor-typed adapter whose read factor factors through the public monitor, certified by one linear identity in zero knowledge. The served residual is pinned exactly at the public base floor (Lemma 1). The deployed monitor augments the operator’s QK map with the value path’s top-gain singular directions (the spectral optimum, Theorem 5), whose reach across architectures we measure (Section 7). • Security evaluation and utility characterization (Section 7): an adaptive adversary, a targeted integrity manipulation, a cross-architecture geometry sweep (every layer and query head of 8 checkpoints spanning four families up to 7B), and a factorial utility study over monitor designs, budgets, ranks, and seeds on two instruction tasks. Confinement costs little and the cost separates cleanly from the security benefit: utility recovers to 98–99% under every monitor while the certified residual varies by orders of magnitude, driven to zero only by a monitor designed for the value path’s gain structure (η 2 : 0.2% vs 85%). • A measured zero-knowledge implementation (Sections 6 and 7): a Halo2 prover certifying value adapters in 6.4–48 s with 96–347 ms verification and 5.5–6.0 KB proofs (plain typed relation to one-time salted commit-and-prove binding), at algebraic false-accept probability ≈ 2−130 per certificate for a fixed commitment (the end-to-end bound adds the binding, knowledge-soundness, and grinding terms, Theorem 6), a whole-checkpoint package root binding every layer’s certificate, and an admission-time typing guard that ties the admitted read factor to the certified one. Together these deliver a proof-carrying adapter : a new supply-chain primitive that turns publisher trust into a verifiable structural guarantee a recipient checks without seeing the certified read factor. We call the end-to-end system ServeGuard, after the serving-time guard that binds the guarantee to the adapter bytes admitted at serving time rather than only the bytes attested (Theorem 7 states the composition). The certificate is relative to a declared public monitor : it certifies the absence of this linear-carrier channel class in the released update, against a committed checkpoint, for the subspace that monitor covers: a payload riding a direction the monitor does not probe is outside it (Section E), and whether that monitor is the safety-relevant object is a declared premise, not a proved one. Separating honest adapters from backdoors is the frontier it opens (Section 9).

Detection from weights, and defense by construction

The introduction described the supply-chain trust gap informally. This section makes it precise: the roles, the channel class, why detection cannot separate honest from malicious, and what defense replaces it. Roles. A prover (the publisher) holds an adapter ∆ = BA, commits to its read factor A and type witness C under a binding, hiding commitment c, and proves a structural property of the adapter. The hiding profile is fixed throughout: A, C, and the commitment salt stay secret; the write factor 3

B ships in the clear with the package and is hash-bound, not hidden; the proved statement is A = CMdep . A verifier (consumer, hub, or regulator) holds c and the public statement, and either the public base model or the published monitor matrix Mdep together with an authenticated manifest binding it to the base, and accepts or rejects. The adversary is the publisher itself, shipping a covert operator-invisible channel while passing benchmarks [23], an untrusted fine-tuning service that injects a payload before the adapter is committed, or a distribution intermediary that substitutes a package (caught by the package binding of Section 6). A compromised serving endpoint is out of scope: the certificate binds the committed checkpoint, not what an endpoint loads at inference (Section 9). The headline deployment is a third-party LoRA/PEFT adapter on a public base. By public we mean an open-weight model whose parameters are available to all parties (e.g. Llama, Qwen, GPT-2 on a model hub): the base weights and therefore any monitor derived from them (such as the QK map π or its augmented variant Mdep ) are public and fixed, and the only untrusted object is the adapter. Certifying the untrusted adapter against a trusted public base is the natural trust boundary of this deployment. In practice, a platform (a model hub or inference service) may provide the proving infrastructure, with the deployer’s own stakeholders verifying without weight access (Fig. 1); Section 9 states what changes when the base is not public. The confinement attestation problem. Given a public base model with value map V0 and a public linear monitor M , and an adapter ∆ = BA whose read factor is committed under a binding, hiding c and whose write factor B ships in the clear with the package (Section 6): construct a proof system in which the publisher convinces the verifier that ∆ adds no component readable only in the monitor’s blind subspace ker M (i.e. ker M ⊆ ker ∆), such that completeness and soundness hold and the transcript reveals nothing about (A, C) beyond c. The served model’s residual blind response should equal the public base contribution V0 restricted to ker M , computable by the verifier in the clear. The released model: base plus update. The served value map (the linear projection WV inside each attention layer, which determines what information the layer extracts from the residual stream) decomposes as Vsrv = V0 + ∆: a base value map V0 , a deterministic public function of the released public base model, plus a committed secret update ∆ (the shipped adapter; for a rank-r LoRA [24], a low-rank factorization ∆ = BA, with c binding the read factor A and the package root binding B together with c, Section 6). The attack surface is the update: an operator-invisible channel is what the publisher adds through ∆. Because the base model is public, its blind read V0 N against any public basis N of ker π is computable by every verifier in the clear: a property of an artifact everyone holds, not a concealed insertion. The certificate therefore attests the update’s contribution ∆N , pinning the served residual blind read at the public base floor V0 N (Section 4), which a low-rank update cannot drive to zero (Proposition 1(b)). Who computes the monitor. Where the monitor is computed sets the trust model. We target the public-base, secret-adapter case: the base is public, so the verifier computes the deployed monitor Mdep (the QK map plus its optimal in-kernel augmentation, Section 3) from the public base, with no access to the secret adapter and no choice left to the publisher, so it cannot be gamed to hide structure. The alternatives are weaker or costlier: a public fixed monitor (the base QK map) is verifier-computable but value-path-misaligned; a publisher-proposed monitor would itself need a ZK proof of its relation to the committed weights; a trusted-auditor or TEE monitor needs weight access.

deployer / proving platform

Open-weight base checkpoint

CompileMonitor

Mdep , µ

TypeTrain

(B, A, C)

CommitCert

(hpkg , P)

recompute Mdep

inference kernel

Package + Prove

admitted tensor

verified package

ServeGuard

VerifyBundle

stakeholder / weight-holding consumer

Figure 1: The ServeGuard pipeline. The deployer or its proving platform compiles the public monitor Mdep from the open base, trains monitor-typed factors, commits to the certified read factor and type witness, computes the package root hpkg binding the public write factor to c, proves the typed identity against a statement carrying that root, and ships the package. A stakeholder verifies without the certified read factor; the consumer’s admission-time guard recomputes Mdep and admits only bytes opening c as the typed identity. The dashed edge is the external serving-integrity obligation (Theorem 7).

The defense: confinement to the visible channel

The previous section established that detection from weights is uninformative and that the defense must be structural. This section gives the construction: confine the adapter to the monitor’s visible channel so no channel in the deployed monitor’s blind subspace ker Mdep can exist, and choose the monitor to minimize the residual cost (Fig. 1). The defense confines the value path to the public monitor’s visible channel (Fig. 1). Its objects form one canonical setup, stated once and used by every section that follows. Definition 1 (The concealment setup). On the residual stream X = Rdmodel (the hidden-state vector passed between transformer layers), a monitor is a public linear map M : X → Y into an observation space Y ; its blind subspace ker M is the set of perturbations the monitor maps to zero. A value map V (here, the value projection an adapter ships) carries the channel: the pair (M, V ) is live iff some payload is concealed (M δ = 0) and active (V δ = ̸ 0), and V is inert relative to M when it annihilates the blind subspace, Inert(M, V ) :⇐⇒ ker M ⊆ ker V ⇐⇒ V (ker M ) = {0},

(1)

equivalently (Theorem 1(b)) when it factors through the monitor, V = CM for some C: the value path reads X only through what the monitor exposes. A deployed monitor may post-process M x nonlinearly; every kernel statement below survives that composition, since δ ∈ ker M leaves M x, and hence any statistic computed from it, unchanged. The concrete instance we study monitors a single head’s query/key map π = [ WQ ; WK ] (written for the monitored head), an attention-pattern monitor of the safety-probing class [3, 50], and confines the layer’s value update WV (the value projection, stacked across the layer’s heads) against it; ker π is the per-head operator-invisibility floor. The certificate types the whole-layer value update against any declared monitor; the attention-block semantic corollary (Lemma 2) is head-local unless the monitor jointly covers every participating head (the joint-coverage predicate, Section G); Section 7 runs the end-to-end pipeline against the published SteerEdit attack and typed garak injection families.

Inertness is built, not tested. An inert value path actuates no concealed direction, so no live operator-invisible payload exists: inertness is exactly the negation of channel liveness (Theorem 1(a)). It is not a property an arbitrary adapter has (Section 7 shows honest fine-tunes are far from inert), so we do not test for it; we install it. Confinement makes inertness automatic. Let Πvis be the public projection onto the visible channel (ker M )⊥ (computable from the public monitor; it annihilates ker M ). Serve the value path through Πvis . Then for any value map V , the confined map V ◦ Πvis is inert: ker M ⊆ ker Πvis =⇒ Inert(M, V ◦ Πvis ),

(2)

because every concealed δ ∈ ker M has Πvis δ = 0 (Theorem 1(c)). The served value path therefore actuates no operator-invisible linear-carrier payload of the committed adapter, by construction, whatever V is: a structural guarantee about this channel class, not behavioral safety and not the operator-visible class (Section 9). For a LoRA update the construction is typed : build the read factor as A = CM (Section 4). The deployed monitor: QK plus its optimal in-kernel augmentation. Confining onto (ker M )⊥ discards the part of the value path that reads ker M , so the choice of M sets both the utility cost and the residual. The primary threat is defined by the QK map π, so the deployed monitor keeps π and augments it within its own blind subspace: the defender additionally monitors the q in-kernel directions that minimize the base value path’s residual gain, optimally the top rightsingular directions of V0 restricted to ker π (Theorem 5): a compiler-optimality statement, given the budget q, CompileMonitor’s augmentation is the best in the declared class and publishes its residual floor. The augmented monitor Mdep is a deterministic public function of the base model (Section 2). Every payload in the augmented blind subspace is still operator-invisible (ker Mdep ⊆ ker π, relative to the same fixed-point compilation of π, so the augmentation only expands coverage within ker π, never outside it), and the certificate proves the update inert exactly, so the served map’s residual blind read is pinned at the deployed floor, the exact public quantity ∥V0 Pker Mdep ∥ computed in the clear; Theorem 5 identifies its ideal-design value σq+1 (V0 Nπ ), and the gap between the two is itself public and verifier-computable; the residual floor is tunable down by raising q (Section 4). Two reference policies calibrate it. The gain monitor, whose visible channel is the top-k right-singular subspace of the base WV , is the unconstrained optimum for a different invisibility policy; its floor is σk+1 (WV ), exactly zero on the low-rank value paths of grouped-query attention. We use it as an oracle benchmark, not as the deployed policy. A data-aligned monitor (the activation covariance) is the negative control: free benign utility, largest residual (Section 7). The predicate family. The construction extends to other fixed public carrier subspaces: joint coverage of two monitors, named-trigger inertness, and their compositions. Each reduces to a homogeneous identity against a public subspace (the cheap ZK direction) and composes into a single certificate. The full predicate table and the harvested red-team certificates are in Section C. The next section turns this defense into a certificate: what the publisher proves, and why it is cheap.

The certificate: typed, real-rank-sound, bounded-residual

The defense is cheap to prove for one reason: the monitor is public, so what the publisher must show is a homogeneous identity between the committed secret and a public matrix. This section 6

gives that certificate: the typed form we deploy, its basis-dependent equivalent and that form’s load-bearing soundness condition, the field-versus-reals gap, and the public base floor that bounds the served residual. The certificate is the adapter’s type. By Theorem 1(b), inertness is exactly factorization through the monitor: ker M ⊆ ker ∆ ⇔ ∃ C : ∆ = CM . So rather than training an unrestricted adapter and afterwards proving a geometric property of it, the publisher builds the adapter monitortyped. For a LoRA ∆ = BA, construct the read factor as A = CM,

∆ = BA = (BC)M,

(3)

which is inert for any write factor B (Theorem 2): the adapter reads the residual stream only through what the monitor exposes, x 7→ M x 7→ CM x 7→ BCM x, and any x ∈ ker M dies at the first arrow. The publisher ships the adapter in the standard serialization (B, A) and commits to it; the type witness C is a private witness committed alongside A in the certificate commitment (Section 6), distinct from the checkpoint identity (B, A) the hub publishes. The certificate is the identity A − CM = 0 (4) over the committed A and witnessed C, against the public M : an honest typed adapter satisfies it by construction, while an A carrying any unconfined component fails it for every C. The check is genuinely linear in the committed secret against public coefficients: no nullspace basis to certify, no in-circuit rank, no spanning check, and no deficient-basis attack surface. The identity is small (r × dmodel entries with inner dimension rank M ), so a circuit can check it in full (the public monitor baked into the verification key) or probe it at 10 challenges fixed after the commitment; both realizations, and what each adds to the soundness error, are in Section 6. The equivalent zero-product, and its spanning condition. The basis-dependent equivalent names a public matrix N ∈ Rdmodel ×b whose columns span the blind subspace ker M (b = dmodel − rank M ) and checks ∆N = 0, which equals inertness exactly when the columns of N span all of ker M (Lemma 4). This form carries a load-bearing precondition the typed form does not have: if N misses part of ker M , an adversary who knows the deficient N ′ ships a map reading an omitted direction, passing V N ′ = 0 while non-inert (the generic failure, not a corner case (Theorem 8)). A verifier using this form must therefore establish M N = 0 and rank N = dmodel − rank M in the clear (the rank equality alone fixes the dimension, not the subspace). We use the zero-product form where the subspace is the given object rather than a computed kernel (the named-trigger predicate, whose N spans a public trigger family (Table 4), and the falsification suite, which exercises the deficient-basis attack (Section 7)) and the typed form (4) as the deployed certificate. The deployed monitor is the security object. The circuit reasons over Fp ; the model is real. We close that gap not by approximating an ideal monitor but by declaring the deployed finite-precision monitor Mdep to be the monitor: it is a bounded public fixed-point matrix, part of the published monitor policy (Section 6), and its blind subspace ker Mdep is the certified object. Weights are fixed-point rationals (as are the shipped factors, built on the same encoding lattice) and the circuit’s range checks confine every entry and product of (4) to the signed integer range, so A = CMdep is a genuine integer identity and inertness against Mdep is exact: for every δ ∈ ker Mdep , ∆ δ = 0, with no tolerance and no prover-chosen slack. There is no field-computed nullspace whose rank or lift would need interpretation (that semantic burden is one reason the zero-product form

is not the deployed one: its basis is computed over Fp , whose correspondence to the real kernel needs a rank-preservation argument the typed form never raises). A deployer who instead wishes to name an ideal real-valued monitor and serve its finite-precision compilation pays an explicit, optional tolerance (7), derived in Section F; the deployed guarantee against Mdep needs none of it. Theorem 3 gives the corresponding bound for the zero-product form. The residual is the public base floor. The update certificate is exact, so by Lemma 1 the served map’s blind read equals the base’s own: for any public monitor with blind-subspace basis N , ∥Vsrv N ∥2 = ∥V0 N ∥2 , a public quantity the verifier computes from the base model in the clear. This equality is exact for the deployed quantized monitor Mdep ; for the ideal real-valued monitor the encoding bound (7) adds an explicit tolerance: ∥Vsrv Pker M ∥2 ≤ σq+1 V0 Nπ + εenc , (5) where εenc = ∥BC∥ ∥Mfp − M ∥, with Mfp the ideal monitor’s fixed-point compilation, is the publicly bounded encoding resolution (Section 6). Under the deployed monitor Mdep (the QK map plus q optimal in-kernel directions), Theorem 5 makes σq+1 the smallest residual any ideal q-direction augmentation preserving the ker π threat can achieve; the deployed compiled floor tracks it measurably (at most 0.25% off, median 0.16%, over the proved GPT-2 layers, a public gap), dialed down by raising q; under the gain oracle it is σk+1 (WV ), reaching exactly zero on the low-rank value paths of grouped-query attention (Section 7). Here and below ∥·∥ denotes the operator/Euclidean 2-norm, written ∥·∥2 for emphasis; adapter occupancy (Section 7) uses the Frobenius norm ∥·∥F . A passing certificate then bounds any downstream readout: for a linear readout G (an unembedding row, a logit map) and concealed δ = N c, ∥G Vsrv δ∥ ≤ ∥G∥ ∥V0 N ∥ ∥c∥

(6)

(Theorem 4), the update contributing exactly zero. Exact base closure is the floor’s zero endpoint; the public base floor is the deployable interior. Section 7 measures both floors. Circuit scale. The committed object is the adapter, not the model: a rank-r LoRA value adapter has O(r(d + dmodel )) secret entries, the witness C adds r · rank M , and the certificate is one small matrix identity against the public M . On GPT-2 (dmodel = 768, d = 64) the deployed monitor has rank rank M ≪ dmodel while the blind subspace has dimension 640; a rank-8 adapter has 6656 secret entries against 49152 for a dense ∆WV . Adapter-scale attestation is thus plausible on present proving stacks; Section 5 states the theorems that make a passing certificate mean what it claims, and Section 6 turns them into a zero-knowledge proof.

Soundness

The certificate of Section 4 is a statement about committed weights; here we state the theorems that give it meaning. All maps are linear over a field; each statement carries its proof idea inline, with auxiliary statements and a machine-checked formalization in Section C. Inertness has three faces: a security property, a normal form, and a construction. The first says what a passing certificate rules out, the second is what the prover actually proves, and the third is why a publisher can install the property instead of testing for it. Theorem 1 (Inertness: channel-absence, factorization, construction). For a monitor M and value map V : (a) Channel-absence. Inert(M, V ) ⇔ ¬ ∃ δ : M δ = 0 ∧ V δ = ̸ 0. (b) Factor-through. 8

Inert(M, V ) ⇔ ∃ C : V = C ◦ M . (c) Construction. If ker M ⊆ ker Πvis then Inert(M, V ◦ Πvis ) for every value map V ; the public projection onto (ker M )⊥ satisfies the hypothesis. Proof idea. (a) unfolds ker M ⊆ ker V . (b) is the universal property of the quotient: an inert V is constant on the fibers of M , so it descends to a well-defined V̄ : Rdmodel / ker M → Rdv and lifts back through any splitting. (c) for δ ∈ ker M , Πvis δ = 0, hence (V ◦ Πvis )δ = 0. The three parts carry three distinct claims. Part (a) is the security meaning: an inert value path admits no concealed-and-active payload, which turns an existential impossibility (no hidden payload exists) into a checkable algebraic inclusion (ker M ⊆ ker V ), the property prior detection methods attempt to test for but cannot certify. Part (b) is the basis-free normal form, naming no N : the value path reads the residual stream only through what the monitor exposes, so it needs no spanning check and has no deficient-basis attack surface, and two inputs the monitor cannot distinguish receive the same value-path output. Part (b) is also what makes the certificate cheap: the identity A = CM is linear in the committed secret against a public matrix, exactly the structure zero-knowledge proofs are built for, and categorically distinct from a magnitude bound, which cannot read the kernel relation an operator-invisible payload hides in [40]. Part (c) is why the property can be built rather than tested: serving V0 + ∆ ◦ Πvis confines the publisher’s contribution while leaving the public base V0 untouched. Which map the certificate should attest, the update or the whole served map, is settled by splitting the served map into its public and secret parts. Definition 2 (Served map: base plus update). The served value map is Vsrv = V0 + ∆: a public base map V0 (a deterministic function of the base model) plus a committed secret update ∆ (the shipped adapter; ∆ = BA for a rank-r LoRA, commitments as in Section 2). Throughout, Vsrv is the value map of the certified released checkpoint; binding it to the model a serving endpoint actually loads is a separate obligation we scope in Section 9. Lemma 1 (Residual is the public base floor). Vsrv N = V0 N + ∆N , and if the update is inert (∆N = 0) then Vsrv N = V0 N . The right side is public: the verifier computes V0 N from the base model and the public N , so an inert update pins the served residual at the base floor in every norm, with no prover-chosen tolerance. Proposition 1 (Attest the update, not the served map). (a) Isolation. If Inert(M, ∆) then Inert(M, Vsrv ) ⇔ Inert(M, V0 ). (b) Rank obstruction. If rank ∆ ≤ r and rank(V0 N ) > r, then Vsrv N ̸= 0. Proof idea. (a) with the update inert, Vsrv δ = V0 δ for every δ ∈ ker M . (b) if Vsrv N = 0 then ∆N = − V0 N , so rank(V0 N ) = rank(∆N ) ≤ rank ∆ ≤ r, contradicting rank(V0 N ) > r. Together these fix the object to certify. By (a) the publisher’s update neither opens nor closes a channel the public base lacks, so attesting Inert(M, ∆) (equivalently the typed factorization ∆ = C ′ M , Theorem 1(b), or the zero-product ∆N = 0 against a spanning basis, Lemma 4) certifies precisely what the publisher adds. By (b) the alternative is unavailable: no rank-r update makes the served map blind-inert once the base reads the blind subspace at rank above r, so “the served model reads nothing blind” is unachievable at adapter scale. We therefore confine the update (Theorem 1(c) on ∆) and report the base floor, rather than attempt an infeasible whole-map closure. Theorem 2 (Typed LoRA is inert by construction). If a LoRA’s read factor factors through the monitor, A = CM , then ∆ = BA is inert for any B. Confinement is then a property of the adapter’s type: the publisher ships and commits the standard factors (B, A), holds the type witness C ∈ Rr×s (s = rank M ) privately, and the certificate is the identity A − CM = 0, linear in the committed 9

secret against the public M . Conversely every rank-r inert update admits such a factorization (Theorem 1(b) applied to ∆, then a rank factorization), so the typed form loses no generality at the dense-update level, up to refactorization of the same ∆. The qualification is real: cancellation through B can make BA inert while A itself is not, so typing the shipped read factor is the stronger per-factor property, and a publisher training under confinement chooses this parameterization from the start. The basis-dependent zero-product equivalent and its load-bearing spanning precondition (Section 4) are stated and proved in Section C. The next two facts bound the residual: the field-versus-reals gap, and the behavioral shift of an ε-inert defense. Theorem 3 (Encoding tolerance). For bounded operators with Vfp ◦ Nfp = 0, ∥V ◦ N ∥ ≤ ∥V − Vfp ∥ ∥N ∥ + ∥Vfp ∥ ∥N − Nfp ∥. The next lemma grounds the abstract maps in an actual attention block. Lemma 2 (Attention instantiation). Fix an attention layer with post-LayerNorm input x, the monitored head’s query/key map π (Definition 1), base value map V0 = WV , output map WO , and value update ∆. For a payload δ ∈ ker π (so WQ δ√= WK δ = 0 for the monitored head): (i) the monitored head’s attention weights softmax(QK ⊤ / d) are unchanged when δ is added to the input of a token j, since its Q, K do not read δ; (ii) with that head’s (unchanged) attention matrix α, its output contribution at token i shifts by αij WO (V0 + ∆)δ, which factors through (V0 + ∆)δ. Hence an update with ∆δ = 0 contributes nothing and the residual shift is the base term αij WO V0 δ, bounded by Theorem 4 with readout G = WO . The semantic reading is head-local: another head whose query/key maps read δ may change its own routing. If the declared monitor jointly stacks every head’s query/key map (the joint-coverage predicate, Section G), a δ in the joint kernel fixes every head’s routing and the block-level claim closes. Proof idea. Write tokens as columns X; the monitored head’s Q, K are linear in X, so for δ ∈ ker π that head’s queries and keys are invariant and its attention α is unchanged. That head’s output ⊤ contribution is WO (V0 + ∆)X α⊤ ; adding δ at token j changes it by WO (V0 + ∆)δ e⊤ j α , i.e. αij WO (V0 + ∆)δ at output token i. Theorem 4 (Bounded behavioral shift). For any downstream linear readout G, value map V , and column-orthonormal basis N of the blind subspace, and any concealed payload δ = N c (so ∥δ∥ = ∥c∥), ∥G V δ∥ ≤ ∥G∥ ∥V ◦ N ∥ ∥c∥. Instantiating with the served map, an inert update pins ∥Vsrv N ∥ = ∥V0 N ∥ (Lemma 1), the public base floor: under the deployed compiled monitor this is the exact public quantity ∥V0 Pker Mdep ∥, whose ideal-design value is σq+1 (V0 Nπ ) (Section 4), at most σk+1 (WV ) under the gain oracle; the update’s own readout shift is exactly zero (∆N = 0), and the endpoint V0 N = 0 makes every readout invariant to concealed payloads. The floor depends on the monitor. The deployed monitor augments the QK map within its own blind subspace, expanding coverage of ker π without monitoring outside it (ker Mdep ⊆ ker π), and there is a best way to do so.

Theorem 5 (Optimal in-kernel augmentation). Let Nπ have orthonormal columns spanning ker π. If the defender monitors, besides π, a q-dimensional T ⊆ ker π (leaving residual blind subspace ker π ∩ T ⊥ ), then the smallest achievable residual gain of the base value path is min V0 Pker π∩T ⊥ = σq+1 V0 Nπ , T ⊆ker π, dim T =q

attained when T spans (through Nπ ) the top-q right-singular directions of V0 Nπ . This is a lower bound among augmentations of the stated size and nesting: no q-direction augmentation within ker π can achieve a smaller residual, so the all-layer frontier of Section 7 plots the ideal-design optimum for this monitor class. One caveat this makes explicit: since ker Mdep ⊊ ker π, a typed adapter reads the augmentation directions T = ker π ∩ (ker Mdep )⊥ , which a bare attention-pattern probe (a function of π alone) does not see. The confinement guarantee is therefore relative to the deployed Mdep : it holds when the served monitor is Mdep itself, augmentation rows included, and reduces to ker π-confinement only if q = 0. The frontier is the graded form of an exact-certification budget: the smallest q at which σq+1 (V0 Nπ ) reaches zero is dim V0 (ker π) = rank[ π; V0 ] − rank π, the minimum number of monitored directions any in-kernel augmentation needs before the base value path’s blind channel closes exactly. Below that endpoint the curve prices every partial budget, so a deployer reads off the residual purchased by each additional monitored direction.

Zero-knowledge realization

The theorems of Section 5 establish what a passing certificate means; this section shows how to prove it in zero knowledge without revealing the read factor it certifies. The certificate is a commit-and-prove statement: commit once to the certified read factor and type witness, then prove that the committed read factor is monitor-typed (A − CMdep = 0 against the public deployed monitor). Commitment. The publisher commits to the read factor A and type witness C with a hiding commitment so it leaks nothing about the committed pair: a randomized hash commitment c = H(domain, ρcom , serialize(A, C)) with a private high-entropy salt ρcom , canonical length-prefixed serialization, and domain separation. This is the commitment the measured circuit implements (the salt is a private witness of the in-circuit hash, Section 7), with a blinded KZG [26] or Pedersen commitment the alternative. The commitment c is a certificate commitment: it binds the read factor A and type witness C that the proof checks, not the full checkpoint (B, A); B is not part of the circuit and does not need commitment-binding. The checkpoint identity (the artifact a hub publishes) remains (B, A) in whatever serialization the deployment uses; a separate binding of c to the checkpoint hash, or a Merkle proof opening A from the checkpoint, ties the certificate to a specific shipped artifact. What is proved. One public-linear fact about the committed secret: the shipped read factor is monitor-typed, A = CMdep for some C, so the update BA is inert by construction for any write factor (Theorem 2). Two realizations check it, neither with an in-circuit rank or nullspace. A custom circuit bakes the public Mdep into the verification key and checks the identity in full, with no challenge and no probabilistic term. The measured stock-toolchain instantiation keeps the circuit minimal and probes the committed typed identity directly: the public inputs are a challenge vector r and the verifier-recomputed m = Mdep r, the circuit checks (A − CMdep ) r = 0 over range-checked 11

fixed-point integers with (A, C, ρcom ) the committed preimage, and the challenge is derived from the commitment (Theorem 6). Passing certifies the per-factor typed relation A = CMdep (not merely dense-update inertness) because B is not in the circuit and cannot cancel an unconfined component of A. Because A is serialized at the product scale (the input and parameter scales are set equal, so A’s entries carry the two fractional-bit blocks of CMdep ), the checked relation is the exact scale-balanced integer identity AZ = CZ (Mdep )Z with no residual scale factor; the no-wrap range checks (below) keep every accumulated product inside the signed range, so a field zero is an integer zero. Crucially, Mdep never enters the circuit as prover-supplied data: the verifier recomputes m from the public monitor in the clear, so a prover cannot substitute a smaller monitor (the deficient-basis attack surface of the zero-product form, Theorem 8, does not arise). Commit-and-prove soundness. Composing the standard primitives gives the end-to-end guarantee. Fix a public statement st comprising the base-model hash; Mdep or its digest; the package root hpkg (computed before proving, Section D); the dimensions dmodel , d, and r; the fixed-point scale and signed range; the circuit version; and the layer/head/tensor identifier. The publisher publishes the hiding commitment c, and the challenge is 10 independent probe vectors rj = H(challenge-domain, st, c, j), probe j expanded from its own domain-separated random-oracle seed, its coordinates successive rejection-sampled outputs uniform over the bounded integer range S (|S| ≈ 213 , bounded so every scaled product stays inside the circuit’s exact no-wrap range: each intermediate obeys a checked bound, and the per-intermediate ledger, worst margin 186 bits below p/2 on the measured configuration, is in Section D; larger probes overflow the range and break the identity), fixed after c so the committed factors cannot be chosen against a known probe. Soundness then amplifies with the probe count 10 rather than the per-probe range. Theorem 6 (Commit-and-prove soundness). Under commitment binding (εbind ), SNARK knowledge soundness (εKS ), the in-circuit range checks (the no-wrap condition below), and the random-oracle challenge, an accepting proof implies that the read factor committed under c is monitor-typed (A = C ′ Mdep for some C ′ , an exact identity on the encoding lattice), hence the update BA formed with any write factor B is inert, except with probability at most εbind +εKS +qH |S|−10 for a qH -query prover. Under commitment hiding (the salted hash modeled in the random-oracle model; a Pedersen or blinded-KZG commitment gives the standard computational-hiding statement) and SNARK zero knowledge, the transcript, st together with the hiding commitment c and the package root hpkg , both of which the verifier already holds, reveals nothing further about (A, C); the write factor B is publicly shipped, hash-bound by hpkg , and outside the hiding claim. Three levels must not be conflated: (i) the algebraic identity and its all-probes form (Lemma 3); (ii) the deployed circuit probes the committed identity at 10 post-commitment challenges, falseaccepting with probability at most |S|−10 ≈ 2−130 plus the qH |S|−10 grinding term (Lemma 3); a field-native realization with a uniform-Fp challenge (or Mdep baked into a custom halo2-lib verification key, checking the identity in full) sharpens the per-certificate term to 1/p at the same proof size; (iii) knowledge soundness and zero knowledge are the SNARK’s, and the commit-andprove link binds the checked witness to c. The no-wrap condition (every accumulated fixed-point product stays within the signed range of Fp , so a field zero is an integer zero) is enforced in-circuit by the range checks, a checked constraint rather than an assumption. Proof system. The predicate is fixed-point linear algebra plus a prover-supplied witness, so a Plonkish system with lookup arguments [5] fits: native lookups make the dominant cost (fixed-point range checks) cheap, a universal structured reference string is reused across adapter shapes (one 12

trusted setup; a per-circuit Groth16 ceremony [22] run by the publisher alone would leave the publisher holding the circuit trapdoor, with which it could forge proofs for that circuit), and the constant-size proof with fast verifier suits an attestation posted beside a checkpoint. The commitand-prove link binding the predicate to c follows the modular CP-SNARK line [6, 7, 30]; reducing a kernel statement to a witness identity is folklore [14]; the secret-artifact-versus-public-specification structure mirrors ZK-CEC [41] and the ZK-UNSAT line [29]; and the fixed-point-after-matmul soundness follows Range-Arithmetic [38]. Because the certificate is matmul-only (a matrix product and a subtraction, with no rank or kernel operator), it is directly expressible as an ONNX graph, so a standard Halo2-backed ZKML compiler (EZKL [49]) proves it as-is; we use this for the feasibility benchmark (Section 7), with a custom halo2-lib circuit the later optimization. Verifier preprocessing. The “hard part is public” argument has a concrete cost: constructing Mdep from the base (weight extraction, restricted SVD, lattice quantization, challenge m = Mdep r) takes 86 ms per layer on GPT-2 (dmodel = 768), and 31–1688 ms across the four models, dominated by the restricted SVD; model loading adds 1–4 s, amortized across layers and sessions. Realized prover. We implement the certificate end-to-end on a Halo2 + KZG backend: a complete proof that a GPT-2-scale value adapter satisfies the typed identity proves in seconds with a millisecond verifier (measured in Section 7, Table 1d); the O(r(d + dmodel )) secret and single small matrix identity (Section 4) are what make this cheap. The commit-and-prove binding uses the hiding commitment above: the factors and private salt ρcom are committed by an in-circuit Poseidon hash exposed as a public instance, so one verification checks the certificate and that it was computed with the adapter committed as c; under Poseidon’s collision resistance no efficient publisher finds a colliding adapter (the binding property), while the commitment’s hiding (that c reveals nothing about the factors beyond st) is a separate assumption on the salted Poseidon commitment, for which the high-entropy salt ρcom supplies the required preimage entropy; collision resistance alone does not give hiding. The in-circuit hash dominates the binding cost (a one-time publisher cost, Section 7), with a KZG polynomial commitment [26] or a custom halo2-lib circuit the remaining speedup.

6.1

The system contract

Two verifier-side procedures close the loop; Section D gives the full protocol interface. VerifyBundle runs the per-layer check on all L layers and recomputes the package root hpkg , which binds each layer’s shipped write factor H(Bℓ ) together with that layer’s proof commitment cℓ . ServeGuard(Ã, C, Mdep ) is run by the weight-holding consumer on the bytes it actually serves: it admits Ã only if Ã opens the commitment as the committed typed identity Ã = CMdep , checked exactly over the integer lattice, with Mdep recomputed from the authenticated base rather than taken from a shipped matrix (closing the deficient-monitor substitution). The check is exact and unconditional: no prime, no field reduction, no acceptance threshold, hence no slack an unbounded write factor could amplify, and no cryptographic assumption on the check itself. The composition of the two is the system’s contract. Theorem 7 (Two-part confinement: bundle plus guard). Fix the authenticated base and the deployed monitors Mdep [ℓ]; write ServeGuardℓ for the guard run with (W0 , policy, cℓ ) on the served bytes and sidecar of layer ℓ. (a) Served integrity (exact, unconditional): if ServeGuardℓ = 1 for the adapter bytes presented at every protected layer, then the canonical tensors Ãℓ the guard returns satisfy ∀ℓ, ∀δ ∈ ker Mdep [ℓ], Bℓ Ãℓ δ = 0, and the served residual on each blind subspace is the authenticated public base floor (Lemma 1). (b) Committed-package soundness (computational): if 13

VerifyBundle = 1, then except with probability L (εbind + εKS + qH |S|−10 ), the adapter committed under hpkg factors through the deployed monitor at every layer (Theorem 6). Proof idea. (a) composes Theorem 2 at each admitted layer with Lemma 1; the guard’s integer identity check is exact, so no slack enters. (b) applies Theorem 6 per layer under a union bound over the L certificates; the package root binds the proof’s own commitment, so no unlinked commitment splits the attested and shipped factors. The two parts have deliberately distinct reach, and conflating them overstates the guarantee. Typedrelation soundness binds the committed adapter: the proof certifies that the A in c, the same c the package root binds, is typed, which is what a remote verifier who never sees the read factor obtains. Because one commitment serves both the proof and hpkg , there is no unlinked second commitment a publisher could split. What it does not do is bind the deployed bytes to c: a publisher could ship an A′ that does not open c. Catching that is ServeGuard, which opens c against the served (A′ , C, ρ) and rejects any other factor, untyped or typed but not the committed one, whatever a malicious publisher or intermediary shipped. The two conclusions have different strengths: exact integer typing gives unconditional confinement of the admitted tensor, while equality with the previously certified factor is computational, under commitment binding, exactly the split of Theorem 7. ServeGuard certifies the tensor it is handed ; the executed-tensor binding is scoped in Section 9. A publisher who needs the full update ∆ = BA confidential needs a different realization; what this one buys is that the confinement property is checkable by a verifier who never sees A.

Evaluation

The previous sections constructed the defense, proved its soundness, and described a zero-knowledge realization. This section asks whether it works in practice: does the certificate decide correctly, does confinement cost utility, does the prover scale, and does the defense hold against an adaptive adversary? All numbers are macro-guarded from the released scripts. Falsification suite. The evaluation escalates through an adversary hierarchy: naive hidden edit, published stealth edit, certificate-aware attacker, package substitution, served-factor substitution. First, the certificate is tested against a suite of structural attacks: a confined value map is accepted; an OBVS construction is rejected (7.7 orders of separation on GPT-2); a partly visible backdoor is rejected at every mixing coefficient; an adaptive payload anywhere in ker π is caught by a spanning basis (Theorem 8); and the tolerance bound is verified numerically. A magnitude/rank/sparsity bound [40] calibrated to accept an honest adapter of the same norm and rank also accepts an OBVS adapter; the confinement certificate rejects it (residual 2.2). Adaptive adversary and published attacks. SteerEdit [47] compiles activation steering into a persistent null-space-constrained weight edit; instantiated on the value path, its stealthy trigger is 88% inside ker π and the certificate ZK-rejects it (4.4 orders from honest); evading the certificate forces visibility (0.26 → 0.54). Our re-implementation of the supervised spectral detector of [35] achieves ROC-AUC 0.96 on loud payloads but degrades to 0.65 under stealth and needs a labeled reference; the certificate is label-free (its reference is the verifier-declared public monitor) and exact. A defense-specific adaptive attacker targets the certificate’s residual budget: the optimal residual attacker saturates σk+1 (WV ), capped below the unconfined σ1 by 0.5–1.1 orders as coverage rises, and driven to zero by exact confinement.

Detection from weights is uninformative. On GPT-2 (dim ker π = 640 of 768), a trained LoRA places 88% of its value-path norm in ker π; a random adapter, 91%; only an adapter built inert by hand sits at the floor; any low-rank adapter concentrates there by geometry, so no kernel-activity test separates honest from malicious. A real published adapter (Stanford-Alpaca gpt2 alpaca-lora, 87% kernel-active) confirms it; confining and then tampering separates at 6.2 orders. A targeted operator-invisible manipulation, caught and removed. The channel’s demonstrable use is an integrity manipulation of the output, and the certificate removes it. We build a value-path payload that reads u ∈ ker π (so WQ u = WK u = 0) and writes toward a chosen token’s unembedding direction, shifting its logit by 31× the base value path’s natural variation at visibility 0. The certificate rejects the tampered adapter (residual 0.98); confining the released update accepts it (residual 1.4 × 10−6 ) and drives the manipulation to zero. This is an integrity channel (Theorem 4 bounds the shift), not a demonstrated content backdoor. The blind subspace is architecture-dependent. Under MHA, heads’ visible channels sit in general position (overlap 1.00); under grouped-query attention (GQA) [1], key sharing collapses a group’s joint visible channel to a fixed low dimension, a measured 384-dimensional group-shared blind floor on Qwen2.5-0.5B; the covering penalty is entirely off-circuit (prover cost is flat in blind dimension). We report the measured frontier; the general group-level observation geometry is outside this paper. Inert-by-design is nearly free, and utility does not select the monitor. Weight-space detection fails because a benign adapter uses ker π; the defense is cheap because it does not need it. We train value-path LoRAs on an instruction task (Qwen2.5-0.5B-Instruct [36], held-out response perplexity), confined to a declared monitor’s visible channel (the deployable construction, trained-in rather than projected after) in a factorial design over the three monitors (gain, the augmented QK policy, and a random control), three visible budgets, two ranks, and 3 seeds (Table 1a). Confinement is not a no-op: it forces ∆N = 0 (the exact update certificate of Proposition 1(a)), killing the channel the publisher could add. Yet task utility survives, and, the design’s decisive finding, survives equally under every monitor : at 25% visible (three-quarters of the residual stream blind), all three recover 98–99% of the unconfined adapter’s gain (standard deviation ≤ 2% over 3 seeds, Table 1a). Matched within each budget–rank–seed cell, the largest monitor-pair difference is 0.13%, a two-one-sided-test equivalence at ±1% over 18 pairs, far tighter than the security separation below. In these experiments, low-rank benign adaptation re-expresses across every sufficiently large subspace tested. But the certified residual does select the monitor. Utility being monitor-agnostic is exactly what makes the security argument sharp: the monitors differ not in trainability but in the certified residual they leave. At the same 25%-visible operating point the gain monitor’s residual is the public floor σk+1 (WV ) = 0 (exact closure on this GQA value path), the augmented-QK residual is 43% of the unconfined blind read, and the random monitor leaves 89%, and still 60% even at 75% visible (Table 1a). Two hypotheses separate cleanly: low-rank fine-tuning repacks into many subspaces (so utility is flexible), but only gain-aware selection minimizes the worst-case residual (so security is not). In the factorial design, monitor identity explains 0.2% of the variance in utility recovery but 85% of the variance in certified residual (η 2 , one-way by monitor); the same factor that is irrelevant for trainability is dominant for security. The gain co-design earns its place on the residual, not on training cost, and a defender who picks the monitor for utility alone, or at 15

(a) Safety–utility DoE

(b) Augmentation frontier

Monitor vis. util. rec. resid.

Model

gain gain gain qk-aug qk-aug qk-aug random random random

GPT-2 (MHA) SmolLM2 (MHA) Qwen-0.5B (GQA) Qwen-1.5B (GQA) Qwen-3B (GQA) Qwen-7B (GQA) Llama-1B (GQA) Llama-3B (GQA)

.25 .50 .75 .25 .50 .75 .25 .50 .75

.991 .988 .996 .984 .985 .994 .984 .985 .997

0 0 0 .43 0 0 .89 .76 .60

k0.01

κ0.1

640 533561 638638 516 638 1918 1920 15181588 1914 1456 1910 768 128128 128128 128 128 256 1280 256256 256256 256 1792 256256 256256 256 256 3328 512512 512512 512 512 1920 512512 512512 511 512 1024 2816 10241024 1023 10241024

83% 79% 17% 20% 14% 15% 27% 36%

(d) Prover cost (Halo2/KZG, BN254)

Model

dmodel dim V gainu QKu gainσ QKσ

Configuration

GPT-2 (MHA) Qwen-0.5B (GQA) SmolLM2 (MHA) Qwen-7B (GQA)

768 896 2048 3584

Typed, full-layer Zero-prod., per-head Zero-prod., layer Salted commit

768 128 2048 512

.08 0 .21 0

.29 .32 .72 .08

0.64 0 0.76 0

k0.1

3.16 0.34 3.64 0.30

Prove Verify Proof 6.4 s 96 ms 5.5 KB 6.4 s 95 ms 5.5 KB 6.4 s 96 ms 5.5 KB 48 s 347 ms 6.0 KB

Table 1: Empirical results. (a) Utility recovery (mean, 3 seeds, rank 16) is high and monitor-agnostic; certified residual separates monitors (exact 0 for gain, large for random). (b) Monitoring complexity kτ = medianqq75 25 directions for σq+1 /σ1 ≤ τ ; κ0.1 = k0.1 /b. GQA saturates at dim V ; MHA needs most of b. (c) Confinement disruption u (the artifact’s relative value-path output-change proxy; not task utility, which (a) measures) and worst-case residual (σk+1 ) at ≈ 13 blind. Gain is tighter on every model and exact (0) on GQA. (d) Cost is near-flat in rank (r ≤ 32); commit-and-prove hash dominates. random, gets a certificate that certifies almost nothing. A second task (Dolly-15k [11], open-domain instruction) replicates the separation: 98–99% utility recovery across the three monitors at 25% visible, while the certified residual fractions are again 0, 43, and 89% (η 2 : 12% utility, 81% residual), so the conclusion is not an artifact of one task. The deployed policy: QK plus its optimal in-kernel augmentation. The deployed monitor expands the QK operator’s coverage within ker π via the in-kernel augmentation of Theorem 5, whose ideal-design residual is σq+1 (V0 Nπ ), the base value path’s gain on the directions actually hidden from that single-head QK monitor (its exact ker π, distinct from the visible-dimension sweep of Table 1c). On GPT-2 that gain is 6.1 un-augmented and the base path is full-rank on ker π (rank 640; the budget is reader-relative, and this is the whole-layer value reader V0 , while a single head’s value reader caps its budget at the head dimension d), so augmenting 160 optimal in-kernel directions cuts it only to 1.8: closing the QK channel is a bounded-residual tradeoff, not free. The augmentation frontier is architectural, and tracks nkv . The 6.1 → 1.8 point is one head; the ideal frontier σq+1 (V0 Nπ ) is exact (Theorem 5; the deployed floor is its fixed-point compilation’s kernel restriction, itself public), so we compute it for every layer and query head of 8 checkpoints, spanning two attention layouts, four families, 0.1–7B, and Q : KV from 3 : 1 to 8 : 1. We report the monitoring complexity kτ = min{q : σq+1 /σ1 ≤ τ }, the budget for a 1/τ attenuation of the base blind read (Table 1b, Fig. 2).

The split is architectural and sharp. On the multi-head-attention paths the frontier is high-rank: the median head needs 533 of 640 directions on GPT-2 for a 10× attenuation, 100× is unreachable for most heads (10% attain it), and κ0.1 = k0.1 /b is 83% (GPT-2) and 79% (SmolLM2). On every grouped-query path it collapses at that model’s own value-path rank nkv d, with interquartile range zero. That ceiling is algebraic (V0 Nπ has at most nkv d nonzero singular values); what the sweep adds is that it is attained in all six cases, so no cheaper-than-rank ideal monitor exists, and that k0.1 = k0.01 there. The fraction is therefore a function of Q : KV , not a constant of the architecture class: Llama-3.2 at 3 : 1 and 4 : 1 costs 36% and 27% where Qwen2.5 at 6 : 1–8 : 1 costs 14–20%; a single-family sweep reports this as one GQA number. The gain-oracle benchmark, across architectures. How far could monitor–value co-design go if coverage were unconstrained? Aligning the monitor’s visible channel to the value path’s high-gain subspace strictly dominates QK: the gain monitor confines at a fraction of QK’s disruption cost and bounds the residual 5× tighter (13× below σ1 (WV ) = 8.0 on GPT-2), on all 4 model configurations we test (Table 1c). Its residual equals the public base floor σk+1 (WV ), verifier-computable from the base WV and tunable; a data-aligned monitor confines cheaply but leaves the largest residual, so co-design must target gain, not data. Detection stays uninformative on every model (a trained honest LoRA is 83–88% kernel-active). Grouped-query attention makes gain-monitor closure easier: its value path is inherently low-rank (dim V = nkv d = 128), so σk+1 (WV ) reaches zero: exact closure against the gain monitor that the high-rank MHA path does not admit. This is closure of the gain-oracle’s channel; the query/key operator’s own residual stays nonzero (Table 1c), so the two are distinct policies. The pattern holds at deployment scale: on a 7B GQA model the gain residual is again exactly zero, at single-digit-percent utility cost, while the operator residual stays nonzero (Table 1c). The update infeasibility (Proposition 1(b)) is unchanged. The prover is cheap (Halo2 + KZG). We prove the certificate end-to-end on a Halo2/KZG backend (BN254). The deployed circuit proves the committed typed identity at a post-commitment challenge (y = Ar − Cm with m = Mdep r, Section 6; the committed factors A and C are the secret witness, and the public output is checked against zero). The shipped factors are fixed-point-exact (A = CMdep on the encoding lattice), so the honest output is exactly zero in the field, not merely small (Table 1d). A tampered adapter that reads a direction hidden from Mdep yields a nonzero public output (99.7 against the honest exact 0), so the verifier’s zero-check rejects it. The equivalent zero-product form [16] y = B(A(N r)) (used by the named-trigger certificates; same 10-probe soundness ≈ 2−130 , Lemma 3) measures comparably. Because the predicate is matmul-only (no execution circuit, no in-circuit rank), it is cheap (Table 1d), and cost is near-flat in the adapter rank over the measured range: the certificate is the single matrix product A − CMdep , whose constraint count is O(r(dmodel + rank Mdep )) but which stays inside the same padded circuit for all r ≤ 64, so measured prover time and proof size rise only marginally with r (Table 1d). A whole checkpoint’s value adapters are 12 independent per-layer certificates bound by one package root, which the verifier recomputes and which any swapped layer changes (Section 6.1). Across the 12 GPT-2 value monitors every typed factor passes and every live-channel substitution is rejected, including the congruent ÃZ + pE attack that defeats a GF(p) rank check (a float projection residual, reported only for intuition, separates honest from substituted by 6 orders). Admission is cheap at serving time: the lattice parse and integer identity take 31 ms per layer, the one-time commitment-opening recomputation 1.2 s per layer at load, and the private sidecar is 18 KB per layer. Measured on GPT-2, the salted commit-and-prove package proves in 555 s (plain 76 s), verifies in 4.1 s, and ships a 70 KB bundle; aggregating the per-layer commitments into the root costs 0.03 ms, while the in-circuit

commitment links dominate the 555 s publication cost. Both the guarantee and these figures cover the value path, not the Q/K/O or MLP projections; certificate and checkpoint costs sit well under the minutes a distilled GPT-2 inference circuit takes on a comparable Halo2-based toolchain [9], the trace-proof cost barrier full-model inference faces [8]. We also exercise the commit-and-prove binding of Section 6 on the measured commitment [21]: a tampered read factor yields a different c (binding rests on Poseidon’s collision resistance; the test exhibits the mechanism, not the assumption), and re-committing the same adapter under a fresh salt yields a different c, confirming the implemented preimage includes the salt (hiding is the assumption of Theorem 6, not an empirical property this test establishes); the salted per-cert costs are one-time publisher costs dominated by the in-circuit hash (Table 1d). All measurements are on commodity hardware; the proving environment is in the released artifacts. Harvested end-to-end certificates. Two representative public-carrier predicates are instantiated end-to-end from garak’s attack suite [12] (EZKL/Halo2, 6.3–6.6 orders separation between honest and payload-carrying adapters on GPT-2, 7.3–6.9 on Qwen/SmolLM2); the verdict survives int8 quantization and predicts the adapter-mediated logit effect (67× the confined adapter’s shift, Theorem 4). The harvested proofs, quantization study, and behavioral validation are in Section C; classifying the full attack surface against the cheap/hard boundary is outside this paper.

Related work

The construction sits at the intersection of four lines of work. Undetectable backdoors (motivation). Backdoors can be planted so as to be provably undetectable from the released weights, computationally [18] or statistically [4]: sparse-hardness and latent-construction results [10, 15] and a detect-to-remove pivot [19] reinforce the picture, motivating our shift from detection to defense relative to a public, declared monitor. Read in reverse, the same algebra is an attack: weight orthogonalization [2] installs r⊤ W = 0 against a public refusal direction r. Reference-based and anomaly-based detection. PEFTGuard [43] and per-projection spectral classifiers [35] learn from labeled adapter corpora; Neural Cleanse [46] reverse-engineers classconditioned candidate triggers; spectral signatures [45] flag representation-space outliers in the training data. Each consumes a behavioral, data, or population reference; absent one, the operatorinvisible subclass is provably hard to distinguish, and confinement supplies the reference structurally. Structural ZK predicates and execution proofs. Shang et al. [40] prove norm/rank/sparsity bounds in ZK under the same publisher–verifier threat model, and FairZK [48] bounds spectral norms for fairness; an operator-invisible payload passes all such bounds; the object here, a kernelconfinement relation, is categorically different. The bulk of zkML proves computational-trace properties [17, 27, 42]; our certificate is a single static predicate, not a trace, sidestepping the cost barrier PAL*M [8] identifies and the ghost-weights attack [20]. Subspace-constrained adaptation [34] is a convergent but uncertified empirical analogue. Hardware attestation and building blocks. PAL*M and Laminator [13] root trust in hardware; the audit-gap analysis [39] formalizes the gap our certificate partially closes. The construction

composes standard machinery [5, 6, 14, 26, 30, 38] and the ZK-CEC precedent [41]. LoRA [24] is the adapter family; MasqLoRA [31] and FloatDoor [28] are live adapter-payload threats.

Scope, limits, and outlook

Each bound below is a theorem or a measured fact. The base model must be public. The certificate is cheap because the blind subspace is a deterministic public function of the base model; a secret base means the verifier cannot recompute Mdep in the clear and certification enters the expensive rank direction (Section 4). Public and identified : the manifest names the deployed base; relaxing identity to membership in a public candidate set is outside this paper. Single-head monitor, extensibly multi-head. The deployed monitor watches one head’s QK map plus its in-kernel augmentation (Theorem 5), and the frontier (Table 1b) is per head; several heads at once is the joint-coverage predicate (Section G), the same typed identity against the stacked monitor, not evaluated end to end. Per-layer, not cross-layer. The certificate confines each layer’s adapter within that layer’s monitor. Under an every-layer defense, cross-layer cascades close by the same rank-nullity argument (Section C); under a partial defense, uncertified layers remain open. Structural, with a bounded behavioral consequence. The certificate is a property of the weights, not a guarantee of behavioral safety: an ε-inert value path shifts any downstream linear readout by at most ∥G∥ε∥δ∥ (Theorem 4), and a model can pass while unsafe in ways the predicate is silent about. Serving-endpoint binding. The certificate and the guard bind the adapter bytes admitted at serving time; binding the admitted tensor to the one the inference kernel executes is outside the attested boundary, the systems frontier (Section 6.1). Knowledge, not just actuation. Typing restricts the adapter’s read to the visible feature Mdep x; it does not constrain the write factor B, nor what behavior is computable from that feature (the full representation is almost surely injective on prompts [33], though a low-rank feature need not be). The boundary is concrete: in the GPT-2 demonstration a directly measured visible contrast c⊤ Mdep x distinguishes the trigger, so a rank-one monitor-typed adapter passes proof and guard yet is 7× trigger-selective (Section E). This is the joint write-and-read channel named in the outlook, not a gap in the structural claim (“no operator-invisible channel of this class”); a knowledge-bounding or behavioral monitor is the complementary defense. Scope of the empirics. The augmentation-frontier geometry is measured across every layer and query head of 8 checkpoints up to 7B (Table 1b and Fig. 2), and the task-utility separation replicates across monitor, budget, rank, and 3 seeds on two instruction tasks (Alpaca [44], Dolly [11]), both modest adaptations on one 0.5B model.

Outlook. Monitor-factorized detection is impossible on this channel, and the reference-free weight statistics we test do not separate benign from malicious use; construction supplies the declared structural reference that detection lacks. A proof-carrying adapter is universal (one static check covers all inputs) and monitor-selective, so monitor quality is what buys security. What it does not cover, nonlinear, compositional, and data-mediated attacks, is the frontier: attesting the joint write-and-read channel.

Ethics considerations

The construction is defensive: it lets a publisher prove a release free of a known attack class without disclosing the certified read factor, and lets a consumer or regulator check that proof. It exposes no new attack. The bounded, named scope of Section 9 is part of the deployment guidance: a passing certificate must be read as the structural, residual-bounded claim it is, not as a comprehensive safety guarantee.

Open science

Code, formal proofs, and reproduction scripts will be released publicly upon acceptance for publication. The research artifacts comprise the paper, the measurement harness, the production pipeline, and the demo. The base models we measure are public (GPT-2, Qwen2.5-0.5B, SmolLM2-1.7B, Qwen2.5-7B on their respective hubs); the release will contain code and derived measurements, with no model weights. Artifact contents. (i) The reference semantics and adversarial falsification suite (clean-accept, OBVS-reject, deficient-basis unsoundness, the defense-specific adaptive attacker), runnable as a single regression target. (ii) An architecture-agnostic measurement library that extracts the query/key/value maps of any supported model (fused and separate projections, multi-head and grouped-query attention) and computes the cost, residual, and kernel-activity statistics as pure functions, with unit tests. (iii) The end-to-end zero-knowledge prover (EZKL/Halo2, KZG–BN254), including the commit-and-prove binding and the garak-harvested certificates. (iv) The Lean 4 development formalizing the soundness statements of Section 5, with the paper-to-declaration table of Table 2. Reproducing the numbers. Every numeric value in the paper is generated from the scripts into macro files the paper reads directly, each value carrying a provenance comment naming its producing script; a documented ordered procedure regenerates the full set (including the cross-architecture cost table Table 1c and figure Fig. 2) and the canonical CSVs the figures and tables read. The Lean development is sorry-free and axiom-clean; a committed check enumerates the axioms each cited declaration depends on (propext, Classical.choice, Quot.sound only). The measurements run on commodity hardware; the largest model is loaded in reduced precision, and the geometric statistics are computed in double precision on the extracted weights.

Machine-checked correspondence

The kernel-algebra and confinement statements of Section 5 are formalized in Lean 4 (with Mathlib) in a self-contained module. Every cited Lean declaration is sorry-free and depends only on the

standard classical axioms propext, Classical.choice, and Quot.sound. The commit-and-prove and attention-instantiation results (Theorem 6 and Lemma 2) and the typed encoding bound (Eq. (7)) are standard linear algebra and cryptographic composition and are not mechanized; of the residual-optimality frontier (Theorem 5), the exact-certification endpoint (the reader-relative characterization and its rank lower bound) is mechanized, while the singular-value grading itself is not. The “machine-checked” claim is scoped to the algebraic core below. Table 2 maps paper statements to Lean declarations. (The formalization builds on a general linear-algebra library; the statements and proofs cited here stand on their own.) Paper statement

Lean declaration

(1) Inertness Theorem 1(a) Channel-absence Theorem 1(c) Defense Theorem 1(b) Factor-through Theorem 2 Typed LoRA Definition 2 Served map Lemma 1 Base floor Proposition 1(a) Isolation Proposition 1(b) Rank obstruction Lemma 4 Zero-product Joint coverage (cheap dual) Theorem 8 Deficient-basis counterexample Theorem 5 zero-residual endpoint (certifies iff) Theorem 5 endpoint rank floor Theorem 3 Encoding tolerance Theorem 4 Behavioral bound

Inert attest sound inert of factor through visible inert iff factors through lora typed inert served served comp eq base of update inert served inert iff base of update inert served comp ne zero of lowrank inert iff zero product joint inert iff spanning necessary readerRelative certifies iff readerRelative rank ge comp perturbation readout shift le

Table 2: Paper-to-Lean correspondence (axiom-clean: propext, Classical.choice, Quot.sound only). The reference implementation and adversarial suite of Section 7 are part of the research artifact described in Section B. The artifact includes the falsification suite, attack/attestation loop, all measurement scripts, and a claim-to-test-to-Lean map; the reproduction procedure is in the artifact’s playbook. Cross-layer cascades under an every-layer defense. The coverage bound of Section 9 governs cross-layer attacks under a strong premise: if every layer’s value path is confined to its own monitor’s visible channel, then a coordinated cancellation cascade (whose per-layer components each lie in that layer’s blind subspace) is inert layer by layer, and the stacked defense closes it by the same rank–nullity argument, not a new mechanism; a component visible at some layer is outside the operator-invisible class by definition, and nonlinear propagation between layers is not modeled beyond this. A cascade against a partially confined stack, in which some layer is left unmonitored, is outside the certificate, exactly as a single unconfined layer is.

The proof-carrying-adapter protocol and trust boundary

We state the deployed system as a named protocol so downstream work cites a fixed interface. Over a public base checkpoint W0 with value map V0 :

(a) Confinement cost

(b) Augmentation frontier 1 0.8 σq+1 /σ1

disruption

1.5 1 0.5 0

0.6 0.4 0.2

0.2

0.4

0.6

0.8

blind fraction dim ker π/dmodel

GPT-2 (MHA) Qwen2.5-1.5B (GQA)

0.2

0.4

0.6

0.8

augmentation fraction q/b

SmolLM2-1.7B (MHA) Qwen2.5-3B (GQA)

Qwen2.5-0.5B (GQA) Llama-3.2-1B (GQA)

Qwen2.5-7B (GQA) Llama-3.2-3B (GQA)

Figure 2: (a) QK-monitor confinement cost grows with blind fraction, across the four checkpoints with capacity measurements. (b) Ideal-design augmentation frontier σq+1 /σ1 (median over all layers and heads, Theorem 5). All eight checkpoints are plotted; the four in (a) keep their colours. The six GQA paths (two families, Q : KV from 3 : 1 to 8 : 1) fall to zero at their own value-path rank nkv dhead , so they collapse at different fractions of b; the MHA paths (GPT-2, SmolLM2) decay only near full coverage. CompileMonitor(W0 , policy) → (Mdep , µ) deterministically builds the finite-precision monitor Mdep from the full base checkpoint (the QK map plus its optimal in-kernel augmentation, Section 3) and an authenticated manifest µ (base hash, model/layer/head, policy, quantization, the compiler digest pinning the SVD implementation with its ordering, sign, and rounding conventions, monitor digest hMdep , verification-key digest, and the public residual floor). TypeTrain(Mdep , data) → (B, A, C) trains the adapter monitor-typed, A = CMdep , so ∆ = BA is inert for every B (Theorem 2). CommitCert(A, C) → c one salted commitment c = Com(A, C; ρ) that the certificate proof opens, hiding A and C from a verifier who never sees the certified read factor, fixed before the challenge is derived. We bind this same c into the package (below), so there is no second, unlinked shipped-factor commitment; committing the read factor alone, which would let a consumer open with a read-only witness, is not expressible under the stock toolchain’s global commitment visibility, so opening c uses (C, ρ), which Package delivers to the weight-holding consumer as a private serving sidecar; the remote verifier receives neither. Package(B, A, µ, c, C, ρ) → (hpkg , P) serializes the shipped package with root hpkg = H µ, (ℓ, tensorIDℓ , shapeℓ , H(Bℓ ), cℓ )L ℓ=1 , binding the shipped write factor and the proof ’s own commitment per layer; P carries the checkpoint (B, A) and, to the serving consumer only, the sidecar (C, ρ). Prove(st; A, C, ρ) → π the certificate proof of the typed relation A = CMdep , opening c (Section 6). Verify(st, π) → {0, 1} one layer’s proof, against st = (hbase , hpkg , µ, Mdep or its digest, c, dmodel , d, r, . . .); VerifyBundle 22

runs Verify on all L layers and recomputes hpkg . ServeGuard(W0 , policy, c, Ã, C, ρ) → {0, 1} × tensor the serving-time guard, run by the weight-holding consumer on the served bytes and the ̸ ÃZ 2−2F private sidecar (C, ρ): (i) it parses Ã as a canonical lattice tensor, rejecting any Ã = 2F for ÃZ = round(Ã 2 ) (a float near a lattice point but not on it is refused, so no off-lattice perturbation, however small, is admitted for the unrestricted write factor to amplify); (ii) it verifies the commitment opening c = Com(Ã, C; ρ), binding the served bytes to the certified factor; (iii) it checks the typed identity exactly over the integer lattice, ÃZ = CZ (Mdep )Z with CZ = round(C 2F ) and (Mdep )Z = round(Mdep 2F ) (the honest adapter is built as A = CMdep on the lattice, so this is an integer equality), where the monitor is recomputed from the authenticated base by CompileMonitor, not a shipped matrix (closing the deficient-monitor substitution); and (iv) it returns the canonical decoded tensor ÃZ 2−2F , the tensor inference must execute (a serving stack that re-casts it to a floating format re-enters the executed-tensor frontier, Section 9). Given the opening, the admission check is exact and unconditional : no prime, no field check, no acceptance threshold, hence no slack that an unbounded write factor B could amplify (Theorem 2). Exactness is a theorem about the canonical weight relation; floating-point evaluation error inside the inference matmul is outside it unless the kernel implements the fixed-point semantics or a separate numerical-error bound is applied. Checking rank over a fixed prime field instead would be unsound, since a congruent ÃZ + pE shares the GF(p) rank yet carries a live channel over the integers; the integer identity above rejects it. The guard reads only the public monitor, the committed read factor, and the served weights, and a defensive range bound on ÃZ rejects wild factors (exactness does not depend on it). The guarantee composes three levels. Algebraic: for every accepted layer, A = CMdep ⇒ ∀δ ∈ ker Mdep , BAδ = 0 (Theorem 2). Served-checkpoint: with Vsrv = V0 + BA, ∀δ ∈ ker Mdep , Vsrv δ = V0 δ (Lemma 1): the publisher adds no blind-subspace channel and the residual is the authenticated base floor. Computational, in two parts. Typed-relation soundness (Theorem 6): except with εbind + εKS + qH |S|−10 , the read factor committed under c is monitor-typed, so the update it forms with any write factor is inert, a privacy-preserving attestation of the committed adapter, checkable without the read factor. No-wrap ledger. The circuit input is m′ = (m, 0): the appended coordinate is a fixed public zero multiplying the committed salt column of C, so the salt enters the commitment preimage but never the identity, and the checked relation stays the homogeneous AZ r = CZ m. The verifier computes m = (Mdep )Z r canonically in exact integer arithmetic outside the circuit (no wrap can occur there) and it enters as a range-checked public input. Every in-circuit cell is bounded by the lookup decomposition (base 214 , two legs): magnitude below 228 , a circuit constraint holding for any witness, not an observed maximum, at the maximum width configured over the twelve generated layer circuits: Intermediate

terms

enforced bound (bits)

AZ r CZ m′ AZ r − CZ m′

dmodel s+1 –

66 65 66

Minimum margin: 186 bits below p/2 (BN254). Served-integrity: ServeGuard admits Ãℓ only if Ãℓ = Cℓ Mdep [ℓ] for the committed Cℓ , an exact integer check that both types the served factor and

binds it to the commitment, so the served update B Ãℓ is confined for the served B whatever an intermediary shipped. The composition is the system’s contract. The contract this interface supports, Theorem 7, is stated and proved in Section 6.1. The probabilistic term in Theorem 6 is the following all-probes bound on the probed identity of Section 6. Lemma 3 (All-probes soundness). Let E := A − CMdep be the residual on the encoding lattice, fixed by the commitment c and the public statement st, and suppose E ̸= 0. If the probe vectors r1 , . . . , r10 have coordinates drawn independently and uniformly from the bounded integer range S after c is fixed, and the no-wrap range checks hold, then Pr[ Erj = 0 for all j ] ≤ |S|−10 , and a prover making qH random-oracle queries to steer the probes succeeds with probability at most qH |S|−10 . Proof. Fix a nonzero row e of E. Conditioning on all coordinates of rj except one at which e is nonzero, at most one value of the remaining coordinate zeroes e · rj , so Pr[e · rj = 0] ≤ 1/|S|; independence across j gives |S|−10 . The union bound over the qH salt choices gives the grinding term. The range checks make a field zero an integer zero, so the field identity checked in-circuit implies the integer one. Overheads. The typing is a training-time parameterization, not a serving-time cost: TypeTrain constrains the read factor to A = CMdep during training, and the shipped (B, A) is an ordinary LoRA once materialized, so inference overhead is zero (the served model runs the standard adapter). The added artifacts are small and one-time: the read factor A is r × dmodel (a rank-8 GPT-2 value adapter is 6656 secret entries), the manifest µ is a handful of hashes and scalars, and the whole-checkpoint proof bundle with its package root is 70 KB, verified in 4.1 s (the root itself 0.03 ms). Prover time is the only material cost and is one-time at publication (555 s for a GPT-2 checkpoint). Table 3: Trust boundary of the deployed certificate.

Object / party

Status

Adapter publisher and prover Read factor A, witness C Write factor B Public base hash, monitor policy Monitor compiler CompileMonitor SNARK, commitment, SRS Artifact distribution Distribution intermediary (may swap A) Served read factor Ã Serving endpoint Served model behavior

untrusted secret, adversarial shipped in the clear, hash-bound trusted public statement deterministic, reproducible cryptographic assumptions bound by hpkg (write factor + the proof’s commitment) untrusted; defeated by ServeGuard admitted only if ServeGuard passes (public monitor) runs ServeGuard; full behavior out of scope absent TEE not certified

Knowledge boundary and parameter-efficiency corollary

The certificate excludes blind actuation; it does not constrain visible-channel knowledge or visible writes, and no predicate keyed to a fixed public carrier decides what rides directions outside that carrier. The demonstration below makes this boundary concrete on GPT-2; the general classification of what cheap certificates can and cannot decide is outside this paper.

Boundary demonstration: knowledge without blind actuation. The knowledge-vsactuation boundary of Section 9 is concrete on real GPT-2: the rank-1 typed adapter A = c⊤ M (with c the monitor-visible contrast of a trigger prompt) passes both the certificate and ServeGuard and reads nothing from ker M (machine zero), yet its output-logit shift is 7× larger on the trigger than on controls. The certificate behaves exactly as specified (it verifies a genuinely typed adapter); the knowledge-conditioned write rides the visible directions: the construction is inside the certified class but outside the blind-actuation class the certificate excludes, which is why a knowledge-bounding or behavioral monitor is the complementary defense. Parameter-efficiency corollary. Confining the value path to a k-dimensional visible channel caps the adapter’s rank at k, so it admits a smaller r × k read parameterization in place of r × dmodel . Empirically a rank-4 adapter confined to a quarter-width channel (11.6× fewer parameters than the unconfined baseline) still recovers 100% of the task gain.

Zero-product form and auxiliary theorems

Optimal in-kernel augmentation (Theorem 5). Proof idea. V0 Pker π = (V0 Nπ )Nπ⊤ ; monitoring T removes the corresponding q domain directions of V0 Nπ , and by the Courant–Fischer min–max characterization the operator norm of the restriction to the remaining (b−q) directions is minimized by dropping its top-q right-singular directions, leaving its (q+1)-th singular value. Ideal-monitor tolerance. A deployer who instead wishes to name an ideal real-valued monitor M and serve its fixed-point compilation Mdep = Mfp pays an explicit, optional tolerance: for any real payload δ ∈ ker M , ∆ δ = BC(Mfp − M ) δ,

∥∆ δ∥ ≤ ∥BC∥ ∥Mfp − M ∥ ∥δ∥,

(7)

since M δ = 0. Here ∥Mfp − M ∥ is the public encoding error of the compiled monitor at the stated fixed-point resolution, and ∥BC∥ ≤ ∥B∥ ∥C∥ is bounded by the range-checked witness C and the norm of the publicly shipped, package-bound write factor B (Section 6), not by any in-circuit constraint on B. This ideal-monitor reading is a modeling choice a deployer may state; the deployed guarantee against Mdep needs none of it. Lemma 4 (Zero-product certificate). If im N = ker M then Inert(M, V ) ⇔ V ◦ N = 0. If only ker M ⊆ im N , then V ◦ N = 0 implies Inert(M, V ). Theorem 8 (Deficient basis: a counterexample). If im N ⊊ ker M (strict), there is a value map V with V ◦ N = 0 yet ¬ Inert(M, V ): a deficient basis admits a non-inert map that passes the certificate. The verifier must check M N = 0 and rank N = dmodel − rank M in the clear. Training can enforce the typed form A = CM by parameterization, or penalize the read factor’s blind component directly as a regularizer; an exact typed adapter has zero blind component.

Predicate family and harvested certificates

Cheap dual (coverage). Inertness against the joint monitor M1 × M2 is inertness against ker M1 ∩ ker M2 , which is publicly computable when both monitors are public; this certifies the dual 25

Predicate

Statement

Role

Inertness

ker M ⊆ ker V , certified by A = CM (or V N = 0) Inert(M, V ◦ Πvis ) for any V Inert(M1 ×M2 , V )

the defense; absence of the OI channel inertness by construction cheap dual

Confinement Joint coverage Behavioral ∥GV δ∥ ≤ ∥G∥ ε ∥δ∥ for δ ∈ bound ker M Named trig- T ⊆ ker V , certified by V N = 0 ger with im N = T

ε-inertness bounded shift fixed public trigger

Table 4: The defense’s predicate family (Section 3). The exact predicates arise from public homogeneous identities; the behavioral row is a norm consequence of inertness. property (closing two monitors’ shared blind spot) by the same cheap zero-product, with no rank lower bound. A budget on a secret monitor is a rank lower bound, the hard direction, and is out of scope (Section 9). Harvested proofs. From garak’s glitch probe: 141 single-token triggers (rank-104 subspace), residual 5.3 × 10−7 (accept) vs 2.3 (reject), 6.6 orders apart. Injection split: 0.90 concealable in ker π, 6.3 orders separation. Architecture-independent: 7.3 (Qwen), 6.9 (SmolLM2). Int8 quantization keeps the tolerance verdict separated (2.0 orders below the backdoor); int4 erodes the margin to 1.5×. Behavioral validation. The rejected adapter shifts glitch-token logits 67× more than the confined one (74 ± 14× over 30 draws); the confined adapter’s shift stays within the Theorem 4 bound. The certificate prevents an adapter from weaponizing the glitch subspace; it does not fix the base model (which fails 95% of 256 prompts on its own).

AI use statement Large language model tooling was used, under the authors’ direction and review, to assist with the Lean 4 formalization of the soundness theorems (every cited Lean declaration is sorry-free and axiom-clean; results or clauses carried only by paper proofs are identified explicitly in Appendix A; the human authors are responsible for the statements and their correspondence to the paper), with implementation of the zero-knowledge prover integration and the measurement harness, and with drafting and editing of the manuscript. All claims, proofs, and reported measurements were verified by the authors, who take full responsibility for the paper’s content. No generative model was used to produce or fabricate experimental data.

References [1] Joshua Ainslie, James Lee-Thorp, Michiel de Jong, Yury Zemlyanskiy, Federico Lebrón, and Sumit Sanghai. GQA: Training generalized multi-query transformer models from multi-head checkpoints. In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 4895–4901, 2023. doi: 10.18653/v1/2023.emnlp-main.298.

[2] Andy Arditi, Oscar Obeso, Aaquib Syed, Daniel Paleka, Nina Panickssery, Wes Gurnee, and Neel Nanda. Refusal in language models is mediated by a single direction. In Advances in Neural Information Processing Systems 37 (NeurIPS 2024), 2024. [3] Yonatan Belinkov. Probing classifiers: Promises, shortcomings, and advances. Computational Linguistics, 48(1):207–219, 2022. doi: 10.1162/coli a 00422. [4] Andrej Bogdanov, Alon Rosen, and Neekon Vafa. Statistically undetectable backdoors in deep neural networks. arXiv:2607.09532, 2026. [5] Sean Bowe, Ying Tong Lai, Daira Emma Hopwood, Jack Grigg, and Electric Coin Company. halo2: The halo2 zero-knowledge proving system, 2024. Software; halo2 proofs 0.3.x. [6] Matteo Campanelli, Dario Fiore, and Anaı̈s Querol. LegoSNARK: Modular design and composition of succinct zero-knowledge proofs. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 2075–2092, 2019. doi: 10.1145/3319535.3339820. [7] Matteo Campanelli, Antonio Faonio, Dario Fiore, Anaı̈s Querol, and Hadrián Rodrı́guez. Lunar: A toolbox for more efficient universal and updatable zkSNARKs and commit-and-prove extensions. In Advances in Cryptology – ASIACRYPT 2021, volume 13092 of Lecture Notes in Computer Science, pages 3–33. Springer, 2021. doi: 10.1007/978-3-030-92078-4 1. [8] Prach Chantasantitam, Adam Ilyas Caulfield, Vasisht Duddu, Lachlan J. Gunn, and N. Asokan. PAL*M: Property attestation for large generative models. arXiv:2601.16199, 2026. [9] Bing-Jyue Chen, Suppakit Waiwitlikhit, Ion Stoica, and Daniel Kang. ZKML: An optimizing system for ML inference in zero-knowledge proofs. In Proceedings of the Nineteenth European Conference on Computer Systems (EuroSys), pages 560–574, 2024. doi: 10.1145/3627703. 3650088. [10] Sarthak Choudhary, Atharv Singh Patlan, Nils Palumbo, Ashish Hooda, Kassem Fawaz, and Somesh Jha. Undetectable backdoors in model parameters: Hiding sparse secrets in high dimensions. arXiv:2605.04209, 2026. [11] Mike Conover, Matt Hayes, Ankit Mathur, Jianwei Xie, Jun Wan, Sam Shah, Ali Ghodsi, Patrick Wendell, Matei Zaharia, and Reynold Xin. Free Dolly: Introducing the world’s first truly open instruction-tuned LLM. Databricks Blog, 2023. databricks/databricks-dolly-15k on Hugging Face. [12] Leon Derczynski, Erick Galinkin, Jeffrey Martin, Subho Majumdar, and Nanna Inie. garak: A framework for security probing large language models. arXiv:2406.11036, 2024. Software; version 0.15.1 used for the harvested certificates. [13] Vasisht Duddu, Oskari Järvinen, Lachlan J. Gunn, and N. Asokan. Laminator: Verifiable ML property cards using hardware-assisted attestations. In Proceedings of the 15th ACM Conference on Data and Application Security and Privacy (CODASPY), pages 317–328, 2025. doi: 10.1145/3714393.3726492. [14] Jean-Guillaume Dumas and Erich Kaltofen. Essentially optimal interactive certificates in linear algebra. In Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation (ISSAC), pages 146–153, 2014. doi: 10.1145/2608628.2608644. 27

[15] Marte Eggen, Eirik Reiestad, Kristian Gjøsteen, and Inga Strümke. Backdoor channels hidden in latent space: Cryptographic undetectability in modern neural networks. arXiv:2605.13214, 2026. [16] Rusins Freivalds. Fast probabilistic algorithms. In Mathematical Foundations of Computer Science 1979, volume 74 of Lecture Notes in Computer Science, pages 57–69. Springer, 1979. doi: 10.1007/3-540-09526-8 5. [17] Sanjam Garg, Aarushi Goel, Somesh Jha, Saeed Mahloujifar, Mohammad Mahmoody, GuruVamsi Policharla, and Mingyuan Wang. Experimenting with zero-knowledge proofs of training. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 1880–1894, 2023. doi: 10.1145/3576915.3623202. [18] Shafi Goldwasser, Michael P. Kim, Vinod Vaikuntanathan, and Or Zamir. Planting undetectable backdoors in machine learning models. In Proceedings of the 63rd IEEE Annual Symposium on Foundations of Computer Science (FOCS), pages 931–942, 2022. doi: 10.1109/FOCS54457. 2022.00092. [19] Shafi Goldwasser, Jonathan Shafer, Neekon Vafa, and Vinod Vaikuntanathan. Oblivious defense in ML models: Backdoor removal without detection. In Proceedings of the 57th Annual ACM Symposium on Theory of Computing (STOC), pages 1785–1794, 2025. doi: 10.1145/3717823.3718245. [20] Chen Gong, Beijie Liu, and Mengyuan Li. Hollow-LLM attack: Computationally trivial weights in zero-knowledge verification of LLM inference. In IEEE Symposium on Security and Privacy (S&P), pages 4339–4355, 2026. doi: 10.1109/SP63933.2026.00258. [21] Lorenzo Grassi, Dmitry Khovratovich, Christian Rechberger, Arnab Roy, and Markus Schofnegger. Poseidon: A new hash function for zero-knowledge proof systems. In 30th USENIX Security Symposium, pages 519–535, 2021. USENIX proceedings; no DOI issued. [22] Jens Groth. On the size of pairing-based non-interactive arguments. In Advances in Cryptology – EUROCRYPT 2016, volume 9666 of Lecture Notes in Computer Science, pages 305–326. Springer, 2016. doi: 10.1007/978-3-662-49896-5 11. [23] Tianyu Gu, Brendan Dolan-Gavitt, and Siddharth Garg. BadNets: Identifying vulnerabilities in the machine learning model supply chain. arXiv:1708.06733, 2017. [24] Edward J. Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen. LoRA: Low-rank adaptation of large language models. In International Conference on Learning Representations (ICLR), 2022. [25] Kuo-Han Hung, Ching-Yun Ko, Ambrish Rawat, I-Hsin Chung, Winston H. Hsu, and PinYu Chen. Attention tracker: Detecting prompt injection attacks in LLMs. In Findings of the Association for Computational Linguistics: NAACL 2025, pages 2309–2322, 2025. doi: 10.18653/v1/2025.findings-naacl.123. [26] Aniket Kate, Gregory M. Zaverucha, and Ian Goldberg. Constant-size commitments to polynomials and their applications. In Advances in Cryptology – ASIACRYPT 2010, volume 6477 of Lecture Notes in Computer Science, pages 177–194. Springer, 2010. doi: 10.1007/ 978-3-642-17373-8 11.

[27] Guofu Liao, Taotao Wang, Shengli Zhang, Jiqun Zhang, Shi Long, and Dacheng Tao. VeriLoRA: Fine-tuning large language models with verifiable security via zero-knowledge proofs. In Proceedings of the Network and Distributed System Security Symposium (NDSS), 2026. [28] Nils Loose, Jonas Sander, Felix Mächtle, and Thomas Eisenbarth. FloatDoor: Platform-triggered backdoors in LLMs. arXiv:2606.19535, 2026. [29] Ning Luo, Timos Antonopoulos, William R. Harris, Ruzica Piskac, Eran Tromer, and Xiao Wang. Proving UNSAT in zero knowledge. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 2203–2217, 2022. doi: 10.1145/ 3548606.3559373. [30] Hidde Lycklama, Alexander Viand, Nikolay Avramov, Nicolas Küchler, and Anwar Hithnawi. Artemis: Efficient commit-and-prove SNARKs for zkML. arXiv:2409.12055, 2024. [31] Liangwei Lyu, Jiaqi Xu, Jianwei Ding, and Qiyao Deng. When LoRA betrays: Backdooring text-to-image models by masquerading as benign adapters. In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR), pages 8577–8586, 2026. [32] George C. Necula. Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 106–119, 1997. doi: 10.1145/263699.263712. [33] Giorgos Nikolaou, Tommaso Mencattini, Donato Crisostomi, Andrea Santilli, Yannis Panagakis, and Emanuele Rodolà. Language models are injective and hence invertible. In The Fourteenth International Conference on Learning Representations (ICLR), 2026. [34] Fabien Polly. Learning only what valid adapters can express: Subspace-constrained adaptation against fine-tuning poisoning. arXiv:2607.05300, 2026. [35] David Puertolas Merenciano, Ekaterina Vasyagina, Kevin Zhu, Javier Ferrando, and Maheep Chaudhary. Weight space detection of backdoors in LoRA adapters. arXiv:2602.15195, 2026. [36] Qwen Team. Qwen2.5 technical report. arXiv:2412.15115, 2024. [37] Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Language models are unsupervised multitask learners. Technical report, OpenAI, 2019. OpenAI technical report; no DOI/arXiv. [38] Ali Rahimi, Babak H. Khalaj, and Mohammad Ali Maddah-Ali. Range-Arithmetic: Verifiable deep learning inference on an untrusted party. arXiv:2505.17623, 2025. [39] Pratinav Seth and Vinay Kumar Sankarapu. Position: Behavioural assurance cannot verify the safety claims governance now demands. arXiv:2605.15164, 2026. [40] Zhenhang Shang, Yingzhe Yu, and Kani Chen. Fine-tuning integrity for modern neural networks: Structured drift proofs via norm, rank, and sparsity certificates. arXiv:2604.04738, 2026. Preprint. [41] Sirui Shen, Zunchen Huang, and Chenglu Jin. Proving circuit functional equivalence in zero knowledge. arXiv:2601.11173, 2026.

[42] Haochen Sun, Jason Li, and Hongyang Zhang. zkLLM: Zero knowledge proofs for large language models. In Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 4405–4419, 2024. doi: 10.1145/3658644.3670334. [43] Zhen Sun, Tianshuo Cong, Yule Liu, Chenhao Lin, Xinlei He, Rongmao Chen, Xingshuo Han, and Xinyi Huang. PEFTGuard: Detecting backdoor attacks against parameter-efficient fine-tuning. In IEEE Symposium on Security and Privacy (S&P), 2025. doi: 10.1109/SP61157. 2025.00161. [44] Rohan Taori, Ishaan Gulrajani, Tianyi Zhang, Yann Dubois, Xuechen Li, Carlos Guestrin, Percy Liang, and Tatsunori B. Hashimoto. Stanford Alpaca: An instruction-following LLaMA model, 2023. Stanford Center for Research on Foundation Models. [45] Brandon Tran, Jerry Li, and Aleksander Madry. Spectral signatures in backdoor attacks. In Advances in Neural Information Processing Systems (NeurIPS), 2018. [46] Bolun Wang, Yuanshun Yao, Shawn Shan, Huiying Li, Bimal Viswanath, Haitao Zheng, and Ben Y. Zhao. Neural Cleanse: Identifying and mitigating backdoor attacks in neural networks. In IEEE Symposium on Security and Privacy (S&P), 2019. doi: 10.1109/SP.2019.00031. [47] Rui Yin, Tianxu Han, Naen Xu, Changjiang Li, Ping He, Chunyi Zhou, Jun Wang, Zhihui Fu, Tianyu Du, Jinbao Li, and Shouling Ji. Compiling activation steering into weights via null-space constraints for stealthy backdoors. In Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 26228–26245, 2026. doi: 10.18653/v1/2026.acl-long.1206. [48] Tianyu Zhang, Shen Dong, Oyku Deniz Kose, Yanning Shen, and Yupeng Zhang. FairZK: A scalable system to prove machine learning fairness in zero-knowledge. In Proceedings of the 2025 IEEE Symposium on Security and Privacy (SP), pages 3460–3478, 2025. doi: 10.1109/SP61157.2025.00205. [49] Zkonduit Inc. EZKL: A library and command-line tool for zero-knowledge inference of deep learning models, 2024. Software; release and proving configuration pinned in the released artifact’s environment manifest. [50] Andy Zou, Long Phan, Sarah Chen, James Campbell, Phillip Guo, Richard Ren, Alexander Pan, Xuwang Yin, Mantas Mazeika, Ann-Kathrin Dombrowski, Shashwat Goel, Nathaniel Li, Michael J. Byun, Zifan Wang, Alex Mallen, Steven Basart, Sanmi Koyejo, Dawn Song, Matt Fredrikson, J. Zico Kolter, and Dan Hendrycks. Representation Engineering: A top-down approach to AI transparency. arXiv:2310.01405, 2023.

Record · ID 1006791 · SHA-256 483bc632d0d24b85
Retrieved via Conceptio — every document is proof-bundled with source, license, and retrieval metadata.