Paper deep dive
Certified Mechanistic Edits: Behavioral Guarantees for Skill Removal and Preservation
Md Sazid Uddin, Md. Khairul Alam Mazumder, M. F. Mridha
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Mechanistic edits (ablations, weight edits, activation steering) are the standard tools for unlearning a harmful capability from a neural network while preserving useful ones. Current approaches validate their effects only by testing, which can never cover an entire continuous region of inputs. Prior work at the interpretability-verification boundary certifies descriptions of a model: what a circuit computes, or whether it faithfully explains the whole. We instead certify the behavioral effect of an edit: that disabling a circuit removes one skill and provably preserves another, for every input in a region; a feature non-interference guarantee in the information-flow-security sense. We demonstrate such certified edits from toy ReLU networks up to a standard softmax + LayerNorm transformer, proving removal and preservation over continuous embedding-space regions and reaching roughly 9x the input-perturbation dimension an exact solver can handle by switching to sound bound propagation. Furthermore, we prove that no finite deterministic black-box test can certify removal, exhibiting an edit that passes exhaustive testing yet provably fails on a survivor pocket that can be made arbitrarily small. Guarantees hold on small, standard-architecture networks and, like any removal claim, presuppose that the target skill admits a decidable specification, a property which real-world harms may not have.
Tags
Links
- Source: https://arxiv.org/abs/2610.03502v1
- Canonical: https://arxiv.org/abs/2610.03502v1
Trouble viewing inline? Open PDF directly →
Full Text
68,583 characters extracted from source content.
Expand or collapse full text
Certified Mechanistic Edits: Behavioral Guarantees for Skill Removal and Preservation Md Sazid Uddin, Md. Khairul Alam Mazumder, M. F. Mridha Affiliation: Department of Computer Science American International University-Bangladesh (AIUB), Dhaka, Bangladesh sazid.uddin, khairul, firoz.mridha@aiub.edu Abstract Mechanistic edits (ablations, weight edits, activation steering) are the standard tools for unlearning a harmful capability from a neural network while preserving useful ones. Current approaches validate their effects only by testing, which can never cover an entire continuous region of inputs. Prior work at the interpretability–verification boundary certifies descriptions of a model: what a circuit computes, or whether it faithfully explains the whole. We instead certify the behavioral effect of an edit: that disabling a circuit removes one skill and provably preserves another, for every input in a region; a feature non-interference guarantee in the information-flow-security sense. We demonstrate such certified edits from toy ReLU networks up to a standard softmax + LayerNorm transformer, proving removal and preservation over continuous embedding-space regions and reaching roughly 9× the input-perturbation dimension an exact solver can handle by switching to sound bound propagation. Furthermore, we prove that no finite deterministic black-box test can certify removal, exhibiting an edit that passes exhaustive testing yet provably fails on a survivor pocket that can be made arbitrarily small. Guarantees hold on small, standard-architecture networks and, like any removal claim, presuppose that the target skill admits a decidable specification, a property which real-world harms may not have. Index Terms: formal verification, mechanistic interpretability, machine unlearning, model editing, non-interference, certified guarantees I Introduction Ablating a circuit, zeroing a weight, clamping a sparse-autoencoder feature, or adding a representation-steering vector now form the standard mechanistic interpretability toolkit for making models safer. These help with unlearning a dangerous capability, suppressing a behavior, or enforcing a refusal. In order to test whether an edit has the desired effect, a mechanistic practitioner runs the edited model on a held-out test set of prompts, checks that the target skill or behavior is gone, and that unrelated skills survive, and ships the edit if the test results are satisfactory. This method of testing answers the question only at the inputs tested. This method of testing answers the question only at the inputs tested. Jailbreaks succeed precisely on inputs outside the distribution that safety training and evaluation covered [1, 2], and unlearning edits that pass their benchmark evaluations are reversed by such inputs [3]. A guarantee that holds for every input in a continuous region would be strictly stronger as a guarantee, and it is exactly what a test set cannot provide. This paper supplies that guarantee. We certify, by formal proof, the behavioral effect of an edit: that after the edit a specified skill is absent, and another is preserved, for all inputs in a region of the model’s input representation. A growing body of work brings formal verification to interpretability, but it certifies descriptions of a model: an accuracy floor for the unedited network [4], whether a discovered circuit faithfully and minimally explains the whole [5], what a circuit computes [6], or whether a circuit is stable under dataset resampling [7]. A separate line of work certifies unlearning statistically, indistinguishability from a model retrained without the deleted data [8]. However, these certificates do not specify how a given edit affects the model’s behavior over a region of inputs. This area of experimentation has been unexplored, and this paper aims to fill this gap. In security terms, our guarantee is a feature non-interference property: the edited component’s output is provably independent of the forbidden input feature, everywhere in the region. The stronger claim is not merely undertested by finite test suites; it is unreachable by them. We prove (Proposition 3) that no finite deterministic black-box test (adaptive queries included) can certify removal of a target skill. The witness is concrete: for an edit that passes an exhaustive grid of tests, our solver exhibits a surviving input where the skill is intact (Fig. 1). Ordinary training produces such “intervention illusions” unprompted, in models as small as four inputs, with survivor pockets below 1.5×10−61.5× 10^-6 of the domain. A diligent tester can therefore ship an edit that leaves the skill alive in a vanishing-but-nonzero pocket, unknowingly. Contributions of this paper: 1. We formalize a certified edit and its certified radius, prove they compose and are cheaply computable (P1–P2), and prove that no finite deterministic black-box test can certify removal (P3), with a constructive witness that our code executes. A companion result (P4) separates edit classes: surgery vs. steering, exactly, with a certified collateral law. 2. An exact-rational encoding into an SMT solver certifies removal and preservation over all token sequences × a continuous embedding ball, on piecewise-linear models up to a threshold-gate transformer, together with a map of exactly how far exact proofs reach (Table I). 3. A bound-propagation extension certifies the same kind of edit on a standard softmax + LayerNorm transformer that the exact solver cannot encode due to its non-linearity. The extension reaches roughly 9×9× the perturbation dimension of the exact frontier, validated to equal the exact radius where both apply and bracketed above by attack. Scope of the guarantees: Our guarantees hold on small, standard-architecture networks; the skills we remove/preserve have a decidable ground-truth specification, which is what makes “removed” a deterministic claim, a property that real harmful capabilities often lack. The demonstration is a proof of concept, motivated by the need for rigorous safety guarantees in AI systems. §VI states the scope in full, and §VII names the follow-up of this work. Fig. 1: An edit that every test approves and the solver refutes. (a) Skill A’s removal region for a constructed two-input model after an ablation edit. A 15×1515× 15 grid (shown), a 201×201201× 201 grid of 40,40140,401 points and 300300 random inputs all report the skill removed while the solver nonetheless returns a surviving input (star). (b) The edited skill-A output along x0x_0 through the survivor: a tent of three ReLUs rises above zero in a band 0.00060.0006 wide, between neighboring grid points 0.0020.002 apart (Proposition 3). (c) An automated search over trained models, 8080 per input dimension, finds no illusion with two or three inputs and three with four or five; their survivor regions lie below 1.5×10−61.5× 10^-6 of the domain (95% Clopper–Pearson bound). I Related Work: the description axis vs. the edit axis We organize the relevant literature by the object each method certifies. Prior formal work certifies objects such as the description of a fixed model; a statistical line certifies an intervention’s average effect; we certify the worst-case behavioral effect of an edit over a continuous region. Table I summarizes the axis. Certified interpretability (the description axis) Compact proofs [4] certify an accuracy bound of the unedited model. Formal mechanistic interpretability [5] certifies that a discovered circuit is faithful and minimal; its Definition 2 quantifies over continuous activation-patch values at finitely many reference inputs, but constrains the agreement with the unedited model, not the task behavior of an edit. Certified Circuits [7] certifies the stability of a discovered circuit under dataset resampling. The nearest neighbor, Verifiable Transformers [6], uses an SMT solver to certify four descriptive properties of a circuit explanation (what it computes, per-input edge necessity, robustness of the final residual); it explicitly disclaims statements about an edit’s behavioral effect. Its “model editing” is surgery performed to make the model verifiable by stripping LayerNorm, replacing heads with restricted programs, then freezing and hashing. It is however not a claim about what an edit does. These methods answer “is this explanation of the model faithful?”; we answer “what happens when you act on it?” Certified edits of a different kind BlockCert [9] attaches certificates to weight edits, but the certified statement is a bound on ∥F′(x)−F(x)∥ F (x)-F(x) over a finite traced prompt set demonstrating how far outputs move, not what the behavior became. A large certified deviation is compatible with the target skill surviving, and a small one with collateral damage. Finite prompt evidence is, moreover, exactly the protocol class our Proposition 3 proves cannot certify removal. We view BlockCert as complementary infrastructure for a different question to our own. Certified unlearning [8] gives a statistical, training-data-level guarantee that the unlearned model is distributionally indistinguishable from one retrained without the deleted data. It certifies a process relative to a counterfactual model, not the behavior of the result; the two guarantees are orthogonal and composable. The statistical / anytime-valid axis A parallel line certifies interventional claims statistically, over a distribution rather than a worst-case region. Certified interventional fidelity (CIF) [10] writes the reported quantity as a causal estimate and gives anytime-valid confidence sequences robust to adaptive intervention sampling. Statistical unlearning of distributions [11] characterizes a removal-preservation Pareto frontier between data distributions. Both are average-case; neither certifies that a specified behavior is absent for every input in a continuous region of one fixed model. CIF is, in fact, precisely the randomized-adaptive-tester case that Proposition 3 explicitly declines to cover. The two are complementary halves of one worry, and we distinguish worst-case/region/exact from average-case/distribution/anytime-valid explicitly. Black-box impossibility neighbors Two methodologically relevant recent results deal with proving impossibility theorems of black-box models. Hair-Trigger Alignment [12] proves that static black-box probing cannot distinguish a genuinely robust model from one hiding adversarial behavior that a single benign fine-tuning update re-activates. This is a statement about a future weight update, not about whether a test certifies that a fixed edit removed a skill over a region. Unlearning as distribution restoration [13] gives an empirical finite-query impossibility for oracle-free unlearning certification; P3 sharpens the deterministic-adaptive case it leaves open. An independent, non-interpretability instance of the same epistemic point, verification over a continuous region catching failures that testing between cases misses appears in autonomous-vehicle control [14]. Non-interference as the security frame We state removal as feature non-interference: the output is provably independent of a forbidden input feature. The vocabulary is borrowed from LLM security. GIF [15] certifies geometric information-flow control for LLM agents (zero flow of untrusted spans to sensitive actions) but is applied there to data flow through an agent. To our knowledge we are the first to certify non-interference as the effect of a mechanistic edit. Editing practice and its pitfalls The steering and unlearning literature ships interventions with empirical validation only [16], and safety analyses document their collateral damage: even random-direction steering breaks safety [17], and refusal ablation has statistically significant, sometimes sign-reversing off-target effects at frontier scale [18, 19]. Our Proposition 4 gives, to our knowledge, the first exact account of that trade-off for a model class, and §V turns it into certified radii. That steering can be compiled into weight changes is established practice [20]. We use the same observation so that one prover covers every edit type. Research gaps The literature leaves three gaps that we address (Table I). • First, formal certificates in interpretability describe a fixed model: its accuracy, its circuits, or the stability of those circuits. The only certificate attached to an edit, BlockCert’s, bounds output deviation on a finite prompt set. No prior work certifies the behavioral effect of a mechanistic edit, removal of one skill and preservation of another, for every input in a continuous region (§IV, §V). • Second, existing impossibility results concern future weight updates or oracle-free empirical certification. None establishes that finite deterministic black-box testing, adaptive or not, cannot certify removal (Proposition 3). • Third, the collateral damage of steering is documented empirically but has no exact account that separates surgical edits from steering (Proposition 4). We address all three gaps using the framework of §I: certificates of removal and preservation over continuous input regions, proved exactly by an SMT solver and extended by sound bound propagation where exact encoding stops (§IV), together with the impossibility and edit-separation results of Propositions 3 and 4. TABLE I: Certification Object and Quantifier Domain comparison of related work with our own Work Certified object Quantifier domain Edit’s behavioral effect? Compact proofs [4] accuracy bound of the unedited model all inputs (small domains) no Formal Mech. Interp. [5] circuit faithfulness under patching continuous activation-patch values, finitely many inputs no Certified circuits [7] stability of a discovered circuit dataset resamplings no Verifiable Transformers [6] four properties of a circuit explanation final-residual perturbations; per-input edge necessity no (disclaimed in [6], §1.4) BlockCert [9] extraction fidelity; output-deviation bound finite traced prompt set partial (how much, not what) Certified unlearning [8] process indistinguishability distribution over models no (statistical) Certified interventional fidelity [10] statistical intervention effect expectation over an input+intervention distribution no (average-case) This paper removal + preservation + certified radius of an edit continuous input regions and their inflations yes I Framework: certified edits and the impossibility of testing I-A Definitions Definition 1 (model class). A network is a function f:ℝd→ℝkf:R^d ^k of the form f(x)=W2ρ(W1x+b1)+b2f(x)=W_2\,ρ(W_1x+b_1)+b_2, where ρ is the componentwise ReLU, the hidden layer has width H (so W1∈ℝH×dW_1 ^H× d, b1∈ℝHb_1 ^H, W2∈ℝk×HW_2 ^k× H), and all weights are rational (every IEEE float is a rational, and the prover hands the solver the exact rationals). We write fhf_h for output coordinate (“head”) h∈1,…,kh∈\1,…,k\ and, for each hidden neuron j∈1,…,Hj∈\1,…,H\, the pre-activation of neuron j is prej(x)=(W1x+b1)jpre_j(x)=(W_1x+b_1)_j. Every such f is continuous and piecewise-linear; the input domain is =[0,1]dD=[0,1]^d. Definition 2 (claim, certificate). A claim is a triplet of shape (h,R,⊳)(h,R, ) with R⊆R a closed box and ⊳∈>,≤ ∈\>,≤\; it holds for g iff ∀x∈R:gh(x)⊳0∀ x∈ R:\;g_h(x) 0. A certificate is a proof of this statement, obtained by showing its negation ∃x∈R:¬(gh(x)⊳0)∃ x∈ R: (g_h(x) 0) is unsatisfiable. Removal of skill A over RAR_A is the claim (A,RA,≤)(A,R_A,≤) about the edited model (the unedited model satisfies (A,RA,>)(A,R_A,>)); preservation of skill B is a pair of claims on B’s regions. Definition 3 (edit). An edit maps a network’s weights to new weights of the same shapes. For a neuron set C⊆1,…,HC \1,…,H\ (the circuit), edit types are defined as follows: 1. Ablation: For each neuron j∈Cj∈ C, zero the jjth row of W1W_1 and the jjth entry of b1b_1; this removes neuron j from the hidden layer, so that prej(x)=0pre_j(x)=0. 2. Weight edit: For head h and neuron j, zero the weight W2[h,j]W_2[h,j]; this removes the contribution of neuron j to head h. 3. Steering: For a steering vector v∈ℝHv ^H (one entry per hidden neuron), add it to the hidden bias, b1←b1+vb_1← b_1+v; this shifts every neuron’s pre-activation by a constant on all inputs, prej(x)→prej(x)+vjpre_j(x) _j(x)+v_j. The special case vj=−sv_j=-s for j∈Cj∈ C and vj=0v_j=0 otherwise is targeted suppression at dose s on C: it pushes down exactly the neurons in C, by an amount s. Definition 4 (inflation, certified radius). For a region R and ε≥0 ≥ 0, the inflated region is Rε=∏i[max(0,li−ε),min(1,ui+ε)]R_ = _i[ (0,l_i- ), (1,u_i+ )] (so R0=R_0=R, Rε⊆R_ ). Given a claim holding on R for g, its certified radius is ε∗=supε∈[0,εmax]:(h,Rε,⊳) holds for g ^\!*= \ ∈[0, _ ]:(h,R_ , ) holds for g\, with εmax _ a fixed upper bound on the inflation considered, chosen large enough that Rεmax=R_ _ =D. Remark 1 (the certified object and the float gap). Certificates are statements about the exact rational network f under real arithmetic. The executed program evaluates the same weights in float64 and can differ pointwise by rounding, bounded by a standard forward-error analysis (≈10−13≈ 10^-13 for our models). A certificate proved with slack γ above that bound holds for the executed program too; a zero-margin claim need not transfer. The toy model’s removal, preservation and control certificates are re-proved with slack γ=10−9γ=10^-9, and every threshold-gate transformer certificate carries slack 10−610^-6 (§IV, App. B). I-B Regions compose and the radius is computable (P1–P2) Proposition 1 (region monotonicity and union closure). Given a model g, a head h, and sign ⊳ , (a) If (h,R,⊳)(h,R, ) holds and R′⊆R R, then (h,R′,⊳)(h,R , ) holds. (b) If (h,Ri,⊳)(h,R_i, ) holds for every i in any index set, then (h,⋃iRi,⊳)(h, _iR_i, ) holds. The family of certified regions is thus downward closed and closed under arbitrary unions, with maximal element the truth set =x∈:gh(x)⊳0T=\x :g_h(x) 0\: a region is certifiable iff it is a subset of T. Both parts are immediate from the meaning of the universal quantifier (proof in App. A). Proposition 1 licenses reporting a maximal certified region and gluing per-patch certificates without re-proving, and underlies the monotonicity of the radius in ε ; it also lets removal and preservation be certified independently and combined. Proposition 2 (the certified radius is well-defined and cheap). Let g be a network, R a box, and suppose (h,R,⊳)(h,R, ) holds. Let S=ε∈[0,εmax]:(h,Rε,⊳) holdsS=\ ∈[0, _ ]:(h,R_ , ) holds\, ε∗=supS ^\!*= S. Then: (a) S is an interval containing 00; (b) if ⊳ is ≤, then the supremum is attained (ε∗∈S ^\!*∈ S); while for >>, only [0,ε∗)⊆S[0, ^\!*) S is guaranteed; (c) for each rational ε , membership ε∈S ∈ S is decided exactly by the (un)satisfiability of a quantifier-free linear-real-arithmetic formula, for which the solver is sound and complete; (d) bisection returns, in at most 2+⌈log2(εmax/τ)⌉2+ _2( _ /τ) queries, either a counterexample, “saturated”, or a bracket [ℓ,hi][ ,hi] with ℓ∈S ∈ S, hi∉Shi∉ S, hi−ℓ≤τhi- ≤τ, hence |ℓ−ε∗|≤τ| - ^\!*|≤τ. The attainment asymmetry in (b) matters for reporting: removal radii (sign ≤) are genuine maxima, whereas preservation radii (sign >>) are suprema our procedure brackets within τ. The bracket guarantee assumes every query is answered; the code treats a solver timeout conservatively as a failed probe, which preserves the soundness of ℓ∈S ∈ S but voids the bracket (no query returned “unknown” in any experiment reported here). Full proof in App. A. I-C No finite test certifies removal (P3) This is the central negative result: the intervention illusion is not an artifact of particular models, but a theorem of the framework itself. Proposition 3 (testing cannot certify removal). Given input dimension d≥1d≥ 1, a removal region R=∏i[li,ui]⊆R= _i[l_i,u_i] with l0<u0l_0<u_0, any finite test set T⊂T , and any δ>0δ>0, there exist a network f, a neuron set C, and the edited model g=ablate(f,C)g=ablate(f,C) such that: (a) the unedited f satisfies the full skill specification; (b) gA(t)≤0g_A(t)≤ 0 for every t∈T∩Rt∈ T∩ R and both preservation claims for skill B hold for g on their entire regions (so even a solver checking preservation approves the edit); (c) the survivor set Sg=x∈R:gA(x)>0S_g=\x∈ R:\,g_A(x)>0\ is nonempty and open, and its relative volume satisfies vol(Sg)/vol(R)<δvol(S_g)/vol(R)<δ. Corollary 1 (adaptive protocols). Let P be any deterministic protocol that queries an edited model at finitely many inputs where each is possibly chosen from earlier answers and then gives its verdicts. If P approves some genuinely edited model, it also approves some edited model that retains the skill on a positive-measure set. Hence, no finite-query deterministic protocol is both sound for removal and nontrivial over any region with nonempty interior. Construction (sketch; full proof App. A). The finitely many test points have finitely many first coordinates; with l0,u0l_0,u_0 they leave an open interval (c−w,c+w)(c-w,c+w) disjoint from all of them. Three hidden neurons with pre-activations x0−(c−w),x0−c,x0−(c+w)x_0-(c-w),\,x_0-c,\,x_0-(c+w) feed head A the combination tentβ(x0)=β[ρ(x0−(c−w))−2ρ(x0−c)+ρ(x0−(c+w))],tent_β(x_0)=β [ρ(x_0-(c-w))-2ρ(x_0-c)+ρ(x_0-(c+w)) ], which is a “hat” that rises to peak βwβ w at x0=cx_0=c, returns to zero at c+wc+w, and is identically zero thereafter (the slopes β,−2β,β,-2β,β cancel); in particular it vanishes at every test point. Lowering head A’s bias by βw/2β w/2 makes gA=tentβ−βw/2g_A=tent_β-β w/2 report “removed” at every test point yet exceed 00 exactly on the slab |x0−c|<w/2|x_0-c|<w/2, of relative volume w/(u0−l0)<δw/(u_0-l_0)<δ (Fig. 1b). For Corollary 1, adding the same gadget to a genuinely edited g0g_0 leaves its transcript on P’s queries unchanged, and therefore P’s deterministic verdict is unchanged, while re-introducing a positive-measure survivor. The scope is deliberate and stated: Cor. 1 covers deterministic black-box protocols (adaptive included); a randomized adaptive tester and a white-box analysis (such as the SMT solver used in this paper) are outside it. Informal statements of P3 should therefore always be read as “no finite deterministic black-box behavioral test.” The constructive proof is the recipe executed by our illusion experiment, and §V reports naturally trained illusions showing the hypothesis needs no adversarial constructor. I-D Surgery vs. steering (P4) Proposition 4 (edit-class separation, one hidden layer). Let g be one-hidden-layer, C⊆1,…,HC \1,…,H\ a neuron set, steerssteer_s targeted suppression at dose s, ablabl ablation of C, and Mj(R)=maxx∈Rprej(x)M_j(R)= _x∈ Rpre_j(x) (attained at a box corner). Then: (a) steers,h(x)=ablh(x)+∑j∈CW2[h,j]ρ(prej(x)−s)steer_s,h(x)=abl_h(x)+ _j∈ CW_2[h,j]\,ρ(pre_j(x)-s) for all x. (b) If s≥maxj∈CMj()s≥ _j∈ CM_j(D) then steers≡ablsteer_s on D, so every certificate and radius is identical. (c) The doses certifying a removal form an interval [s∗(R),∞)[s^*(R),∞) with s∗(R)s^*(R) finite and non-decreasing in R, hence s∗(Rε)s^*(R_ ) non-decreasing in ε (more wiggle room demands more dose). (d) For a general steering vector v=sv^v=s v, on any set of pattern-stable points sharing active set ⊆1,…,HA \1,…,H\, head B’s logit shifts by exactly s∑j∈W2[B,j]v^js _j W_2[B,j] v_j—linear in dose. A circuit disjoint from head B (W2[B,j]=0W_2[B,j]=0) yields provably zero collateral at every dose; a data-derived direction heard by head B erodes preservation in proportion to dose and breaks it outright once the shift exceeds B’s margin. P4 turns the edit comparison of §V-E from measurement into theorem for the one-hidden-layer class: surgical edits must show zero collateral when the circuit is disjoint from head B; diff-of-means steering heard by head B must erode skill B’s preserved margin linearly in dose and break it at sufficient dose. The deeper-network generalization is open (the leftover term propagates through later nonlinearities). P2–P4 each have a machine-checked witness (App. E); P1 follows from the meaning of the universal quantifier. IV Method IV-A Exact encoding (SMT) We encode a network (Def. 1) into the Z3 SMT solver [21] using exact rationals: every weight is converted to a fraction, and each ReLU ρ(z)ρ(z) becomes the split case ite(z>0,z,0)ite(z>0,z,0). A claim (h,R,⊳)(h,R, ) is proved by asserting its negation (an input in R violating it) and obtaining unsat. Because the formula is quantifier-free linear real arithmetic (QF-LRA) over rationals, the verdict is exact and complete (Proposition 2c). An unsat certifies the claim for every point of R, whereas sat returns a concrete counterexample (the solver catching an input for which the skill still fires; such an input might be missed by a test suite). Certified radii are found by bisecting proofs (Proposition 2d). Every proof is cross-checked against a brute-force grid; because the grid runs the float program while the solver reasons about the ideal network, disagreement beyond float noise signals a bug, and disagreement within ∼10−12 \!10^-12 of zero signals a genuinely zero-margin claim (App. B). Sequences and continuous noise in one solver query For a token model we quantify in a single query over all token sequences × a continuous ball of embedding noise. Two encodings are available. The Boolean encoding uses Boolean token selectors (the exact discrete claim) but branches combinatorially and exceeds the time budget at every size we tried. The hull relaxation replaces the discrete token choice with continuous mixture weights over the embedding simplex; the resulting region is a strict superset of the discrete inputs, so an unsat still certifies the discrete claim via Proposition 1a, with no Boolean branching. The hull relaxation is what makes the transformer tractable, once the model is shrunk to the measured frontier (§V). Handling of the float gap Certificates concern the exact rational network while the executed model runs float64. A standard forward-error bound puts the gap at ≈10−13≈ 10^-13 here. The toy model’s removal, preservation and control certificates are re-proved with explicit slack γ=10−9γ=10^-9, and every threshold-gate transformer certificate carries slack 10−610^-6, so these certificates transfer to the executed program. A constructed zero-margin claim is proved by the solver yet violated by the float program by ∼10−16 \!10^-16 (App. B). IV-B Bound-propagation extension (CROWN) Softmax and LayerNorm cannot be encoded exactly: their exponentiations and divisions are outside linear arithmetic. To certify edits on a standard softmax + LayerNorm transformer we switch to bound propagation (auto_LiRPA [22] / CROWN [23]), which computes sound linear lower and upper bounds on the output over an input ball. Bound propagation is sound but incomplete: it may fail to certify a true claim, but never certifies a false one. Two checks support its results. M0 (validate the pipeline against the exact solver) Bound propagation is sound by construction [23], so this check (M0) validates the implementation rather than the guarantee. On the toy ReLU MLP both tools apply and the exact solver is complete (Proposition 2c), so its certified radius is the true radius. CROWN reproduces it exactly (§V): the two pipelines encode the same model, edit and claim, and the relaxation is tight on this subject. Tightness does not transfer to the softmax subject, where no exact oracle is available; attack bracketing covers that case. Attack bracketing Beyond the exact frontier we bracket every certified radius from above by a projected-gradient attack: for each claim we report certified≤true≤attackcertified . A certified radius above an attack radius would be unsound; no reported radius is. The gap between the two measures prover looseness, reported per claim. IV-C Scope of the bound-propagation results A CROWN radius is a lower bound: the interval up to the attack radius is unresolved, and its width measures prover looseness rather than the edit’s fragility. The exact solver instead returns the tipping point itself (Proposition 2b). The relaxation is degenerate at ε=0 =0, so the bisection probes only balls of radius ≥10−4≥ 10^-4, which is the smallest radius we report. Greedy component search finds no separable head/MLP circuit in a from-scratch softmax transformer, so skill A is removed by a position-scoped attention knockout. The certificate concerns the behavioral effect of that intervention instead of the identification of a component-level circuit. V Findings The following findings are discussed in order of safety significance and each finding is supported by whichever experimental subject demonstrates it. The subjects themselves (a progression from a two-input ReLU network to a softmax + LayerNorm transformer) are summarized, with every certified radius, in Table I and detailed in App. D. TABLE I: Certified radii ε∗ ^\!* (Def. 4) by subject. Parenthesized values are skill B’s radius before the edit, so collateral reads as the drop. Exact removal radii are attained tipping points and exact preservation radii are bracketed within the bisection tolerance (Proposition 2b,d); bound-propagation radii are sound lower bounds. Values from committed reports (App. D). Subject Size Prover Pert. dims Removal ε∗ ^\!* Preservation ε∗ ^\!* (unedited) Toy MLP (separated) d=2d=2, 16 hidden SMT 2 ≥0.6≥ 0.6 a 0.09960.0996 (0.0996)(0.0996) Toy MLP (entangled) d=2d=2, 16 hidden SMT 2 ≥0.6≥ 0.6 a 0.09610.0961 (0.0961)(0.0961) Deep MLP 3-12-8-23-12-8-2 SMT 3 ≥0.5≥ 0.5 a 0.07420.0742 (0.0938)(0.0938) b Gate transformer 8 wide, 2 heads SMT (hull) 48 0.01560.0156 0.01250.0125 (0.0344)(0.0344) Adder transformer p=5p=5, 8 wide, 2 heads SMT (siamese) 40 ≥0.05≥ 0.05 a ≥0.002≥ 0.002 c Softmax + LN transf. 64 wide, 4 heads, 2 layers CROWN 448 0.00910.0091 d 0.00790.0079, 0.00980.0098 d a saturated at the search ceiling: bounded by the probe range, not the model. b four-neuron layer-1 circuit, bottleneck layer banned. c plus exact correctness on all 625625 clean sequences at ε=0 =0. d attack-bracketed: ≤0.030.0091\!≤\!0.03, ≤0.050.0079\!≤\!0.05, ≤0.10.0098\!≤\!0.1. V-A An edit’s behavioral effect (removal and preservation of skills) can be proved over a whole input region on a transformer On a standard softmax + LayerNorm transformer (which the SMT solver cannot encode) bound propagation certifies that a position-scoped edit removes skill A (accuracy drops to chance) and preserves skill B (accuracy 100%100\%), over continuous embedding-noise balls in 448448 perturbation dimensions, roughly 9×9× the exact frontier established by SMT. Every radius is bracketed by attack (certified≤true≤attackcertified ): removal 0.0091≤0.030.0091≤ 0.03, preservation 0.0079≤0.050.0079≤ 0.05 and 0.0098≤0.10.0098≤ 0.1; none unsound (Fig. 2). The same guarantee holds exactly on a threshold-gate transformer. The exact solver certifies removal and preservation over all token sequences × a continuous embedding ball in one query. The ablated circuit spans an attention head and three MLP neurons, and switching off the heads alone, or the MLP alone, leaves skill A firing (Fig. 3). Removal certifies to radius 0.0160.016 and preservation to 0.0130.013 (Table I), with the collateral quantified: skill B’s radius falls from 0.0340.034 to 0.0130.013 under the edit. On a known-formula subject (two independent modular adders on disjoint positions) both sides are certified over noise: exact-rational correctness on all 625625 clean sequences, removal to radius ≥0.05≥ 0.05 and preservation robust to radius ≥0.002≥ 0.002 (App. D). Fig. 2: Certified removal and preservation on a standard softmax + LayerNorm transformer, which the exact encoding cannot represent, over embedding-noise balls in 448448 dimensions (about 9×9× the exact frontier of Table I). Solid bars are sound certified radii from bound propagation; each cross marks the radius at which a projected-gradient attack first breaks the claim, so the true radius lies on the dotted span between them. No attack succeeds below a certified radius. Fig. 3: The certified circuit is distributed across attention and the MLP. One decoder block of the exact subject (88 wide, 22 heads, L=6L=6), drawn as its forward pass runs: each block reads the residual stream and adds its output back. Skill A’s circuit (filled) was found by a greedy search over heads and MLP neurons that preserves skill B; switching off the heads alone, or the MLP alone, leaves skill A firing. Ablating the whole circuit certifies removal of A and preservation of B (Table I). V-B No finite test protocol can certify removal Proposition 3 states that the guarantee is unreachable by testing. As witness, we show a constructed edit passes a 40,40140,401-point grid with preservation of skill B proved, yet the solver refutes removal with a concrete surviving input. Ordinary training through our experiments produces three naturally occurring illusions in 160160 models (from models with ≥4≥ 4 inputs), each passing a full grid plus 1,0001,000 random inputs plus preservation checks, and each is refuted by the solver. Their survivor pockets, where skill A is still alive, are tiny: zero hits in 2×1062× 10^6 uniform darts give a 95%95\% Clopper–Pearson ceiling of 1.5×10−61.5× 10^-6 of the domain. A diligent tester may ship these edits believing the skill removed, while the skill survives in a vanishing-but-nonzero pocket (Fig. 1). V-C Feature non-interference A stronger security guarantee is demonstrating that the component’s output is provably independent of the forbidden input rather than merely that the readout is below a threshold. We certify it directly with a two-copy (siamese) encoding (Fig. 4) that bounds a certified influence: the worst-case change in the head’s output as the forbidden input varies over the whole domain. On the transformer the certified influence reaches exactly 00, meaning the readout ignores the quote content everywhere, out to a larger radius than removal itself. On the toy subject the surgical edit drives influence from 2222 to <0.001<\!0.001; on a deliberately entangled “messy” model the edit certifies removal yet influence falls only from 6363 to 1010, quantifying that removal is not deafness. The illusion edit is refuted here too, with a concrete input pair and influence ceiling 0.600.60—exactly the tent’s height. Fig. 4: The certified-influence query. The edited network g is encoded twice, over inputs x and y in the same region that agree on every coordinate except the forbidden one (x0x_0 on the toy models; the quote-token content on the transformer, with the embedding noise shared). The solver searches for a pair whose skill-A outputs differ by more than κ: unsat proves that changing the forbidden input alone moves the output by at most κ, and sat returns such a pair. Bisection on κ yields the certified influence; influence 00 certifies feature non-interference. V-D Removal is robust to input perturbation, up to a certified radius Removal and preservation hold not only on the claimed region but on its inflation by the certified radius (Def. 4). Read on the region’s edge, the radius measures tightness (Proposition 2): the inflated edge stops where the edited model’s own decision boundary does, not at a margin added by the prover (Fig. 5). Across the correctness claims of both toy models, certified edges reach within 0.00120.0012 of the 0.50.5 rule for skill A and within 0.00390.0039 at worst. The residual gap is the model’s decision margin, not prover slack. Fig. 5: The certified radius in input space, for the entangled toy model after ablation and the claim that skill B fires on R=[0,1]×[0.6,1]R=[0,1]×[0.6,1] (Table I). (a) R (dashed) and its inflation by the certified radius ε∗=0.0961 ^\!*=0.0961: the certified region is shaded, and the band that inflation adds to R is hatched. (b) The strip near the rule x1=0.5x_1=0.5 (dotted). The certified edge stops 0.00390.0039 above the rule, within the bisection tolerance of the highest point of the edited model’s own decision boundary gB=0g_B=0 (solid), at x0=0x_0=0. At the smallest refuted inflation the solver returns a counterexample (star) beyond that boundary. Fig. 6: Surgical edits certify zero collateral; diff-of-means steering certifiably erodes the preserved skill. (a) Skill B’s certified radius after each edit type on a separated and an entangled toy model, against each model’s unedited radius (dotted). Ablation, weight editing and targeted steering leave it unchanged; diff-of-means falls short even at the smallest dose that removes skill A. (b) The same radius against diff-of-means dose. Each marker is a separate proof: filled markers also remove skill A, open ones are too weak to. The radius falls linearly in dose (least-squares fits, R2≥0.999R^2≥ 0.999), consistent with Proposition 4(d), until preservation is refuted (cross). V-E Surgical edits certify collateral-free removal, unlike steering Proposition 4 predicts, and the experiments confirm, a sharp split. Surgical edits (ablation, weight edit) certify removal at maximal radius with provably zero (disjoint circuit) or bounded collateral. Realistic diff-of-means steering provably erodes the preserved skill’s margin as dose rises (on the separated model the certified radius falls from 0.09960.0996 to 0.09080.0908 at dose 44 and to 0.06560.0656 at dose 1616, consistent with P4(d)’s linearity), until it breaks preservation outright (Fig. 6). On the transformer the split is starkest: no dose both removes A and preserves B (App. D). A sparse-autoencoder feature clamp, on a model where skill A splits across three features, is certified by the same prover: removal to radius ≥0.5≥ 0.5 and preservation to 0.0640.064, against ablation’s 0.1000.100 on the same model (App. D). The dose→ claim rests on P4(d)’s proven linearity plus a full dose sweep (Fig. 6b). V-F The exact verification frontier and its sound extension The exact frontier is set by internal branching: the Boolean encoding’s cost is exponential in the model’s case splits, and it exceeds the time budget at every size. The shrink-plus-hull-relaxation path reaches a two-head transformer exactly (Table I). Bound propagation goes past it, validated to equal the exact radius on every claim where both provers apply—0.5=0.50.5=0.5 for removal and 0.0996=0.09960.0996=0.0996 for both preservation claims (M0)—and attack-bracketed beyond (M1). Finally, the continuous radius is not a disguised discrete-robustness claim. The smallest single-token swap moves the embedding by 2.942.94, some ≈324×≈\!324× the certified ball, so the continuous guarantee and discrete-prompt robustness are different objects (App. D). Taken together, the findings answer the three gaps of §I. First, an edit’s effect can be proved rather than sampled: on every subject, from a two-input network to a softmax + LayerNorm transformer, removal and preservation hold for every input in a continuous region, and on the toy models the exact certificates stop at the model’s own decision boundary, not at slack in the prover. Second, passing a test suite is not evidence of removal: ordinary training produces edits that pass every test while the skill survives, and the solver refutes them with a concrete input. Third, the choice of edit is itself certifiable: surgical edits remove a skill with provably zero collateral, whereas steering trades removal against collateral in a way no dose resolves. For a practitioner validating a safety edit, the certificate therefore replaces the test set as the evidence that the edit did what it was meant to do, within the scale bound that §VI states. TABLE I: Where exact certification stops. Each row is a configuration of the threshold-gate transformer; each cell is one all-sequences hull query of the unedited model’s skill-A claim, without noise or with it. The rule marks the frontier; the exact subject of Table I has the bold row’s size, with two heads. Configuration Noise vars ε=0 =0 ε=0.005 =0.005 8 wide, 1 head, L=4L=4 32 ✓ 32 s ✓ 155 s 8 wide, 1 head, L=6L=6 48 ✓ 40 s ✓ 230 s 8 wide, 1 head, L=8L=8 64 too loose too loose 12 wide, 1 head, L=6L=6 72 ✓ 31 s timeout 16 wide, 1 head, L=6L=6 96 ✓ 120 s timeout 16 wide, 2 heads, L=8L=8 128 timeout timeout ✓ proved, with solver time; too loose: the hull relaxation is inconclusive; timeout: exceeds the 300300 s query budget, and the 128128-variable row also exceeds 3030 min at ε∈0.01,0.05 ∈\0.01,0.05\. VI Limitations and Scope Scale: Guarantees are proved on small, standard-architecture networks; the exact frontier is exponential in internal branching (§V-F), and bound-propagation results, while sound, are not exact. Wide certified-to-attack gaps reflect prover looseness, and radii are reported over balls of radius ≥10−4≥ 10^-4 (CROWN is degenerate at ε=0 =0). The edit on the softmax model is a position path-patch, not a component circuit, because a from-scratch softmax transformer yields no separable head/MLP circuit. Input region instead of arbitrary prompt: The guarantee is over a class of token sequences × a continuous embedding ball. In the exact cases this covers every discrete prompt in the model’s input space and a continuous neighborhood of each (a superset of all possible prompts). But the continuous axis is embedding-space noise. A certified radius is not a discrete-prompt-edit distance, and indeed a single token swap is ≈324×≈\!324× the certified ball (§V-F). We therefore claim continuous-region robustness, not frontier-scale prompt robustness. The decidable-oracle assumption: Every skill we certify has a decidable ground truth, a computable function such as “input contains more « than »” or (a+b)modp(a+b) p, which is exactly what makes “removed” or “preserved” a crisp, checkable claim. Real harmful capabilities in frontier models have no such decidable oracle: whether an output “exhibits a harmful skill” is contested and, in general, undecidable. The certified-removal setup therefore presupposes a decidable specification of the target skill, and that assumption does not transfer to real harms for free. The known-formula subject is a deliberate step from a threshold rule to an arithmetic specification; the future-work counterpart is in §VII. The demonstration is therefore a proof of concept, not a certificate over a real dangerous capability. VII Conclusion and Future Work We introduced certified mechanistic edits: proofs, holding over a continuous input region, that an edit removes one skill and preserves another. We (1) built the framework (P1–P4) and proved that no finite deterministic black-box test can deliver such a guarantee (P3), (2) gave an exact method and mapped its frontier, and (3) went past that frontier soundly with bound propagation on a standard softmax + LayerNorm transformer. The natural next step is certified mechanistic edits at scale and on real skills: bound propagation on a pretrained small language model with a genuinely safety-relevant capability and a real edit (SAE clamp or unlearning), and a discrete edit-distance certificate to complement the continuous one. The prerequisite that our limitations expose is sharper: applying any of this to real harms first requires a framework that decides (deterministically or probabilistically) whether a model output exhibits a target capability. That decidable or estimable oracle is what would let the certified-edit machinery leave the toy and known-formula regime. Such a step would show that mechanistic edits can be certified on real models and real skills, and that the certified radius is meaningful in discrete prompt space. Open Science All claims are reproducible from committed code and fixed seeds: each reported number is regenerated by a single command from a versioned report (App. D). The exact pipeline depends only on numpy and an SMT solver; the bound-propagation extension isolates its dependencies in a separate environment. The code and all committed reports will be released publicly with the final version of this paper. LLM usage considerations LLMs were used for editorial purposes in this manuscript, and all outputs were inspected by the authors to ensure accuracy and originality. They were also used as coding and writing assistants (code scaffolding, prose editing, and literature-scan support). All formal statements, proofs, experimental designs, and numerical results were produced and verified by the authors and by the machine-checked witnesses of App. E; no experimental result or citation was taken from an LLM without independent verification against primary sources. Ethical Considerations This work develops defensive guarantees: proofs that a safety edit did what it was intended to do. Two dual-use points need stating. First, Proposition 3 and the intervention-illusion experiments show that an edit can pass exhaustive testing while a skill survives; we present this to caution practitioners against over-trusting test-based validation, not as an evasion recipe; the survivors are exhibited precisely so they can be caught. Second, Proposition 4 and §V-E characterize when steering damages an unrelated skill; the same algebra that predicts collateral also bounds it, and we report it to make edits auditable. All models and skills studied here are toy or known-formula constructs with no dangerous capability; no human-subjects data, personal data, or deployed system is involved. References [1] A. Wei, N. Haghtalab, and J. Steinhardt, “Jailbroken: How does llm safety training fail?” Advances in neural information processing systems, vol. 36, p. 80 079–80 110, 2023. [2] A. Zou, Z. Wang, N. Carlini, M. Nasr, J. Z. Kolter, and M. Fredrikson, “Universal and transferable adversarial attacks on aligned language models,” arXiv preprint arXiv:2307.15043, 2023. [3] J. Łucki, B. Wei, Y. Huang, P. Henderson, F. Tramèr, and J. Rando, “An adversarial perspective on machine unlearning for ai safety,” 2025. [Online]. Available: https://arxiv.org/abs/2409.18025 [4] J. Gross, R. Agrawal, T. Kwa, E. Ong, C. H. Yip, A. Gibson, S. Noubir, and L. Chan, “Compact proofs of model performance via mechanistic interpretability,” Advances in Neural Information Processing Systems, vol. 37, p. 79 453–79 515, 2024. [5] I. Hadad, G. Katz, and S. Bassan, “Formal mechanistic interpretability: Automated circuit discovery with provable guarantees,” arXiv preprint arXiv:2602.16823, 2026. [6] N. Somani, “Towards verifiable transformers: Solver-checkable circuit explanations,” arXiv preprint arXiv:2605.24033, 2026. [7] A. Anani, T. Lorenz, B. Schiele, M. Fritz, and J. Fischer, “Certified circuits: Stability guarantees for mechanistic circuits,” arXiv preprint arXiv:2602.22968, 2026. [8] A. Koloskova, Y. Allouah, A. Jha, R. Guerraoui, and S. Koyejo, “Certified unlearning for neural networks,” arXiv preprint arXiv:2506.06985, 2025. [9] S. Andric, “BlockCert: Certified blockwise extraction of transformer mechanisms,” arXiv preprint arXiv:2511.17645, 2025. [10] A. Asiaee, “Certified interventional fidelity: Anytime-valid, adaptive evaluation of causal claims in mechanistic interpretability,” arXiv preprint arXiv:2607.08349, 2026. [11] A. Pandey and S. Kulkarni, “Statistical unlearning of distributions: A hypothesis testing approach,” arXiv preprint arXiv:2605.16645, 2026. [12] Y. F. Bakman, D. N. Yaldiz, S. Avestimehr, and S. P. Karimireddy, “Hair-trigger alignment: Black-box evaluation cannot guarantee post-update alignment,” in Proceedings of the 6th Workshop on Trustworthy NLP (TrustNLP 2026), 2026, p. 180–203. [13] S. Yang and Y.-H. Yeung, “Unlearning as distribution restoration: A controlled counterfactual study, a validated selective screen, and the limits of oracle-free certification,” arXiv preprint arXiv:2607.19442, 2026. [14] M. Ghalan, C. Rodgers, and Z. D. Asher, “Testing between the test cases: Proving end-to-end steering in conditions you never drove,” arXiv preprint arXiv:2609.10951, 2026. [15] A. Storek, N. Holzer, Z. Zhang, and S. Jana, “GIF: Locally sound geometric information flow control for LLMs,” arXiv preprint arXiv:2606.23277, 2026. [16] A. Zou, L. Phan, S. Chen, J. Campbell, P. Guo, R. Ren, A. Pan, X. Yin, M. Mazeika, A.-K. Dombrowski et al., “Representation engineering: A top-down approach to AI transparency,” arXiv preprint arXiv:2310.01405, 2023. [17] A. Korznikov, A. Galichin, A. Dontsov, O. Y. Rogov, I. Oseledets, and E. Tutubalina, “The rogue scalpel: Activation steering compromises LLM safety,” arXiv preprint arXiv:2509.22067, 2025. [18] A. Fafuła, “Abliteration is not a scalpel: Off-target effects of refusal removal on decision disposition across model families,” arXiv preprint arXiv:2607.17427, 2026. [19] Y. Li, A. Fastowski, E. Zaradoukas, B. Prenkaj, and G. Kasneci, “Analysing the safety pitfalls of steering vectors,” in Findings of the Association for Computational Linguistics: ACL 2026, 2026, p. 11 182–11 204. [20] R. Yin, T. Han, N. Xu, C. Li, P. He, C. Zhou, J. Wang, Z. Fu, T. Du, J. Li et al., “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), 2026, p. 26 228–26 245. [21] L. de Moura and N. Bjørner, “Z3: An efficient smt solver,” in Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and J. Rehof, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, p. 337–340. [22] K. Xu, Z. Shi, H. Zhang, Y. Wang, K.-W. Chang, M. Huang, B. Kailkhura, X. Lin, and C.-J. Hsieh, “Automatic perturbation analysis for scalable certified robustness and beyond (auto_LiRPA),” in Advances in Neural Information Processing Systems, vol. 33, 2020. [23] H. Zhang, T.-W. Weng, P.-Y. Chen, C.-J. Hsieh, and L. Daniel, “Efficient neural network robustness certification with general activation functions (CROWN),” in Advances in Neural Information Processing Systems, vol. 31, 2018. Appendix A Full Proofs of P1–P4 Throughout, g is a network of Definition 1, so ghg_h is continuous and piecewise-linear on =[0,1]dD=[0,1]^d; “claim”, “certificate”, “edit”, “inflation” and “certified radius” are as in Definitions 2–4. A-A Proposition 1 (region monotonicity and union closure) Proof. Both parts are immediate from the meaning of the universal quantifier. (a) A statement true of every point of R is true of every point of any R′⊆R R. (b) A statement true of every point of each RiR_i is true of every point of ⋃iRi _iR_i. Consequently the union of all certified regions is itself certified and contains every certified region; it equals the truth set =x∈:gh(x)⊳0T=\x :g_h(x) 0\ because each singleton x⊆\x\ is certified, and any certified region is a subset of T by definition. ∎ A-B Proposition 2 (the certified radius) Proof. Write loi(ε)=max(0,li−ε)lo_i( )= (0,l_i- ), hii(ε)=min(1,ui+ε)hi_i( )= (1,u_i+ ). (a) Interval structure. If ε′≤ε ≤ then loi(ε)≤loi(ε′)lo_i( ) _i( ) and hii(ε′)≤hii(ε)hi_i( ) _i( ) coordinatewise, so Rε′⊆RεR_ R_ ; the claim on RεR_ then gives the claim on Rε′R_ by Proposition 1(a). Hence S is downward closed in [0,εmax][0, _ ] and contains 00, i.e. an interval. (b) Attainment. Non-strict sign ≤: fix x∈Rε∗x∈ R_ ^\!*; we show gh(x)≤0g_h(x)≤ 0. Each endpoint is 11-Lipschitz in ε and loi(ε)≤li≤ui≤hii(ε)lo_i( )≤ l_i≤ u_i _i( ), so every RεR_ is a nonempty box. For ε<ε∗ < ^\!* let x(ε)x( ) be the coordinatewise clip of x into RεR_ ; then x(ε)∈Rεx( )∈ R_ and |x(ε)i−xi|≤ε∗−ε|x( )_i-x_i|≤ ^\!*- , so x(ε)→x( )→ x as ε↑ε∗ ^\!*. Choose εn↑ε∗ _n ^\!* with εn∈S _n∈ S (possible since S⊇[0,ε∗)S [0, ^\!*) by (a)); then gh(x(εn))≤0g_h(x( _n))≤ 0, and by continuity gh(x)=limngh(x(εn))≤0g_h(x)= _ng_h(x( _n))≤ 0. Hence ε∗∈S ^\!*∈ S. Strict sign >>: [0,ε∗)⊆S[0, ^\!*) S is (a); that ε∗ ^\!* may fail is shown by d=1d=1, g(x)=ρ(0.5−x)g(x)=ρ(0.5-x), claim g>0g>0 on R=[0,0.2]R=[0,0.2]: then Rε=[0,0.2+ε]R_ =[0,0.2+ ] and the claim holds iff 0.2+ε<0.50.2+ <0.5, so S=[0,0.3)S=[0,0.3) and at ε∗=0.3 ^\!*=0.3 the point x=0.5x=0.5 gives g(x)=0≯0g(x)=0 >0. (c) Decidability. The negated claim is ∃x:⋀i(loi≤xi≤hii)∧¬(gh(x)⊳0)∃ x: _i(lo_i≤ x_i _i) (g_h(x) 0), where gh(x)g_h(x) is built from rational constants, addition, multiplication-by-constant, and ite(z>0,z,0)ite(z>0,z,0) terms. Eliminating each iteite into a disjunction of two linear cases yields a quantifier-free formula of linear real arithmetic; satisfiability of QF_LRA is decidable (e.g. by simplex-based DPLL(T)), and with rational inputs the answer is exact. A solver timeout returns “unknown”, which the implementation reports rather than treating as either verdict. (d) Cost bound. One query at ε=0 =0 (vacuity) and one at εmax _ (saturation); thereafter bisection maintains a bracket [ℓ,hi][ ,hi] with ℓ∈S ∈ S, hi∉Shi∉ S—valid because S is an interval by (a)—halving hi−ℓhi- once per query until hi−ℓ≤τhi- ≤τ, i.e. ⌈log2(εmax/τ)⌉ _2( _ /τ) queries. Since ℓ≤ε∗≤hi ≤ ^\!* , |ℓ−ε∗|≤τ| - ^\!*|≤τ. The bracket half of the guarantee assumes each probe is answered; treating “unknown” as a failed probe preserves soundness of ℓ∈S ∈ S but voids |ℓ−ε∗|≤τ| - ^\!*|≤τ. ∎ A-C Proposition 3 and its corollaries Proof of Proposition 3. Constructive. The gadget. The finitely many test points have finitely many first coordinates t0:t∈T\t_0:t∈ T\; together with l0,u0l_0,u_0 these leave an open interval (c−w,c+w)⊂(l0,u0)(c-w,c+w)⊂(l_0,u_0) disjoint from all of them (finitely many points cannot cover an interval: pick c strictly between two consecutive such values and w below half the gap). Shrink w further if needed so w<δ(u0−l0)w<δ(u_0-l_0). Take three hidden neurons with pre-activations x0−(c−w),x0−c,x0−(c+w)x_0-(c-w),\,x_0-c,\,x_0-(c+w) and feed head A tentβ(x0)=β[ρ(x0−(c−w))−2ρ(x0−c)+ρ(x0−(c+w))].tent_β(x_0)=β [ρ(x_0-(c-w))-2ρ(x_0-c)+ρ(x_0-(c+w)) ]. A case check on the four intervals cut by c−w,c,c+wc-w,c,c+w shows tentβtent_β is the “hat”: zero for x0≤c−wx_0≤ c-w, rising linearly to peak βwβ w at x0=cx_0=c, falling to zero at x0=c+wx_0=c+w, and identically zero thereafter (the slopes β,−2β,β,-2β,β cancel). In particular tentβ≥0tent_β≥ 0 and tentβ(t0)=0tent_β(t_0)=0 at every test point. The model. Let f consist of a main pathway for skill A with decision margin exceeding βw/2β w/2 on A’s specification regions; an untouched pathway for skill B reading only x1x_1 (zero weight from the gadget into head B); the gadget neurons into head A; and head-A bias lowered by βw/2β w/2 (the “hurdle”). Let C be the main-pathway A-neurons and g=ablate(f,C)g=ablate(f,C). (a) Pre-edit, head A=main(x0)+tentβ(x0)−βw/2A=main(x_0)+tent_β(x_0)-β w/2. On A’s HIGH region the main margin exceeds βw/2β w/2 and tentβ≥0tent_β≥ 0, so head A>0A>0; on A’s LOW region the bump is absent (it lies inside HIGH, so tentβ=0tent_β=0 there), the main pathway is nonpositive, and the hurdle only lowers it, so head A≤0A≤ 0. Skill B’s claims hold as its pathway is disjoint from the gadget and C. (b) Post-edit, gA(x)=tentβ(x0)−βw/2g_A(x)=tent_β(x_0)-β w/2. At each t∈Tt∈ T, tentβ(t0)=0tent_β(t_0)=0, so gA(t)=−βw/2<0g_A(t)=-β w/2<0; and B’s pathway, untouched and receiving nothing from the gadget, preserves both claims on their full regions. (c) gA(x)>0g_A(x)>0 iff tentβ(x0)>βw/2tent_β(x_0)>β w/2 iff |x0−c|<w/2|x_0-c|<w/2; so Sg=x∈R:x0∈(c−w/2,c+w/2)S_g=\x∈ R:x_0∈(c-w/2,c+w/2)\ is open, nonempty, of relative volume w/(u0−l0)<δw/(u_0-l_0)<δ. ∎ Corollary 2 (random testing). A test drawing m i.i.d. uniform points from R wrongly approves g with probability at least (1−δ)m≥1−mδ(1-δ)^m≥ 1-mδ. Proof. By Proposition 3(c), each draw lands in SgS_g with probability below δ; independence gives miss probability >(1−δ)m≥1−mδ>(1-δ)^m≥ 1-mδ (Bernoulli). For the constructed gadget the pocket volume is exact; for the naturally-trained illusions of §V-B it is only sampled (zero hits in 2×1062× 10^6 darts, a 95%95\% Clopper–Pearson ceiling of 1.5×10−61.5× 10^-6). ∎ Proof of Corollary 1. Run the deterministic protocol P against a genuinely edited g0g_0 (g0,A≤0g_0,A≤ 0 on all of R); it queries a finite set T′T and approves. Apply the gadget to T′T : choose (c−w,c+w)(c-w,c+w) avoiding T′T ’s first coordinates and add the three tent neurons to head A with pattern (β,−2β,β)(β,-2β,β) and no bias change, giving g=g0+tentβg=g_0+tent_β on head A. Since tentβtent_β vanishes at every point of T′T , g agrees with g0g_0 at every query, so P’s transcript—and hence its verdict, P being deterministic—is identical: P approves g. But g0,Ag_0,A is continuous on the compact R, hence bounded below by some −G-G; choosing β with βw/2>Gβ w/2>G makes gA>0g_A>0 on |x0−c|<w/2|x_0-c|<w/2, a positive-measure set. (g is a legitimate edited model: add the same gadget to g0g_0’s parent and ablate the same C.) ∎ Scope. Corollary 2 covers i.i.d. uniform sampling; Corollary 1 covers deterministic black-box protocols (adaptive included). A randomized adaptive tester (transcript replay yields only a fooling probability) and a white-box analysis such as the SMT solver used here are deliberately outside the statements—the latter escape being the paper’s point. TABLE IV: The command behind each reported result. Result Script Softmax + LayerNorm transformer, 448448 noise dimensions: certified ≤ attack for removal and both preservation claims (Fig. 2) run_boundprop_transformer.py† Threshold-gate transformer, exact over all sequences: removal 0.0160.016, preservation 0.0130.013, collateral 0.034→0.0130.034→ 0.013 (Table I) run_transformer.py Distributed circuit: neither the attention heads nor the MLP alone removes skill A (Fig. 3) results/rung2_circuit_search.pyb Modular-adder transformer: removal as exact independence of the summands, radius ≥0.05≥0.05 (§V-A) run_rung3.py Modular-adder transformer: correctness on all 625625 clean sequences, preservation radius ≥0.002≥0.002 (§V-A) run_rung3_preservation.py Constructed illusion: passes a 40,40140,401-point grid with preservation proved, refuted by the solver (Fig. 1a,b) run_illusion.py Three naturally trained illusions in 160160 four- and five-input models (§V-B) run_illusion_nd.py Illusions per input dimension, 8080 models each; the d=4,5d=4,5 rows reproduce the pooled run exactly (Fig. 1c) run_illusion_dims.py Certified influence exactly 00 on the transformer (§V-C) run_transformer_independence.py Certified influence on the separated and entangled models; the illusion edit refuted with an input pair (§V-C) run_independence.py Certified boundary within 0.00120.0012 of the model’s decision rule (§V-D) run_margin_curve.py Certified edge against the model’s own decision boundary (Fig. 5) run_robustness.py Radii per edit type on the two toy subjects (Table I, §V-E) run_robustness.py Deep MLP: four-neuron layer-1 circuit and its collateral (Table I) run_deep_multi.py Steering dose sweep over doses 0.50.5–6464 (§V-E) run_collateral_sweep.pya On the transformer, no steering dose both removes A and preserves B (§V-E) run_transformer_steering.py SAE feature-clamp edit certified by the same prover (§V-E) run_sae_clamp.py Edit-type tables on the transformer and the modular adder (§V-E) run_transformer_edit_table.py run_rung3_edit_table.py Exact-frontier size ladder and encoding timeouts (§V-F) results/rung2_size_ladder.pyb results/rung2_hull_wall.pyb M0: bound propagation equals the exact radius where both apply (§IV-B) run_boundprop_validate.py† Smallest token swap is ≈324×≈324× the certified ball (§V-F) run_boundprop_quantifier.py† Float-gap ceiling and slack re-proofs (App. B) run_float_gap.py Machine-checked witnesses for P1–P4 (App. E) run_theory_checks.py Each script run_⟨ ⟩ .py writes results/⟨ ⟩ _report.md,json, except: a writes results/collateral_sweep.json; b writes the matching results/rung2_*.log. † requires the separate bound-propagation environment; every other script needs only numpy and an SMT solver. A-D Proposition 4 (edit-class separation) Proof. (a) Neurons outside C have identical pre-activations and outputs under steerssteer_s and ablabl. A neuron j∈Cj∈ C outputs ρ(prej(x)−s)ρ(pre_j(x)-s) under steerssteer_s and 00 under ablabl, where prejpre_j is the unedited pre-activation. Heads are affine in the neuron outputs with coefficients W2[h,⋅]W_2[h,·], so the head difference is exactly ∑j∈CW2[h,j]ρ(prej(x)−s) _j∈ CW_2[h,j]\,ρ(pre_j(x)-s). (b) prejpre_j is affine, so its maximum over the box D is at a corner, giving Mj()M_j(D). If s≥Mj()s≥ M_j(D) for all j∈Cj∈ C then every leftover term is 00 on D, so by (a) the two edited models are equal as functions; equal functions satisfy the same claims over every region, hence share every certificate and certified radius. (c) Each leftover term is nonincreasing in s (ρ nondecreasing, its argument decreasing), so maxx∈R[ablA(x)+∑j∈CW2[A,j]ρ(prej(x)−s)] _x∈ R[abl_A(x)+ _j∈ CW_2[A,j]ρ(pre_j(x)-s)] is nonincreasing in s; the certifying condition “≤0≤ 0” therefore holds on an up-closed set [s∗(R),∞)[s^*(R),∞), nonempty because at s=maxjMj()s= _jM_j(D) it reduces to ablabl’s certificate by (b). Enlarging R can only enlarge the max, so s∗s^* grows; RεR_ is monotone in ε (Proposition 2a). The left side is continuous in s (finite max over compact R of a jointly continuous function), so the non-strict inequality passes to the limit and s∗(R)s^*(R) is attained. (d) Applying the same affine-head argument to steervsteer_v and the unedited g gives steerv,h(x)−gh(x)=∑jW2[h,j][ρ(prej(x)+vj)−ρ(prej(x))].steer_v,h(x)-g_h(x)= _jW_2[h,j] [ρ(pre_j(x)+v_j)-ρ(pre_j(x)) ]. At a pattern-stable x with active set A: a neuron active in both contributes ρ(prej+vj)−ρ(prej)=vjρ(pre_j+v_j)-ρ(pre_j)=v_j, one inactive in both contributes 00, and terms with vj=0v_j=0 vanish; the sum reduces to ∑j∈W2[h,j]vj _j W_2[h,j]v_j, independent of x. With v=sv^v=s v this is s∑j∈W2[B,j]v^js _j W_2[B,j] v_j for head B—linear in s. A circuit C with W2[B,j]=0W_2[B,j]=0 leaves head B unchanged at every dose; a direction heard by head B shifts its margin proportionally and breaks preservation once the shift exceeds B’s minimum on the pattern-stable part of R. ∎ Appendix B Exact Encoding Details and the Float Gap The encoding converts every weight to an exact rational and every ReLU to an iteite term; a claim is proved by unsat of its negation. The forward-error ceiling between the ideal rational network and the executed float64 program is ≈10−13≈ 10^-13 for our models. The toy model’s removal, preservation and control certificates re-prove with slack γ=10−9γ=10^-9 (prove_forall(…,slack=γ)), and every threshold-gate transformer certificate carries slack 10−610^-6. A constructed zero-margin claim proved exactly yet violated by the float program by ∼10−16 \!10^-16 on about a quarter of a region is the boundary of the transfer argument; region endpoints are float constants too (∼10−17 \!10^-17 from the stated rationals), immaterial at our margins. Appendix C Bound-Propagation Setup CROWN bounds are computed in chunks with gradients disabled during certification for memory safety; radii are reported over balls of radius ≥10−4≥ 10^-4 (CROWN is degenerate at ε=0 =0). Every certified radius is bracketed above by a projected-gradient attack, and the bound-propagation dependencies are isolated from the pure numpy++SMT exact pipeline. Appendix D Reproducibility Each reported result is regenerated by one command from committed code and fixed seeds; Table IV maps every result to its script. Appendix E Machine-Checked Witnesses P2–P4 each have a runnable check (P1 follows from the meaning of the universal quantifier): P2’s query-count bound with re-proof at the returned radius and re-refutation just past it; P3’s per-grid gadget with the survivor located in the predicted sliver c±w/2c± w/2; the adaptive-tester transcript replay for Corollary 1; P4(a)’s leftover identity at 2×1052× 10^5 random inputs and several doses, P4(b)’s corner-formula threshold, and P4(d)’s pattern-stable collateral constant per observed activation pattern. The margin-curve dose sweep (Table IV) exercises P4(c). All checks pass.