Certified Mechanistic Edits: Behavioral Guarantees for Skill Removal and Preservation

Certified Mechanistic Edits: Behavioral Guarantees for Skill Removal and Preservation Md Sazid Uddin, Md. Khairul Alam Mazumder, M. F. Mridha

arXiv:2610.03502v1 [cs.LG] 2 Oct 2026

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 noninterference 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. I NTRODUCTION Ablating a circuit, zeroing a weight, clamping a sparseautoencoder 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−6 of the domain. A diligent tester can therefore ship an edit that leaves the skill alive in a vanishingbut-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 III). 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× 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 groundtruth 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. II. R ELATED W ORK : 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. a) 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, perinput 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?” b) 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)∥ 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.

c) 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. d) 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]. e) 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. f) 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

(a)

(b)

(c)

0.5

survivor

survivor band, width 0.0006

2/92 illusions found

skill A output after edit

x1

1.0

0

2

1/106 1

grid spacing 0.002 0.0 0.6

0.7

0.8

x0

0.9

1.0

0.811

0.813

0.815

x0

0.817

0.819

0

0/49

0/100

2

3

4

5

inputs

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 × 15 grid (shown), a 201 × 201 grid of 40,401 points and 300 random inputs all report the skill removed while the solver nonetheless returns a surviving input (star). (b) The edited skill-A output along x0 through the survivor: a tent of three ReLUs rises above zero in a band 0.0006 wide, between neighboring grid points 0.002 apart (Proposition 3). (c) An automated search over trained models, 80 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−6 of the domain (95% Clopper–Pearson bound).

mechanistic edit, removal of one skill and preservation of model satisfies (A, RA , >)); preservation of skill B is a pair another, for every input in a continuous region (§IV, §V). of claims on B’s regions. • Second, existing impossibility results concern future weight updates or oracle-free empirical certification. None Definition 3 (edit). An edit maps a network’s weights to new establishes that finite deterministic black-box testing, weights of the same shapes. For a neuron set C ⊆ {1, . . . , H} (the circuit), edit types are defined as follows: adaptive or not, cannot certify removal (Proposition 3). • Third, the collateral damage of steering is documented 1) Ablation: For each neuron j ∈ C, zero the jth row of W1 empirically but has no exact account that separates surgical and the jth entry of b1 ; this removes neuron j from the edits from steering (Proposition 4). hidden layer, so that prej (x) = 0. We address all three gaps using the framework of §III: 2) Weight edit: For head h and neuron j, zero the weight certificates of removal and preservation over continuous input W2 [h, j]; this removes the contribution of neuron j to regions, proved exactly by an SMT solver and extended by head h. sound bound propagation where exact encoding stops (§IV), 3) Steering: For a steering vector v ∈ RH (one entry per together with the impossibility and edit-separation results of hidden neuron), add it to the hidden bias, b1 ← b1 + v; Propositions 3 and 4. this shifts every neuron’s pre-activation by a constant on all inputs, prej (x) → prej (x) + vj . The special case III. F RAMEWORK : CERTIFIED EDITS AND THE vj = −s for j ∈ C and vj = 0 otherwise is targeted IMPOSSIBILITY OF TESTING suppression at dose s on C: it pushes down exactly the neurons in C, by an amount s. A. Definitions Definition 1 (model class). A network is a function f : Rd → Definition 4 (inflation, certified Qradius). For a region R and ε ≥ Rk of the form f (x) = W2 ρ(W1 x + b1 ) + b2 , where ρ is the 0, the inflated region is Rε = i [max(0, li −ε), min(1, ui +ε)] componentwise ReLU, the hidden layer has width H (so W1 ∈ (so R0 = R, Rε ⊆ D). Given a claim holding on R RH×d , b1 ∈ RH , W2 ∈ Rk×H ), and all weights are rational for g, its certified radius is ε∗ = sup{ε ∈ [0, εmax ] : (every IEEE float is a rational, and the prover hands the solver (h, Rε , ▷) holds for g}, with εmax a fixed upper bound on the exact rationals). We write fh for output coordinate (“head”) the inflation considered, chosen large enough that Rεmax = D. h ∈ {1, . . . , k} and, for each hidden neuron j ∈ {1, . . . , H}, Remark 1 (the certified object and the float gap). Certificates the pre-activation of neuron j is prej (x) = (W1 x+b1 )j . Every are statements about the exact rational network f under real such f is continuous and piecewise-linear; the input domain arithmetic. The executed program evaluates the same weights d is D = [0, 1] . in float64 and can differ pointwise by rounding, bounded by a Definition 2 (claim, certificate). A claim is a triplet of shape standard forward-error analysis (≈ 10−13 for our models). A (h, R, ▷) with R ⊆ D a closed box and ▷ ∈ {>, ≤}; it holds certificate proved with slack γ above that bound holds for the for g iff ∀x ∈ R : gh (x) ▷ 0. A certificate is a proof of executed program too; a zero-margin claim need not transfer. this statement, obtained by showing its negation ∃x ∈ R : The toy model’s removal, preservation and control certificates ¬(gh (x) ▷ 0) is unsatisfiable. Removal of skill A over RA are re-proved with slack γ = 10−9 , and every threshold-gate is the claim (A, RA , ≤) about the edited model (the unedited transformer certificate carries slack 10−6 (§IV, App. B).

TABLE I C ERTIFICATION O BJECT AND Q UANTIFIER D OMAIN 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; perinput 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 fidelity [10]

statistical intervention effect

expectation over an input+intervention distribution

no (average-case)

removal + preservation + certified radius of an edit

continuous input regions and their inflations

yes

This paper

interventional

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, ▷) holds and R′ ⊆ R, then (h, R′ , ▷) holds. (b) If (h, S Ri , ▷) holds for every i in any index set, then (h, i Ri , ▷) holds. The family of certified regions is thus downward closed and closed under arbitrary unions, with maximal element the truth set T = {x ∈ D : gh (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.

code treats a solver timeout conservatively as a failed probe, which preserves the soundness of ℓ ∈ S but voids the bracket (no query returned “unknown” in any experiment reported here). Full proof in App. A. 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). Q Given input dimension d ≥ 1, a removal region R = i [li , ui ] ⊆ D with l0 < u0 , any finite test set T ⊂ D, and any δ > 0, there exist a network f , a neuron set C, and the edited model g = ablate(f, C) such that: (a) the unedited f satisfies the full skill specification; (b) gA (t) ≤ 0 for every t ∈ 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) > 0} is nonempty and open, and its relative volume satisfies vol(Sg )/vol(R) < δ.

