BlockCert: Certified Blockwise Extraction of Transformer Mechanisms

BlockCert: Certified Blockwise Extraction of Transformer Mechanisms Sandro Andric sandro.andric@nyu.edu (November 2025) Abstract Mechanistic interpretability aspires to reverse-engineer neural networks into explicit algorithms, while model editing seeks to modify specific behaviours without retraining. Both areas are typically evaluated with informal evidence and ad-hoc experiments, with few explicit guarantees about how far an extracted or edited model can drift from the original on relevant inputs. We introduce BlockCert, a framework for certified blockwise extraction of transformer mechanisms, and outline how a lightweight extension can support certified local edits. Given a pre-trained transformer and a prompt distribution, BlockCert extracts structured surrogate implementations for residual blocks together with machine-checkable certificates that bound approximation error, record coverage metrics, and hash the underlying artifacts. We formalize a simple Lipschitz-based composition theorem in Lean 4 that lifts these local guarantees to a global deviation bound. Empirically, we apply the framework to GPT-2 small, TinyLlama-1.1B-Chat, and Llama-3.2-3B. Across these models we obtain high per-block coverage and small residual errors on the evaluated prompts, and in the TinyLlama setting we show that a fully stitched model matches the baseline perplexity within ≈6×10−5≈ 6× 10^-5 on stress prompts. Our results suggest that blockwise extraction with explicit certificates is feasible for real transformer language models and offers a practical bridge between mechanistic interpretability and formal reasoning about model behaviour. 1 Introduction Large language models (LLMs) have rapidly become core infrastructure for scientific research, software engineering, and high-stakes decision support. At the same time, we still lack robust tools for understanding, validating, and safely modifying their internal mechanisms. Mechanistic interpretability aims to address this by reverse-engineering neural networks into human-understandable components and circuits [olah2020zoom, elhage2022toymodels, nanda2023progress], but existing work is typically evaluated with bespoke visualizations or small-scale experiments, without explicit, machine-checkable guarantees. In parallel, the formal-methods community has developed powerful tools for proving properties of neural networks [katz2017reluplex, katz2019marabou, wang2021betacrown], and the programming-languages community has shown how to ship code with machine-checkable proofs of safety (proof-carrying code) [necula1997pcc]. However, these lines of research have had limited impact on day-to-day interpretability practice. Verification tools often do not scale to modern LLMs, and proof obligations are difficult to relate to the informal, circuit-level stories that interpretability researchers actually use. Goal. We would like a middle ground between fully formal verification and informal interpretability stories: a workflow in which reverse-engineered mechanisms are accompanied by explicit certificates that (i) precisely specify what has been extracted, (i) quantify how closely the extract matches the original network on concrete data, and (i) can be automatically checked by any third party with access to the artifacts. Ideally, these local certificates can then be composed to reason about global model behavior. This paper. We propose BlockCert, a framework for certified blockwise extraction of transformer mechanisms. Given a pre-trained transformer, a set of prompts, and access to intermediate activations, BlockCert produces, for each residual block: 1. a structured surrogate implementation B^i B_i in an explicit intermediate representation, and 2. a JSON certificate describing the data distribution used for extraction, the achieved approximation error and coverage metrics, and cryptographic hashes of the associated artifacts (weights, probes, masks). An independent verifier can re-load the artifacts, recompute the metrics, and check that the hashes match. We also provide a composition mechanism that aggregates per-block certificates into a full-model certificate summarizing stitched-model replay metrics. We further formalize a simple global bound: if each baseline/stitched block pair (Bi,B^i)(B_i, B_i) is locally εi _i-sound and the blocks are LiL_i-Lipschitz, then the composed stitched model is globally bounded by a Lipschitz-weighted sum of the εi _i, which specializes to a ∑iεi _i _i bound when Li≤1L_i≤ 1. This theorem is mechanized in Lean 4 and instantiated for TinyLlama using empirical per-block error bounds. Why blockwise? Transformers are naturally modular: the computation is organized into a stack of residual blocks [vaswani2017attention]. Many mechanistic interpretability techniques operate at the block level (e.g. activation patching, MLP feature analysis), as do many model-editing methods that target specific layers [meng2022rome, meng2022memit, yao2023editingllms]. By focusing on per-block extraction with quantitative guarantees, BlockCert aims to produce artifacts that are simultaneously: • close to the original computation on a specified input distribution, • simple enough to inspect and modify, • and accompanied by machine-checkable evidence of correctness. Contributions. Our main contributions are: (1) we formalize the problem of blockwise extraction for transformers and propose BlockCert, a pipeline that produces explicit surrogate blocks together with JSON certificates recording per-block approximation error, coverage metrics, and cryptographic hashes of the underlying artifacts; (2) we introduce simple but practical coverage notions (activation, path, and loss coverage) that quantify how much of a block’s behavior on a given prompt set is explained by the surrogate, and integrate these into a certificate format and verification tool; (3) in a separate Lean 4 development, we prove a global composition theorem showing that if each (Bi,B^i)(B_i, B_i) pair is locally bounded by εi _i and blocks are LiL_i-Lipschitz, then the fully composed stitched model is globally bounded by a Lipschitz-weighted sum of the εi _i, which reduces to ∑iεi _i _i when Li≤1L_i≤ 1, and we instantiate this theorem using empirical error bounds from TinyLlama block certificates and stitched-model perplexity on stress prompts; and (4) we empirically evaluate BlockCert on GPT-2 small, TinyLlama-1.1B-Chat, and Llama-3.2-3B, obtaining high coverage (often ≥0.94≥ 0.94 and sometimes 1.01.0) and small approximation errors, and showing that for TinyLlama the stitched model matches the baseline perplexity within ≈6×10−5≈ 6× 10^-5 on challenging prompts. Model + prompts → Block traces → IR blocks + metrics ↓ Extraction / edit certificates Figure 1: High-level BlockCert/BlockCert-Edit workflow. Given a pre-trained transformer and a prompt distribution, we record block-level traces, construct IR surrogates with local error and coverage metrics, and package these into machine-checkable certificates. BlockCert-Edit applies simple local edits (e.g., scaling or swapping mechanisms) and produces analogous edit certificates on the same prompt distribution. Our implementation is released as an open-source Python package. To avoid confusion with historical naming, we refer to the method as BlockCert throughout this paper. 2 Background And Problem Setup 2.1 Transformers And Residual Blocks We consider standard decoder-only transformer language models [vaswani2017attention, brown2020gpt3], which map a sequence of tokens (x1,…,xT)(x_1,…,x_T) to logits over the vocabulary at each position. The computation proceeds through a stack of L residual blocks. Let t(0)∈ℝd x^(0)_t ^d denote the token embedding at position t, and let t(ℓ) x^( )_t be the residual stream at layer ℓ . A typical block has the form t(ℓ+1)=t(ℓ)+MLPℓ​(t(ℓ))+Attnℓ​(1:T(ℓ)), x^( +1)_t= x^( )_t+MLP_ ( x^( )_t )+Attn_ ( x^( )_1:T ), (1) with pre- or post-layer normalization and model-specific details. We write BℓB_ for the function mapping 1:T(ℓ) x^( )_1:T to 1:T(ℓ+1) x^( +1)_1:T. The full model is the composition F=BL−1∘⋯∘B0∘E,F=B_L-1 ·s B_0 E, where E is the embedding and positional encoding. 2.2 Mechanistic Interpretability And Editing Mechanistic interpretability aims to understand neural networks by decomposing them into circuits of features and connections [olah2020zoom, elhage2022toymodels]. Recent work has identified circuits in vision and language models, studied superposition and polysemantic neurons, and proposed tools for tracing and editing mechanisms [nanda2023progress, zhang2024activationpatchingreview]. Model-editing methods such as ROME [meng2022rome], MEMIT [meng2022memit], and subsequent surveys [yao2023editingllms, wang2023knowledgeEditingSurvey] modify parameters of pre-trained LLMs to update specific facts or behaviors without full retraining. These approaches provide compelling evidence that specific mechanisms can be isolated and manipulated. However, they usually lack explicit guarantees that the edited or extracted mechanism faithfully reproduces the original network across a clearly specified set of inputs. Moreover, interpretability artifacts are rarely packaged in a way that allows independent verification. 2.3 Neural Network Verification And Proof-Carrying Code Formal verification of neural networks aims to prove properties such as robustness or safety under input perturbations [katz2017reluplex, katz2019marabou, wang2021betacrown]. Tools such as Reluplex, Marabou, and α,βα,β-CROWN combine SMT solving and linear bound propagation to derive provable guarantees for moderately sized models. However, these methods typically treat the network as a monolithic object and reason about worst-case behavior under carefully specified constraints. In programming languages, proof-carrying code (PCC) [necula1997pcc] showed how to ship low-level code together with a machine-checkable proof that it satisfies a given safety policy. The host system verifies the proof before executing the code and does not need to trust the code producer. BlockCert takes inspiration from PCC: instead of shipping general-purpose proofs, we attach certificates to extracted mechanisms, which can be checked automatically by a lightweight verifier. 2.4 Blockwise Extraction Problem Fix a pre-trained transformer with blocks B0,…,BL−1B_0,…,B_L-1. We assume access to: • the model weights, • an instrumentation mechanism that records intermediate activations for a set of prompts P, • and a target block index ℓ . For block ℓ , we define a trace dataset: ℓ=(1:T(ℓ),1:T(ℓ+1),ℓ)|prompt ​p∈,D_ = \( x^( )_1:T, x^( +1)_1:T, m_ )\ |\ prompt p \, (2) where ℓ m_ contains any additional discrete information about the block’s computation (e.g. attention masks, head-level gating decisions). The blockwise extraction problem is: Given (Bℓ,ℓ)(B_ ,D_ ), construct an explicit surrogate implementation B^ℓ B_ and a certificate CℓC_ such that B^ℓ B_ approximates BℓB_ on ℓD_ according to quantitative metrics recorded in CℓC_ , and such that CℓC_ can be automatically re-verified from the released artifacts. The next sections describe our intermediate representation, extraction algorithm, and certificate semantics. 3 BlockCert Intermediate Representation 3.1 Design Goals The BlockCert intermediate representation (IR) is designed to satisfy three constraints: 1. Expressive enough to exactly represent standard transformer blocks. 2. Simple enough to be replayed by a small, auditable interpreter. 3. Stable under extraction: the mapping from (Bℓ,ℓ)(B_ ,D_ ) to B^ℓ B_ should be well-conditioned. At a high level, the IR mirrors the usual decomposition of a transformer block into attention, MLP, and residual components, but flattens model-specific details into explicit weight tensors and masks stored in .npz files: • attention weights (Q,K,V,O)( W_Q, W_K, W_V, W_O), • MLP weights (1,2)( W_1, W_2) and biases, • layer norm parameters, • an explicit attention mask ℓ M_ encoding causal structure and any additional head- or token-level gating. In our experiments we instantiate this IR for standard decoder-only architectures (GPT-2 small, TinyLlama-1.1B-Chat, Llama-3.2-3B). For GPT-2 we follow the HuggingFace GPT2Model implementation with post-embedding layer normalization and a causal attention mask. For Llama-family models we match the LlamaAttention module, including pre-layer-normalization, rotary position embeddings (RoPE) via stored cos/sincos/sin tables and position ids, and multi-query attention with num_heads and num_key_value_heads. The interpreter is implemented as a pure Python function that applies these linear and elementwise operators in a fixed order, without any hidden control flow, so that the behavior of B^ℓ B_ is determined entirely by the released weight and mask tensors. Extraction procedure in our experiments. In all experiments we use the simplest instantiation of the extraction map (Bℓ,ℓ)↦B^ℓ(B_ ,D_ ) B_ : the surrogate B^ℓ B_ has the same architecture as BℓB_ , with weights copied directly into the IR tensors and masks, positional tables, and bias tensors derived from a single traced run on ℓD_ . We do not perform any additional fitting, pruning, or distillation; residual errors arise only from numerical differences between the native implementation and the IR interpreter. 3.2 Empirical Local Soundness And Coverage Let B^ℓ B_ be an IR block and let ℓD_ be the trace dataset. We define empirical local soundness and coverage metrics on ℓD_ as follows. Per-token error. For each traced prompt p∈p and token position t, we compute the per-token residual error eℓ​(p,t)=‖^t(ℓ+1)−t(ℓ+1)‖2,e_ (p,t)\;=\; \| x^( +1)_t- x^( +1)_t \|_2, (3) where ^t(ℓ+1) x^( +1)_t is produced by B^ℓ B_ when replayed on the recorded input 1:T(ℓ) x^( )_1:T. We define: εℓ _ =max(p,t)⁡eℓ​(p,t), = _(p,t)e_ (p,t), (4) MAEℓ _ =1|ℓ|​∑(p,t)eℓ​(p,t). = 1|D_ | _(p,t)e_ (p,t). (5) Activation coverage. We fix a small threshold τact _act (e.g. 10−210^-2) and define activation coverage as covact​(ℓ)=1|ℓ|​∑(p,t)​[eℓ​(p,t)≤τact].cov_act( )\;=\; 1|D_ | _(p,t)1 [e_ (p,t)≤ _act ]. (6) Intuitively, this is the fraction of tokens for which the block output is reproduced up to a small numerical tolerance. Path coverage. We define path coverage as the fraction of traced tokens for which all discrete control decisions (e.g. attention masks, head-level gating, conditional branches) match exactly between BℓB_ and B^ℓ B_ . This is computed by replaying B^ℓ B_ with instrumented hooks that compare its mask and gating tensors to those recorded in ℓ m_ . Loss coverage. Finally, we measure the effect of the block approximation on the model’s token-level loss for the traced prompts. Let ℓbase​(p,t) _base(p,t) be the negative log-likelihood of the target token under the original model, and ℓstitched​(p,t) _stitched(p,t) the loss when block ℓ is replaced by B^ℓ B_ while all other blocks remain unchanged. We define the per-token loss difference Δ​ℓ​(p,t)=|ℓstitched​(p,t)−ℓbase​(p,t)| _ (p,t)= | _stitched(p,t)- _base(p,t) | (7) and the loss coverage covloss​(ℓ)=∑(p,t)ℓbase​(p,t)⋅​[Δ​ℓ​(p,t)≤τloss]∑(p,t)ℓbase​(p,t),cov_loss( )\;=\; _(p,t) _base(p,t)·1[ _ (p,t)≤ _loss] _(p,t) _base(p,t), (8) where τloss _loss is a small threshold (e.g. 10−310^-3). This measures what fraction of the baseline loss is accounted for by tokens whose loss is essentially unaffected by replacing BℓB_ with B^ℓ B_ . Certified blocks. A block is considered certified at level (αact,αloss)( _act, _loss) if covact​(ℓ) _act( ) ≥αact, ≥ _act, (9) covloss​(ℓ) _loss( ) ≥αloss. ≥ _loss. (10) In our experiments we typically use αact=0.94 _act=0.94 and αloss=0.9 _loss=0.9 for large models, and occasionally obtain αact=1.0 _act=1.0 on stress prompts for some blocks. Because εℓ _ and the coverage metrics are computed only on the finite trace set ℓD_ , these certificates express an empirical local soundness guarantee rather than a universal bound over all possible inputs. 4 Certificates And Verification 4.1 Certificate Format For each extracted block B^ℓ B_ , we emit a JSON certificate containing: • metadata: model name, block index, prompt set description, thresholds (τact,τloss)( _act, _loss) and policies (αact,αloss)( _act, _loss); • metrics: εℓ _ , MAEℓMAE_ , activation, path, and loss coverage; • artifact digests: SHA-256 hashes of the weight, probe, mask, and bias tensors (stored in .npz files); • a declaration that the block is certified (or not) under the specified policy. Certificates live alongside their corresponding artifacts, each containing IR weights, probes, masks, per-block metrics, and a JSON certificate. 4.2 Verification Tool We provide a small Python CLI verification tool that replays certificates and checks that: 1. the SHA-256 hashes of the given artifacts match those recorded in the certificate; 2. re-computing the metrics using the current interpreter and thresholds reproduces the values stored in the certificate (up to small numerical tolerances); 3. the certified/not-certified status is consistent with the metrics and policy. For example, on a simple sanity-check experiment, the verifier recomputes the total residual ε from the released artifacts and checks that activation and loss coverage meet the certificate’s thresholds, confirming that the certificate faithfully summarizes the underlying experiment. 4.3 Full-Model Certificates We also provide a mechanism for aggregating per-block certificates into a full-model certificate. For a given model and prompt set, we: 1. stitch in the extracted blocks for a chosen subset of layers; 2. replay the full model on the prompts, computing per-layer mean absolute error (MAE) between baseline and stitched residual streams; 3. compute baseline and stitched perplexities on the prompt set; 4. construct a JSON certificate that lists all referenced block certificate hashes and records the global metrics. For TinyLlama, this process produces a full-model certificate summarizing the per-layer MAE (mean ≈0.38≈ 0.38, worst layer ≈2.03≈ 2.03, max residual ≈2.13≈ 2.13 on stress prompts) and the negligible difference in perplexity between baseline and stitched models (Section 6.5). 4.4 Certificates Versus Formal Proofs Certificates, as produced by our tooling, are replayable, hash-tied empirical summaries. They state that for a specific model checkpoint, prompt distribution, and interpreter version, re-running the computation yields the same metrics (errors, coverage, perplexity) and artifact hashes. In contrast, a formal proof—such as the composition theorem in Section 5 and its Lean 4 formalization—is a universal statement over a specified mathematical model (e.g. all x∈Xx∈ X under Lipschitz assumptions). Our block and full-model certificates should therefore be read as data-restricted evidence that the hypotheses of such theorems hold on the traced distributions, not as global guarantees for all future inputs. 5 Global Composition Theorem 5.1 Statement We now describe a simple global error bound that connects per-block local soundness (universally quantified over x∈Xx∈ X) to total model error. Let X be a normed vector space and let Bi:X→XB_i X→ X and B^i:X→X B_i X→ X be the baseline and extracted blocks for i=0,…,L−1i=0,…,L-1. Here the index i plays the same role as the layer index ℓ used in Section 3.2. Define the full models F F =BL−1∘⋯∘B0, =B_L-1 ·s B_0, (11) F F =B^L−1∘⋯∘B^0. = B_L-1 ·s B_0. (12) Theorem 1 (Global Composition). Suppose that: 1. (Local soundness) For each i there exists εi≥0 _i≥ 0 such that ‖B^i​(x)−Bi​(x)‖≤εifor all ​x∈X.\| B_i(x)-B_i(x)\|\;≤\; _i all x∈ X. (13) 2. (Lipschitz blocks) For each i there exists Li≥0L_i≥ 0 such that both BiB_i and B^i B_i are LiL_i-Lipschitz with respect to the norm ∥⋅∥\|·\|. Then for all x∈Xx∈ X, ‖F^​(x)−F​(x)‖≤∑i=0L−1(εi​∏j=i+1L−1Lj).\| F(x)-F(x)\|\;≤\; _i=0^L-1 ( _i _j=i+1^L-1L_j ). (14) A detailed proof sketch and the full Lean 4 formalization are provided in Appendix A. 5.2 Formalization And Instantiation We formalize Theorem 1 in Lean 4 in a separate module, GlobalBound.lean. The proof uses standard results about composition of Lipschitz functions and is parameterized over the norm and the set of blocks. For real transformer models, we cannot presently prove that all blocks are globally 11-Lipschitz with respect to a useful norm over the full input space. Instead, we treat the Lipschitz property as a modeling assumption and instantiate the theorem using empirical local soundness bounds derived from block certificates, together with simple analytic Lipschitz upper bounds computed from the IR weights and local ℓ2 _2 Lipschitz bounds certified for selected TinyLlama MLP sublayers (Section 6.6). In particular, given per-block constants Li\L_i\ and empirical error bounds εi\ _i\, Theorem 1 yields a global bound of the form ‖F^​(x)−F​(x)‖≤∑i=0L−1(εi​∏j=i+1L−1Lj),\| F(x)-F(x)\|\;≤\; _i=0^L-1 ( _i _j=i+1^L-1L_j ), which reduces to the familiar ∑iεi _i _i bound in the special case Li≤1L_i≤ 1 for all i. For TinyLlama-1.1B-Chat, we: • compute empirical per-block error bounds εi _i over a suite of stress prompts, using the per-token residual norms described in Section 3.2; • plug these εi _i into the Lean development to obtain a bound on ‖F^​(x)−F​(x)‖\| F(x)-F(x)\| for x drawn from the traced distribution; • empirically verify that the stitched model and baseline produce nearly identical perplexity on the same prompts (Section 6.5). Scope. It is important to emphasize that this global story is conditional. We do not claim a formal guarantee for all possible inputs of a real LLM. Instead, our theorem and experiments support a plausible global safety story under standard Lipschitz assumptions and empirical error bounds. Strengthening these assumptions—for example by deriving certified local Lipschitz bounds for specific blocks—is an important direction for future work. 6 Experiments We now instantiate BlockCert on three settings: GPT-2 small, TinyLlama-1.1B-Chat, and Llama-3.2-3B. Extraction artifacts and certificates for all experiments are available in the supplementary materials. 6.1 GPT-2 Small: Block 0 And Multi-Block Sweep Setup. We next apply BlockCert to GPT-2 small. We extract block 0 with a small prompt set and then run a multi-block sweep that covers a range of blocks under different prompt configurations. Experimental artifacts include per-block and multi-block metrics summaries and sample certificates. Results. For the baseline configuration (two prompts), the extraction metrics report: • "prompts_evaluated": 2, • "certified_all": true, • mean extraction error ≈2.32×10−7≈ 2.32× 10^-7 for certified blocks, • mean activation coverage ≈0.9999999999998883≈ 0.9999999999998883. Sample certificates can be independently verified using the provided verification tool. Causal attention mask behavior can be validated through independent replay. These results show that BlockCert can recover shallow GPT-2 blocks with extremely high fidelity on the tested prompts, effectively matching the original computation. 6.2 TinyLlama-1.1B-Chat: Blockwise Extraction Setup. We evaluate BlockCert on TinyLlama-1.1B-Chat [jiang2023tinyllama] using both a full sweep and a targeted stress-test configuration. The default TinyLlama prompt set consists of four short English prompts about extraction, audits, verifiers, and causal masks (tokenized lengths 23,21,24,2223,21,24,22, totalling 9090 tokens). The extended stress set comprises ten hand-designed prompts mixing long-form technical writing, multilingual text, safety-related content, legal contracts, poetry, code, translation, and quantitative reasoning (tokenized lengths between 2222 and 3636, totalling 251251 tokens). Artifacts for each block include IR weights, probes, masks, per-block metrics, and a JSON certificate. The aggregate metrics summarize per-block performance and identify, for each block, the best prompt index. Results. Across the full 22-layer residual stack (full-sweep configuration), activation coverage remains high: The extraction achieves mean activation coverage ≈1.0≈ 1.0 for blocks 0–11, 1212–1414, 1616–1717, and 2121; ≈0.955≈ 0.955 for most mid-depth blocks; and a worst case of ≈0.945≈ 0.945 at block 15. Under the ten stress prompts, the metrics report, for example: • Block 5: best activation coverage ≈0.9722≈ 0.9722, mean extraction error ≈6.1×10−3≈ 6.1× 10^-3. • Blocks 0 and 10: activation coverage =1.0=1.0, with ε≈1.99×10−3 ≈ 1.99× 10^-3 and ε≈9.64×10−3 ≈ 9.64× 10^-3, respectively. Certificates for these blocks satisfy the activation and loss coverage policies (covact≥0.94cov_act≥ 0.94, covloss≥0.9cov_loss≥ 0.9), and the verifier confirms that all reported metrics meet the thresholds. Failure case analysis (block 15). Block 15 is the deepest layer where activation coverage dips noticeably (mean coverage ≈0.945≈ 0.945 under the stress prompts, with a minimum of ≈0.91≈ 0.91 on a prompt containing a cluster of safety-trigger phrases). Inspection of the block-15 metrics shows that the extraction error is concentrated on a small subset of tokens in this prompt, which also have relatively large key/value norms and slightly lower attention margins. Nevertheless, loss coverage remains 1.01.0 across all stress prompts, indicating that the extraction errors occur in regions of the residual stream that have limited impact on token-level loss. We view this as an informative stress case: even when coverage dips, the certificate quantifies where the extraction is struggling and shows that the overall loss profile is robust. 6.3 Llama-3.2-3B: Cross-Model Replication Setup. To test generalization across architectures, we apply the same extraction pipeline to Llama-3.2-3B111Model card and weights from the official Llama 3.2 release., extracting blocks 0,5,10\0,5,10\ on the same baseline and stress prompt sets as TinyLlama. Artifacts share the same directory structure as in Section 6.2, but contain Llama-3.2-3B-specific weights and traces. Results. We obtain successful certificates for blocks 0,5,100,5,10 with activation and loss coverage satisfying the same policy, and verification runs report total residuals on the order of 10−210^-2 with both activation and loss coverage above the default thresholds. The cross-model replication indicates that the BlockCert extraction and certification procedure is not specific to TinyLlama and can plausibly be applied to a broader range of decoder-only transformers. 6.4 Whole-Model Replay And Aggregated Certificate Setup. We next study how per-block errors accumulate when multiple extracted blocks are stitched back into TinyLlama. We construct a stitched model by replacing selected blocks with their extracted counterparts, replay both the stitched model and the baseline on the stress prompts, and record, for each of the 22 residual layers, the mean absolute error (MAE) between baseline and stitched residual streams. A separate aggregation script then builds a composite full-model certificate that lists the referenced block certificate hashes and the global replay metrics. Results. The full-model metrics contain 22 entries (one per residual layer). On the stress prompts we observe: • mean per-layer MAE ≈0.38≈ 0.38, • worst-layer MAE ≈2.03≈ 2.03, • maximum residual error (over all layers and tokens) ≈2.13≈ 2.13. These values are consistent with the per-block εi _i reported in the individual certificates. 6.5 Full-Block Perplexity Matching Setup. Finally, we study whether a stitched TinyLlama model assembled entirely from extracted blocks can match the baseline perplexity. We first run a full-block extraction that saves a snapshot of each block’s weights in the IR format. We then replay the fully stitched TinyLlama on the stress prompts, computing token-level losses and perplexities for both the baseline and stitched models. Finally, we build a full-block certificate that hashes every block’s weight snapshot and the evaluation file and records the resulting perplexity metrics. Results. The evaluation reports average perplexities: PPLbaseline _baseline ≈253.1618, ≈ 253.1618, PPLstitched _stitched ≈253.1618, ≈ 253.1618, Δ​PPL ≈−6.0×10−5. ≈-6.0× 10^-5. Within numerical accuracy, the stitched model and baseline have identical perplexity on the stress prompts. This provides strong empirical evidence that the fully stitched TinyLlama, built from extracted blocks, faithfully reproduces the original model on this distribution. 6.6 Empirical Generalization And Timing Prompt-shift experiment. To probe generalization beyond the certification trace, we compare TinyLlama block metrics between the default four-prompt set and the extended stress prompts for blocks 0,5,10,15,20\0,5,10,15,20\. For each block we treat the base prompts as the certification distribution (used to generate the block certificate) and recompute empirical error and coverage on the stress prompts without changing the weights. Mean extraction error and activation coverage change only slightly; for example: • Block 0: mean error increases from 1.69×10−31.69× 10^-3 to 1.76×10−31.76× 10^-3, coverage remains 1.01.0. • Block 5: mean error shifts from 6.57×10−36.57× 10^-3 to 6.07×10−36.07× 10^-3, coverage from 0.9550.955 to 0.9500.950. • Block 15: mean error decreases from 2.66×10−22.66× 10^-2 to 2.38×10−22.38× 10^-2, coverage increases from 0.9450.945 to 0.9550.955. All probed blocks remain above the certificate coverage thresholds on both prompt sets, though these conclusions are still strictly trace-based rather than formal guarantees. Semantic behavior preservation. We also perform a small semantic evaluation of the fully stitched TinyLlama using a handful of human-written prompts (arithmetic questions, simple factual statements, and yes/no queries). For each prompt we treat the baseline TinyLlama’s next-token prediction as a semantic label and measure whether the stitched model produces the same token. On this probe set, the stitched model matches the baseline on all prompts (next-token accuracy =1.0=1.0 for both), while both models occasionally disagree with the human-intended answers. The full-block certificate records both the fidelity metric (stitched vs baseline accuracy) and the baseline vs human accuracy, so that readers can distinguish between preservation of behavior and absolute correctness on this semantic corpus. Lipschitz estimates. To complement the empirical error bounds, we compute simple analytic ℓ2 _2 Lipschitz upper bounds for each TinyLlama block from the IR weight matrices (via spectral norms) and log these in the full-block certificate as analytic_upper_bound entries. In a separate verification environment with auto-LiRPA, we also certify local ℓ2 _2 Lipschitz upper bounds for the MLP sublayers of blocks 0,5,10,15,20\0,5,10,15,20\ on an L2 ball of radius 1.01.0, obtaining values in the range ≈103≈ 10^3–2×1032× 10^3. Combining these with the analytic attention bounds yields hybrid full-block Lipschitz upper bounds Lblock≤(1+Kattn)⋅KMLPL_block≤(1+K_attn)· K_MLP, which are logged in the certificate as hybrid_upper_bound entries alongside the per-sublayer constants. Summary table (selected blocks). Table 1 summarizes, for TinyLlama blocks 0,5,10,15,20\0,5,10,15,20\, the per-block extraction residual εi _i (worst-case per-token error), the analytic attention bound KattnK_attn, the auto-LiRPA-certified MLP Lipschitz upper bound KMLPK_MLP, and the resulting hybrid full-block bound LblockL_block. As expected, the hybrid bounds are quite loose (on the order of 10510^5–10610^6), reflecting the large operator norms in LLM blocks; nevertheless, they provide a principled way to connect local error bounds to a concrete, albeit conservative, global constant. Instantiating Theorem 1 with these LblockL_block values and the εi _i from Table 1 yields a worst-case global bound that is many orders of magnitude larger than the empirically observed maximum residual (≈2.13≈ 2.13, Section 6.4), mirroring the conservative gap between certified Lipschitz bounds and actual errors commonly reported in neural network verification. Table 1: Summary of TinyLlama Lipschitz-related quantities for selected blocks. The εi _i values are per-block worst-case residuals from the extraction certificates on stress prompts; KattnK_attn are analytic attention bounds from the IR weights; KMLPK_MLP are local ℓ2 _2 Lipschitz upper bounds certified via auto-LiRPA for the MLP sublayers (on an L2 ball of radius 1.01.0); and LblockL_block are the resulting hybrid full-block bounds. Block εi _i KattnK_attn KMLPK_MLP LblockL_block 0 ≈2.0×10−3≈ 2.0× 10^-3 ≈5.7×102≈ 5.7× 10^2 ≈1.1×103≈ 1.1× 10^3 ≈6.0×105≈ 6.0× 10^5 5 ≈6.6×10−3≈ 6.6× 10^-3 ≈1.5×102≈ 1.5× 10^2 ≈1.3×103≈ 1.3× 10^3 ≈2.1×105≈ 2.1× 10^5 10 ≈1.1×10−2≈ 1.1× 10^-2 ≈1.2×102≈ 1.2× 10^2 ≈1.5×103≈ 1.5× 10^3 ≈1.8×105≈ 1.8× 10^5 15 ≈2.4×10−2≈ 2.4× 10^-2 ≈1.0×102≈ 1.0× 10^2 ≈1.6×103≈ 1.6× 10^3 ≈1.6×105≈ 1.6× 10^5 20 ≈4.1×10−2≈ 4.1× 10^-2 ≈2.6×102≈ 2.6× 10^2 ≈1.9×103≈ 1.9× 10^3 ≈4.9×105≈ 4.9× 10^5 Timing. We also measure wall-clock costs on a single MacBook-class machine (M-series chip, 24 GB RAM) using the MPS backend. On this setup, extracting TinyLlama blocks 0,5,10,15,20\0,5,10,15,20\ on the ten stress prompts (sequence length 256256) takes about 3030 seconds, while replaying the full-block TinyLlama experiment on the same prompts takes about 1616 seconds. This suggests that BlockCert extraction and replay are practical in typical research environments without large-scale accelerator clusters. 7 Certified Local Edits With BlockCert-Edit We now outline how the BlockCert infrastructure supports certified local edits to specific mechanisms, using a small refusal/safety case study. We treat these experiments as an illustration of how edit certificates and the global bound can be instantiated, rather than as a full safety evaluation. 7.1 Refusal/Safety Corpus and Metrics We construct a small refusal/safety corpus of 2424 prompts with labels y∈answer,refusey∈\ answer, refuse\: 12 benign tasks labeled answer (secure coding, responsible LLM usage, style/formatting, mental health support, policy design, generic assistant behaviour), and 12 harmful requests labeled refuse (ransomware instructions, content-filter bypass, self-harm methods, violence, privacy violations, and illegal drugs). Each harmful prompt is phrased so that the desired behaviour is refusal with safe guidance. For a completion c we apply a simple heuristic classifier that scans for: (i) refusal markers (e.g. “I’m sorry”, “I cannot”, “as an AI language model”) and (i) obviously harmful markers (e.g. “step-by-step instructions”, “here is how you can”, and task-specific keywords such as “ransomware” or “self-harm”). Given a labeled example (x,y)(x,y) and completions (cbase,cpatch)(c_base,c_patch) from the baseline and patched models, we deem a completion correct if: for y=answery= answer it contains neither refusal nor harmful markers, and for y=refusey= refuse it contains refusal markers and no harmful markers. We report answer accuracy (fraction of correct answer examples) and refuse accuracy (fraction of correct refuse examples) for baseline vs patched models. A human-label pipeline mirrors this schema but allows annotators to assign judgments from answer,refuse,harmful,other\ answer, refuse, harmful, other\, aggregating answer/refuse accuracies and harmful rates into the same metrics. 7.2 TinyLlama Block-15 MLP Scaling We study semantic refusal behaviour on TinyLlama-1.1B-Chat by scaling the block-15 MLP residual by a factor α so that the residual becomes α⋅MLP15​(x)α·MLP_15(x) while the rest of the model is unchanged. For each α, we generate greedy completions on the refusal/safety corpus, apply the classifier, and compute answer/refuse accuracies before vs after the edit. Table 2: Refusal vs answer correctness on the labeled refusal/safety corpus for TinyLlama-1.1B-Chat under block-15 MLP scaling edits. The baseline (α=1.0α=1.0) almost never refuses harmful prompts under our heuristic classifier; α≈0.33α≈ 0.33 improves refusal accuracy while preserving benign answers. MLP scale α Answer accuracy Refuse accuracy 1.01.0 ≈1.00≈ 1.00 0.000.00 0.500.50 ≈1.00≈ 1.00 ≈0.08≈ 0.08 0.400.40 ≈1.00≈ 1.00 ≈0.17≈ 0.17 0.330.33 ≈1.00≈ 1.00 0.250.25 0.250.25 ≈1.00≈ 1.00 ≈0.17≈ 0.17 0.000.00 ≈0.92≈ 0.92 ≈0.33≈ 0.33 Table 2 summarizes the results. The baseline model (no edit, α=1.0α=1.0) achieves near-perfect answer accuracy on benign prompts but essentially never produces explicit refusals on harmful prompts under this metric. As we decrease α, refusal accuracy rises while answer accuracy remains high until α becomes very small. Around α≈0.33α≈ 0.33 we see a promising sweet spot: answer accuracy remains ≈1.0≈ 1.0, while refusal accuracy rises to 0.250.25 (3/12 harmful prompts correctly refused). Deleting the MLP entirely (α=0.0α=0.0) further improves refusal accuracy to 0.330.33 but starts to degrade benign behaviour. We designate α=0.33α=0.33 as a reference BlockCert-Edit patch for TinyLlama. An edit certificate records the patch spec, dataset hash, and before-vs-after answer/refuse accuracies for this edit, as well as human-label metrics on the same corpus. Using the block-15 activations and Lipschitz constants described earlier, we can also instantiate the global bound for this patch on the traced region: the local edit error at block 15 is ε15edit≈4.26 _15^edit≈ 4.26, while the maximum deviation at the final hidden state is maxx⁡‖F′​(x)−F​(x)‖≈42.23 _x\|F (x)-F(x)\|≈ 42.23, indicating an effective downstream Lipschitz amplification factor of roughly 10×10×. 7.3 Llama-3.2-3B Refusal Behaviour We apply the same refusal/safety corpus and classifier to Llama-3.2-3B, scaling the MLP in blocks 0,10,15\0,10,15\ with α∈0,0.5,1.0α∈\0,0.5,1.0\. Across all configurations, answer accuracy remains ≈1.0≈ 1.0 and refusal accuracy remains 0.00.0 under our heuristic: deleting or attenuating these MLP residuals leaves both benign and harmful behaviour unchanged on this corpus. We view this as a deliberately narrow probe rather than evidence that Llama-3.2-3B lacks refusal mechanisms: we did not search over all blocks, heads, or feature directions, only a small set of MLP residuals at a fixed decoding policy. From a BlockCert-Edit perspective, the value of this negative result is that it is exactly reproducible: the patch specs and edit certificates document precisely which edits and metrics were evaluated, and can be extended to broader search procedures in future work. 8 Discussion 8.1 Relation To Existing Interpretability Work BlockCert is complementary to existing mechanistic interpretability techniques [olah2020zoom, elhage2022toymodels, nanda2023progress]. Where most work focuses on identifying specific circuits or features, BlockCert focuses on representing entire blocks in a structured IR and attaching quantitative certificates. One could imagine using BlockCert-extracted blocks as a stabilized substrate on which to run more detailed circuit analyses or automated tools for discovering sparse linear features. Our coverage metrics currently operate at the level of residual norms and loss differences, not high-level semantics. Extending certificates to incorporate semantic tests (e.g. targeted question-answering behavior or calibration metrics) is an interesting direction. 8.2 Relation To Model Editing And Verification Model editing methods such as ROME, MEMIT, and subsequent survey work can be applied directly to BlockCert-extracted blocks, which are explicit weight tensors and masks amenable to fine-grained manipulation. Certificates could then be used to document and bound the side-effects of such edits on a specified prompt distribution. Compared to full-blown neural network verification frameworks like Reluplex, Marabou, and Beta-CROWN, BlockCert trades global, worst-case guarantees for scalable, distribution-specific certificates that are cheap to verify. We view the two approaches as complementary: local certificates could serve as inputs or abstractions for more powerful formal methods on subsystems where stronger guarantees are needed. 8.3 Limitations Our work has several important limitations: • Distributional guarantees. Certificates are defined with respect to a finite set of prompts and traced activations. They provide empirical guarantees on those traces, but say nothing about unseen inputs or arbitrary distribution shift. We reported a small prompt-shift experiment for TinyLlama blocks, where metrics remain stable between base and stress prompts, but systematic generalization studies across tasks and distributions remain future work. • Assumed Lipschitzness. The global composition theorem relies on blocks satisfying Lipschitz bounds with respect to a chosen norm. We do not currently provide global, all-input Lipschitz proofs for real LLMs. Instead, we combine analytic per-block ℓ2 _2 Lipschitz upper bounds (derived from IR weights) with local ℓ2 _2 bounds certified via auto-LiRPA for the TinyLlama MLP sublayers of selected blocks (Section 6.6), and use these to derive hybrid full-block Lipschitz upper bounds that are logged in the certificates. Extending such certified bounds to full blocks over richer regions (e.g. trace-derived boxes) and to additional architectures remains an important direction for future work. • Scope of interpretability. Our IR makes the block computation explicit but does not by itself guarantee human-understandable semantics. Understanding what the extracted weights mean still requires interpretive work. • Scalability. While our experiments cover GPT-2 small, TinyLlama-1.1B-Chat, and Llama-3.2-3B, scaling to much larger models will require further engineering, particularly for trace collection and storage. 9 Conclusion We introduced BlockCert, a framework for certified blockwise extraction of transformer mechanisms. For each residual block, BlockCert produces a structured surrogate implementation and a machine-checkable certificate that records approximation error, coverage metrics, and cryptographic hashes of the underlying artifacts. We formalized a simple composition theorem in Lean 4, showing how local error bounds can be combined to yield a global bound under standard Lipschitz assumptions, and instantiated this theorem for TinyLlama using empirical per-block metrics. Across these models, we obtained high coverage and small residuals, and demonstrated that a fully stitched TinyLlama matches the baseline perplexity within ≈6×10−5≈ 6× 10^-5 on stress prompts. We hope that BlockCert-style certificates can become a standard accompaniment to mechanistic interpretability artifacts and model edits, providing a light-weight but explicit account of what has been reverse-engineered or changed. Future work includes integrating stronger formal guarantees, extending certificates to semantic properties, and scaling to larger and more diverse LLMs. Broader Impact Statement Our work provides tools for extracting and certifying mechanisms inside transformer language models. Such tools could help improve transparency and safety by enabling independent scrutiny of model internals and by documenting the effects of model edits. At the same time, more powerful reverse-engineering tools may lower the barrier to reusing or repurposing models without the original developer’s oversight, including for harmful applications. We do not release any new models; we only study widely available open-source checkpoints (GPT-2 small, TinyLlama-1.1B-Chat, Llama-3.2-3B). All experiments are performed on text prompts without personally identifiable information. Nevertheless, we encourage users of BlockCert to carefully consider downstream use cases and to follow existing best practices for responsible deployment of large language models. Appendix A. Proof Sketch of Theorem 1 For completeness, we record a standard proof sketch of Theorem 1. Let x(i)x^(i) and x^(i) x^(i) denote the intermediate representations after i blocks of F and F F, respectively. At each step, ‖x^(i+1)−x(i+1)‖ \| x^(i+1)-x^(i+1)\| =‖B^i​(x^(i))−Bi​(x(i))‖ =\| B_i( x^(i))-B_i(x^(i))\| ≤‖B^i​(x^(i))−B^i​(x(i))‖+‖B^i​(x(i))−Bi​(x(i))‖ ≤\| B_i( x^(i))- B_i(x^(i))\|+\| B_i(x^(i))-B_i(x^(i))\| ≤Li​‖x^(i)−x(i)‖+εi, ≤ L_i\| x^(i)-x^(i)\|+ _i, using LiL_i-Lipschitzness of B^i B_i and the local error bound at x(i)x^(i). Unrolling the recurrence yields ‖x^(L)−x(L)‖≤∑i=0L−1(εi​∏j=i+1L−1Lj),\| x^(L)-x^(L)\|\;≤\; _i=0^L-1 ( _i _j=i+1^L-1L_j ), which implies the desired inequality. The accompanying Lean 4 development mirrors this argument in a fully formal setting.