Proposition 2 (the certified radius is well-defined and cheap). Let g be a network, R a box, and suppose (h, R, ▷) holds. Let S = {ε ∈ [0, εmax ] : (h, Rε , ▷) holds}, ε∗ = sup S. Then: (a) S is an interval containing 0; (b) if ▷ is ≤, then the supremum is attained (ε∗ ∈ S); while for >, only [0, ε∗ ) ⊆ S is guaranteed; (c) for each rational ε, membership ε ∈ S is decided exactly Corollary 1 (adaptive protocols). Let P be any deterministic by the (un)satisfiability of a quantifier-free linear-real- protocol that queries an edited model at finitely many inputs arithmetic formula, for which the solver is sound and where each is possibly chosen from earlier answers and then gives its verdicts. If P approves some genuinely edited model, complete; (d) bisection returns, in at most 2 + ⌈log2 (εmax /τ )⌉ queries, it also approves some edited model that retains the skill on either a counterexample, “saturated”, or a bracket [ℓ, hi] a positive-measure set. Hence, no finite-query deterministic protocol is both sound for removal and nontrivial over any with ℓ ∈ S, hi ∈ / S, hi − ℓ ≤ τ , hence |ℓ − ε∗ | ≤ τ . region with nonempty interior. The attainment asymmetry in (b) matters for reporting: removal radii (sign ≤) are genuine maxima, whereas preservation Construction (sketch; full proof App. A). The finitely many radii (sign >) are suprema our procedure brackets within τ . test points have finitely many first coordinates; with l0 , u0 they The bracket guarantee assumes every query is answered; the leave an open interval (c − w, c + w) disjoint from all of them.

Three hidden neurons with pre-activations x0 − (c − w), x0 − c, x0 − (c + w) feed head A the combination   tentβ (x0 ) = β ρ(x0 −(c−w))−2ρ(x0 −c)+ρ(x0 −(c+w)) ,

IV. M ETHOD 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, which is a “hat” that rises to peak βw at x0 = c, returns to zero and each ReLU ρ(z) becomes the split case ite(z > 0, z, 0). A at c+w, and is identically zero thereafter (the slopes β, −2β, β claim (h, R, ▷) is proved by asserting its negation (an input in cancel); in particular it vanishes at every test point. Lowering R violating it) and obtaining unsat. Because the formula is head A’s bias by βw/2 makes gA = tentβ − βw/2 report quantifier-free linear real arithmetic (QF-LRA) over rationals, “removed” at every test point yet exceed 0 exactly on the slab the verdict is exact and complete (Proposition 2c). An unsat |x0 − c| < w/2, of relative volume w/(u0 − l0 ) < δ (Fig. 1b). certifies the claim for every point of R, whereas sat returns For Corollary 1, adding the same gadget to a genuinely edited a concrete counterexample (the solver catching an input for g0 leaves its transcript on P ’s queries unchanged, and therefore which the skill still fires; such an input might be missed by P ’s deterministic verdict is unchanged, while re-introducing a a test suite). Certified radii are found by bisecting proofs positive-measure survivor. (Proposition 2d). Every proof is cross-checked against a bruteThe scope is deliberate and stated: Cor. 1 covers deterministic force grid; because the grid runs the float program while the black-box protocols (adaptive included); a randomized adaptive solver reasons about the ideal network, disagreement beyond tester and a white-box analysis (such as the SMT solver used float noise signals a bug, and disagreement within ∼ 10−12 of in this paper) are outside it. Informal statements of P3 should zero signals a genuinely zero-margin claim (App. B). therefore always be read as “no finite deterministic blacka) Sequences and continuous noise in one solver query: box behavioral test.” The constructive proof is the recipe For a token model we quantify in a single query over all executed by our illusion experiment, and §V reports naturally token sequences × a continuous ball of embedding noise. trained illusions showing the hypothesis needs no adversarial Two encodings are available. The Boolean encoding uses constructor. Boolean token selectors (the exact discrete claim) but branches combinatorially and exceeds the time budget at every size we D. Surgery vs. steering (P4) tried. The hull relaxation replaces the discrete token choice with continuous mixture weights over the embedding simplex; Proposition 4 (edit-class separation, one hidden layer). Let the resulting region is a strict superset of the discrete inputs, so g be one-hidden-layer, C ⊆ {1, . . . , H} a neuron set, steers an unsat still certifies the discrete claim via Proposition 1a, targeted suppression at dose s, abl ablation of C, and Mj (R) = with no Boolean branching. The hull relaxation is what makes maxx∈R prej (x) (attained at a box corner). Then: P the transformer tractable, once the model is shrunk to the (a) steers,h (x) = ablh (x) + j∈C W2 [h, j] ρ(prej (x) − s) measured frontier (§V). for all x. b) Handling of the float gap: Certificates concern the (b) If s ≥ maxj∈C Mj (D) then steers ≡ abl on D, so every exact rational network while the executed model runs float64. A certificate and radius is identical. standard forward-error bound puts the gap at ≈ 10−13 here. The (c) The doses certifying a removal form an interval [s∗ (R), ∞) toy model’s removal, preservation and control certificates are rewith s∗ (R) finite and non-decreasing in R, hence s∗ (Rε ) proved with explicit slack γ = 10−9 , and every threshold-gate non-decreasing in ε (more wiggle room demands more transformer certificate carries slack 10−6 , so these certificates dose). transfer to the executed program. A constructed zero-margin (d) For a general steering vector v = sv̂, on any set of pattern- claim is proved by the solver yet violated by the float program stable points sharing active set PA ⊆ {1, . . . , H}, head by ∼ 10−16 (App. B). B’s logit shifts by exactly s j∈A W2 [B, j]v̂j —linear in dose. A circuit disjoint from head B (W2 [B, j] = B. Bound-propagation extension (CROWN) 0) yields provably zero collateral at every dose; a dataSoftmax and LayerNorm cannot be encoded exactly: their derived direction heard by head B erodes preservation in exponentiations and divisions are outside linear arithmetic. To proportion to dose and breaks it outright once the shift certify edits on a standard softmax + LayerNorm transformer we exceeds B’s margin. switch to bound propagation (auto_LiRPA [22] / CROWN [23]), P4 turns the edit comparison of §V-E from measurement which computes sound linear lower and upper bounds on the into theorem for the one-hidden-layer class: surgical edits must output over an input ball. Bound propagation is sound but show zero collateral when the circuit is disjoint from head B; incomplete: it may fail to certify a true claim, but never certifies diff-of-means steering heard by head B must erode skill B’s a false one. Two checks support its results. preserved margin linearly in dose and break it at sufficient a) M0 (validate the pipeline against the exact solver): dose. The deeper-network generalization is open (the leftover Bound propagation is sound by construction [23], so this check term propagates through later nonlinearities). P2–P4 each have (M0) validates the implementation rather than the guarantee. a machine-checked witness (App. E); P1 follows from the On the toy ReLU MLP both tools apply and the exact solver meaning of the universal quantifier. 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. b) Attack bracketing: Beyond the exact frontier we bracket every certified radius from above by a projectedgradient attack: for each claim we report certified ≤ true ≤ attack. 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. 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, so the bisection probes only balls of radius ≥ 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. F INDINGS 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 II and detailed in App. D. 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%), over continuous embedding-noise balls in 448 perturbation dimensions, roughly 9× the exact frontier established by SMT. Every radius is bracketed by attack (certified ≤ true ≤ attack): removal 0.0091 ≤ 0.03, preservation 0.0079 ≤ 0.05 and 0.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.016 and preservation to 0.013 (Table II), with the collateral quantified: skill B’s radius falls from 0.034 to 0.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 625 clean sequences, removal to radius ≥ 0.05 and preservation robust to radius ≥ 0.002 (App. D).

0.0091

0.03

removal (A ∙ 0)

0.0079

0.05

preserve (B > 0)

0.0098

0.1

preserve (B ∙ 0) 0.00

0.02

0.04

0.08

0.06

0.10

embedding perturbation radius " (L1 ) Fig. 2. Certified removal and preservation on a standard softmax + LayerNorm transformer, which the exact encoding cannot represent, over embedding-noise balls in 448 dimensions (about 9× the exact frontier of Table III). 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.

attention

MLP (8 neurons)

head 0 head 1

tokens +"

0

1

2

3

4

5

6

7

+

+

readout

residual stream

skill A circuit: head 0 + MLP neurons 1, 2, 5 Fig. 3. The certified circuit is distributed across attention and the MLP. One decoder block of the exact subject (8 wide, 2 heads, L = 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 II).

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,401point 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 160 models (from models with ≥ 4 inputs), each passing a full grid plus 1,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 × 106 uniform darts give a 95% Clopper–Pearson ceiling of 1.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). 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

TABLE II C ERTIFIED RADII ε∗ (D EF. 4) BY SUBJECT. PARENTHESIZED VALUES ARE SKILL B’ S RADIUS BEFORE THE EDIT, SO COLLATERAL READS AS THE DROP. E XACT REMOVAL RADII ARE ATTAINED TIPPING POINTS AND EXACT PRESERVATION RADII ARE BRACKETED WITHIN THE BISECTION TOLERANCE (P ROPOSITION 2 B , D ); BOUND - PROPAGATION RADII ARE SOUND LOWER BOUNDS . VALUES FROM COMMITTED REPORTS (A PP. D). Subject

Size

Toy MLP (separated) Toy MLP (entangled) Deep MLP Gate transformer Adder transformer Softmax + LN transf.

Prover

Pert. dims

d=2, 16 hidden SMT d=2, 16 hidden SMT 3-12-8-2 SMT 8 wide, 2 heads SMT (hull) p=5, 8 wide, 2 heads SMT (siamese) 64 wide, 4 heads, 2 layers CROWN

Removal ε∗

Preservation ε∗ (unedited)

≥ 0.6 a ≥ 0.6 a

0.0996 (0.0996) 0.0961 (0.0961) 0.0742 (0.0938) b 0.0125 (0.0344) ≥ 0.002 c 0.0079, 0.0098 d

2 2 3 ≥ 0.5 a 48 0.0156 40 ≥ 0.05 a 448 0.0091 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 625 clean sequences at ε=0. d attack-bracketed: 0.0091 ≤ 0.03, 0.0079 ≤ 0.05, 0.0098 ≤ 0.1.

free

tied

edited g

x0

x1 ; …; xd ¡ 1

gA (x)

= y1 ; …; yd ¡ 1

(b) 0.508

jgA (x) ¡ gA (y)j > ∙ ? gA (y)

R

0.6

unsat: proved influence ∙ ∙

certified edge 0:6 ¡ " ¤

0.504

gB = 0

x1

y0

(a) 1.0

sat: a pair (x; y) refutes ∙

bisection on ∙ gives the certified influence

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 (x0 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 0 certifies feature non-interference.

in the head’s output as the forbidden input varies over the whole domain. On the transformer the certified influence reaches exactly 0, 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 22 to < 0.001; on a deliberately entangled “messy” model the edit certifies removal yet influence falls only from 63 to 10, quantifying that removal is not deafness. The illusion edit is refuted here too, with a concrete input pair and influence ceiling 0.60—exactly the tent’s height.

"

rule x1 = 0:5

0.500

¤

0.0039

counterexample

0.5 0.4

0.496 0

x0

1

0

x0

1

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] (Table II). (a) R (dashed) and its inflation by the certified radius ε∗ = 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.5 (dotted). The certified edge stops 0.0039 above the rule, within the bisection tolerance of the highest point of the edited model’s own decision boundary gB = 0 (solid), at x0 = 0. At the smallest refuted inflation the solver returns a counterexample (star) beyond that boundary.

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.0996 to 0.0908 at dose 4 and to 0.0656 at dose 16, 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 D. Removal is robust to input perturbation, up to a certified B (App. D). A sparse-autoencoder feature clamp, on a model where skill A splits across three features, is certified by the radius same prover: removal to radius ≥ 0.5 and preservation to Removal and preservation hold not only on the claimed 0.064, against ablation’s 0.100 on the same model (App. D). region but on its inflation by the certified radius (Def. 4). The dose→collateral claim rests on P4(d)’s proven linearity Read on the region’s edge, the radius measures tightness plus a full dose sweep (Fig. 6b). (Proposition 2): the inflated edge stops where the edited model’s own decision boundary does, not at a margin added by the F. The exact verification frontier and its sound extension prover (Fig. 5). Across the correctness claims of both toy The exact frontier is set by internal branching: the Boolean models, certified edges reach within 0.0012 of the 0.5 rule for encoding’s cost is exponential in the model’s case splits, and skill A and within 0.0039 at worst. The residual gap is the it exceeds the time budget at every size. The shrink-plusmodel’s decision margin, not prover slack. hull-relaxation path reaches a two-head transformer exactly

(a) separated model entangled model

0.0996 0.0961

weight edit

0.0996 0.0961

targeted steering

0.0996 0.0961

diff-of-means

dose 3

0.10

skill B certified radius

ablation

(b) unedited

removes A too weak to remove A preservation of B refuted

0.08 0.06 0.04 0.02

0.0932

dose 5

0.0791

0.07

0.08

0.09

skill B certified radius

0.10

0.00

0

10

20

30

40

50

diff-of-means steering dose

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.999), consistent with Proposition 4(d), until preservation is refuted (cross).

TABLE III (Table III). Bound propagation goes past it, validated to equal the exact radius on every claim where both provers apply— W HERE EXACT CERTIFICATION STOPS . E ACH ROW IS A CONFIGURATION OF THE THRESHOLD - GATE TRANSFORMER ; EACH CELL IS ONE 0.5=0.5 for removal and 0.0996=0.0996 for both preservation ALL - SEQUENCES HULL QUERY OF THE UNEDITED MODEL’ S SKILL -A CLAIM , claims (M0)—and attack-bracketed beyond (M1). Finally, the WITHOUT NOISE OR WITH IT. T HE RULE MARKS THE FRONTIER ; THE EXACT SUBJECT OF TABLE II HAS THE BOLD ROW ’ S SIZE , WITH TWO HEADS . continuous radius is not a disguised discrete-robustness claim. The smallest single-token swap moves the embedding by 2.94, Configuration Noise vars ε = 0 ε = 0.005 some ≈ 324× the certified ball, so the continuous guarantee 8 wide, 1 head, L = 4 32 ✓ 32 s ✓ 155 s and discrete-prompt robustness are different objects (App. D). 8 wide, 1 head, L = 6 48 ✓ 40 s ✓ 230 s Taken together, the findings answer the three gaps of 8 wide, 1 head, L = 8 64 too loose too loose §II. First, an edit’s effect can be proved rather than sam12 wide, 1 head, L = 6 72 ✓ 31 s timeout pled: on every subject, from a two-input network to a soft16 wide, 1 head, L = 6 96 ✓ 120 s timeout 16 wide, 2 heads, L = 8 128 timeout timeout max + LayerNorm transformer, removal and preservation hold for every input in a continuous region, and on the toy models ✓ proved, with solver time; too loose: the hull relaxation is inconclusive; the exact certificates stop at the model’s own decision boundary, timeout: exceeds the 300 s query budget, and the 128-variable row also exceeds 30 min at ε ∈ {0.01, 0.05}. 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 Input region instead of arbitrary prompt: The guarantee them with a concrete input. Third, the choice of edit is itself is over a class of token sequences × a continuous embedding certifiable: surgical edits remove a skill with provably zero ball. In the exact cases this covers every discrete prompt in the collateral, whereas steering trades removal against collateral in model’s input space and a continuous neighborhood of each a way no dose resolves. For a practitioner validating a safety (a superset of all possible prompts). But the continuous axis edit, the certificate therefore replaces the test set as the evidence is embedding-space noise. A certified radius is not a discretethat the edit did what it was meant to do, within the scale prompt-edit distance, and indeed a single token swap is ≈ 324× bound that §VI states. the certified ball (§V-F). We therefore claim continuous-region robustness, not frontier-scale prompt robustness. VI. L IMITATIONS AND S COPE The decidable-oracle assumption: Every skill we certify Scale: Guarantees are proved on small, standard-architecture has a decidable ground truth, a computable function such networks; the exact frontier is exponential in internal branching as “input contains more « than »” or (a + b) mod p, which (§V-F), and bound-propagation results, while sound, are not is exactly what makes “removed” or “preserved” a crisp, exact. Wide certified-to-attack gaps reflect prover looseness, checkable claim. Real harmful capabilities in frontier models and radii are reported over balls of radius ≥ 10−4 (CROWN have no such decidable oracle: whether an output “exhibits is degenerate at ε = 0). The edit on the softmax model is a a harmful skill” is contested and, in general, undecidable. position path-patch, not a component circuit, because a from- The certified-removal setup therefore presupposes a decidable scratch softmax transformer yields no separable head/MLP specification of the target skill, and that assumption does not circuit. 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. C ONCLUSION AND F UTURE W ORK 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. O PEN S CIENCE 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 boundpropagation 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. E THICAL C ONSIDERATIONS 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. R EFERENCES [1] A. Wei, N. Haghtalab, and J. Steinhardt, “Jailbroken: How does llm safety training fail?” Advances in neural information processing systems, vol. 36, pp. 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, pp. 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, “Hairtrigger alignment: Black-box evaluation cannot guarantee post-update alignment,” in Proceedings of the 6th Workshop on Trustworthy NLP (TrustNLP 2026), 2026, pp. 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, pp. 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, pp. 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, pp. 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.

[ℓ, hi] with ℓ ∈ S, hi ∈ / S—valid because S is an interval by (a)—halving hi − ℓ once per query until hi − ℓ ≤ τ , i.e. ⌈log2 (εmax /τ )⌉ queries. Since ℓ ≤ ε∗ ≤ hi, |ℓ − ε∗ | ≤ τ . The bracket half of the guarantee assumes each probe is answered; treating “unknown” as a failed probe preserves soundness of ℓ ∈ S but voids |ℓ − ε∗ | ≤ τ .

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 }; together with l0 , u0 these leave an open interval A PPENDIX A (c − w, c + w) ⊂ (l0 , u0 ) disjoint from all of them (finitely F ULL P ROOFS OF P1–P4 many points cannot cover an interval: pick c strictly between Throughout, g is a network of Definition 1, so gh is two consecutive such values and w below half the gap). Shrink continuous and piecewise-linear on D = [0, 1]d ; “claim”, w further if needed so w < δ(u0 − l0 ). Take three hidden “certificate”, “edit”, “inflation” and “certified radius” are as neurons with pre-activations x0 − (c − w), x0 − c, x0 − (c + w) in Definitions 2–4. and feed head A   A. Proposition 1 (region monotonicity and union closure) tentβ (x0 ) = β ρ(x0 −(c−w))−2ρ(x0 −c)+ρ(x0 −(c+w)) . Proof. Both parts are immediate from the meaning of the A case check on the four intervals cut by c − w, c, c + w universal quantifier. (a) A statement true of every point of R is shows tentβ is the “hat”: zero for x0 ≤ c − w, rising linearly ′ true of every point of any R ⊆ R. (b) A statement true of every S to peak βw at x0 = c, falling to zero at x0 = c + w, and point of each Ri is true of every point of i Ri . Consequently identically zero thereafter (the slopes β, −2β, β cancel). In the union of all certified regions is itself certified and contains particular tentβ ≥ 0 and tentβ (t0 ) = 0 at every test point. every certified region; it equals the truth set T = {x ∈ D : The model. Let f consist of a main pathway for skill A with gh (x) ▷ 0} because each singleton {x} ⊆ T is certified, and decision margin exceeding βw/2 on A’s specification regions; any certified region is a subset of T by definition. an untouched pathway for skill B reading only x1 (zero weight from the gadget into head B); the gadget neurons into head B. Proposition 2 (the certified radius) Proof. Write loi (ε) = max(0, li − ε), hii (ε) = min(1, ui + ε). A; and head-A bias lowered by βw/2 (the “hurdle”). Let C (a) Interval structure. If ε′ ≤ ε then loi (ε) ≤ loi (ε′ ) and be the main-pathway A-neurons and g = ablate(f, C). (a) Pre-edit, head A = main(x0 ) + tentβ (x0 ) − βw/2. On hii (ε′ ) ≤ hii (ε) coordinatewise, so Rε′ ⊆ Rε ; the claim on A’s HIGH region the main margin exceeds βw/2 and tentβ ≥ Rε then gives the claim on Rε′ by Proposition 1(a). Hence S 0, so head A > 0; on A’s LOW region the bump is absent is downward closed in [0, εmax ] and contains 0, i.e. an interval. (it lies inside HIGH, so tentβ = 0 there), the main pathway (b) Attainment. Non-strict sign ≤: fix x ∈ Rε∗ ; we show is nonpositive, and the hurdle only lowers it, so head A ≤ 0. gh (x) ≤ 0. Each endpoint is 1-Lipschitz in ε and loi (ε) ≤ li ≤ Skill B’s claims hold as its pathway is disjoint from the gadget ∗ ui ≤ hii (ε), so every Rε is a nonempty box. For ε < ε let and C. x(ε) be the coordinatewise clip of x into Rε ; then x(ε) ∈ Rε (b) Post-edit, gA (x) = tentβ (x0 ) − βw/2. At each t ∈ T , and |x(ε)i − xi | ≤ ε∗ − ε, so x(ε) → x as ε ↑ ε∗ . Choose tent ∗ ∗ β (t0 ) = 0, so gA (t) = −βw/2 < 0; and B’s pathway, εn ↑ ε with εn ∈ S (possible since S ⊇ [0, ε ) by (a)); then untouched and receiving nothing from the gadget, preserves gh (x(εn )) ≤ 0, and by continuity gh (x) = limn gh (x(εn )) ≤ both claims on their full regions. ∗ ∗ ∗ 0. Hence ε ∈ S. Strict sign >: [0, ε ) ⊆ S is (a); that ε (c) gA (x) > 0 iff tentβ (x0 ) > βw/2 iff |x0 − c| < w/2; so may fail is shown by d = 1, g(x) = ρ(0.5 − x), claim g > 0 Sg = {x ∈ R : x0 ∈ (c − w/2, c + w/2)} is open, nonempty, on R = [0, 0.2]: then Rε = [0, 0.2 + ε] and the claim holds of relative volume w/(u0 − l0 ) < δ. iff 0.2 + ε < 0.5, so S = [0, 0.3) and at ε∗ = 0.3 the point x = 0.5 gives g(x) = 0 ̸> 0. Corollary 2 (random testing). A test drawing m i.i.d. uniform V (c) Decidability. The negated claim is ∃x : i (loi ≤ xi ≤ points from R wrongly approves g with probability at least hii )∧¬(gh (x)▷0), where gh (x) is built from rational constants, (1 − δ)m ≥ 1 − mδ. addition, multiplication-by-constant, and ite(z > 0, z, 0) terms. Proof. By Proposition 3(c), each draw lands in Sg with Eliminating each ite into a disjunction of two linear cases yields probability below δ; independence gives miss probability a quantifier-free formula of linear real arithmetic; satisfiability > (1 − δ)m ≥ 1 − mδ (Bernoulli). For the constructed gadget of QF_LRA is decidable (e.g. by simplex-based DPLL(T)), the pocket volume is exact; for the naturally-trained illusions and with rational inputs the answer is exact. A solver timeout of §V-B it is only sampled (zero hits in 2 × 106 darts, a 95% returns “unknown”, which the implementation reports rather Clopper–Pearson ceiling of 1.5 × 10−6 ). than treating as either verdict. (d) Cost bound. One query at ε = 0 (vacuity) and one Proof of Corollary 1. Run the deterministic protocol P against at εmax (saturation); thereafter bisection maintains a bracket a genuinely edited g0 (g0,A ≤ 0 on all of R); it queries a

finite set T ′ and approves. Apply the gadget to T ′ : choose (c − w, c + w) avoiding T ′ ’s first coordinates and add the three tent neurons to head A with pattern (β, −2β, β) and no bias change, giving g = g0 + tentβ on head A. Since tentβ vanishes at every point of T ′ , g agrees with g0 at every query, so P ’s transcript—and hence its verdict, P being deterministic— is identical: P approves g. But g0,A is continuous on the compact R, hence bounded below by some −G; choosing β with βw/2 > G makes gA > 0 on |x0 − c| < w/2, a positivemeasure set. (g is a legitimate edited model: add the same gadget to g0 ’s parent and ablate the same C.)

A PPENDIX B E XACT E NCODING D ETAILS AND THE F LOAT G AP

The encoding converts every weight to an exact rational and every ReLU to an ite 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 for our models. The toy model’s removal, preservation and control certificates re-prove with slack γ = 10−9 (prove_forall(...,slack=γ)), and every thresholdgate transformer certificate carries slack 10−6 . A constructed zero-margin claim proved exactly yet violated by the float program by ∼ 10−16 on about a quarter of a region is the Scope. Corollary 2 covers i.i.d. uniform sampling; Corollary 1 boundary of the transfer argument; region endpoints are float covers deterministic black-box protocols (adaptive included). constants too (∼ 10−17 from the stated rationals), immaterial A randomized adaptive tester (transcript replay yields only a at our margins. fooling probability) and a white-box analysis such as the SMT solver used here are deliberately outside the statements—the A PPENDIX C latter escape being the paper’s point. B OUND -P ROPAGATION S ETUP D. Proposition 4 (edit-class separation)

CROWN bounds are computed in chunks with gradients disabled during certification for memory safety; radii are reported over balls of radius ≥ 10−4 (CROWN is degenerate at ε = 0). Every certified radius is bracketed above by a projectedgradient attack, and the bound-propagation dependencies are isolated from the pure numpy+SMT exact pipeline.

Proof. (a) Neurons outside C have identical pre-activations and outputs under steers and abl. A neuron j ∈ C outputs ρ(prej (x)−s) under steers and 0 under abl, where prej is the unedited pre-activation. Heads are affine in the neuron outputs with P coefficients W2 [h, ·], so the head difference is exactly A PPENDIX D j∈C W2 [h, j] ρ(prej (x) − s). R EPRODUCIBILITY (b) prej is affine, so its maximum over the box D is at a corner, giving Mj (D). If s ≥ Mj (D) for all j ∈ C then every Each reported result is regenerated by one command from leftover term is 0 on D, so by (a) the two edited models are committed code and fixed seeds; Table IV maps every result equal as functions; equal functions satisfy the same claims to its script. over every region, hence share every certificate and certified A PPENDIX E radius. M ACHINE -C HECKED W ITNESSES (c) Each leftover term is nonincreasing in s (ρ nondeP2–P4 each have a runnable check (P1 follows from the creasing, its argument decreasing), so maxx∈R [ablA (x) + P meaning of the universal quantifier): P2’s query-count bound W [A, j]ρ(pre (x) − s)] is nonincreasing in s; the 2 j j∈C certifying condition “≤ 0” therefore holds on an up-closed set with re-proof at the returned radius and re-refutation just [s∗ (R), ∞), nonempty because at s = maxj Mj (D) it reduces past it; P3’s per-grid gadget with the survivor located in the to abl’s certificate by (b). Enlarging R can only enlarge the predicted sliver c ± w/2; the adaptive-tester transcript replay max, so s∗ grows; Rε is monotone in ε (Proposition 2a). The for Corollary 1; P4(a)’s leftover identity at 2 × 105 random left side is continuous in s (finite max over compact R of a inputs and several doses, P4(b)’s corner-formula threshold, and jointly continuous function), so the non-strict inequality passes P4(d)’s pattern-stable collateral constant per observed activation pattern. The margin-curve dose sweep (Table IV) exercises to the limit and s∗ (R) is attained. (d) Applying the same affine-head argument to steerv and P4(c). All checks pass. the unedited g gives X   steerv,h (x)−gh (x) = W2 [h, j] ρ(prej (x)+vj )−ρ(prej (x)) . j

At a pattern-stable x with active set A: a neuron active in both contributes ρ(prej + vj ) − ρ(prej ) = vj , one inactive in both contributes 0, and terms with vj = 0 vanish; the sum P reduces to W2 [h, j]vj , independent of x. With v = sv̂ j∈A P this is s j∈A W2 [B, j]v̂j for head B—linear in s. A circuit C with W2 [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.

TABLE IV T HE COMMAND BEHIND EACH REPORTED RESULT. Result

Script

Softmax + LayerNorm transformer, 448 noise dimensions: certified ≤ attack for removal and both preservation claims (Fig. 2) Threshold-gate transformer, exact over all sequences: removal 0.016, preservation 0.013, collateral 0.034 → 0.013 (Table II) Distributed circuit: neither the attention heads nor the MLP alone removes skill A (Fig. 3) Modular-adder transformer: removal as exact independence of the summands, radius ≥0.05 (§V-A) Modular-adder transformer: correctness on all 625 clean sequences, preservation radius ≥0.002 (§V-A) Constructed illusion: passes a 40,401-point grid with preservation proved, refuted by the solver (Fig. 1a,b) Three naturally trained illusions in 160 four- and five-input models (§V-B) Illusions per input dimension, 80 models each; the d = 4, 5 rows reproduce the pooled run exactly (Fig. 1c) Certified influence exactly 0 on the transformer (§V-C) Certified influence on the separated and entangled models; the illusion edit refuted with an input pair (§V-C) Certified boundary within 0.0012 of the model’s decision rule (§V-D) Certified edge against the model’s own decision boundary (Fig. 5) Radii per edit type on the two toy subjects (Table II, §V-E) Deep MLP: four-neuron layer-1 circuit and its collateral (Table II) Steering dose sweep over doses 0.5–64 (§V-E) On the transformer, no steering dose both removes A and preserves B (§V-E) SAE feature-clamp edit certified by the same prover (§V-E) Edit-type tables on the transformer and the modular adder (§V-E)

run_boundprop_transformer.py†

Exact-frontier size ladder and encoding timeouts (§V-F) M0: bound propagation equals the exact radius where both apply (§IV-B) Smallest token swap is ≈324× the certified ball (§V-F) Float-gap ceiling and slack re-proofs (App. B) Machine-checked witnesses for P1–P4 (App. E)

run_transformer.py results/rung2_circuit_search.pyb run_rung3.py run_rung3_preservation.py run_illusion.py run_illusion_nd.py run_illusion_dims.py run_transformer_independence.py run_independence.py run_margin_curve.py run_robustness.py run_robustness.py run_deep_multi.py run_collateral_sweep.pya run_transformer_steering.py run_sae_clamp.py run_transformer_edit_table.py run_rung3_edit_table.py results/rung2_size_ladder.pyb results/rung2_hull_wall.pyb run_boundprop_validate.py† run_boundprop_quantifier.py† run_float_gap.py run_theory_checks.py

Each script run_⟨name⟩.py writes results/⟨name⟩_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.

Related documents

• Certified Mechanistic Edits: Behavioral Guarantees for Skill Removal and Preservation#1188180
• Certified Interventional Fidelity: Anytime-Valid, Adaptive Evaluation of Causal Claims in Mechanistic Interpretability#353083
• Mechanization Singularity live performance#430059
• Rethinking Circuit Evaluation: Do Circuits Explain Model Errors?#1130338
• Rethinking Circuit Evaluation: Do Circuits Explain Model Errors?#1108755