Verified by Construction: Machine-Checked Proofs for Hand-Written Transformer Circuits and Their Composition

When transformer weights are written by hand or compiled in rather than trained, an auditor needs to know what they compute on every input. Sampled evaluation cannot tell: a hand-written multiplication transformer with 100% sampled accuracy answers 89984*48898= wrongly. We give machine-checked Lean 4 proofs that follow the mechanism the weights were written for. First, we prove seven hand-written weight-space programs correct on every input of their task, with up to about 1.3M parameters, up to 26^9 ≈ 5.4×10^12 prompts, and real LayerNorm. Second, for circuits appended to the residual stream of a trained host, we prove a grafting theorem for any host in our formalised pre-LayerNorm architecture with positive width and LayerNorm ε, on prompts within its context length. For circuits whose features are zero-sum with constant energy, LayerNorm compensation makes an idle circuit with positive LayerNorm ε leave the host's logits exactly unchanged. On prompts whose host variance is at most a stated σ², a circuit with zero-sum writes moves the logits at a position by at most an explicit bound if, for every variance profile up to σ², its readout there vanishes for every token and its final energy stays in a band [E, E+Δ] starting at its features' energy E; and its token wins if, for every such profile, its energy is at least that of its features and its margin beats the host gap of every other token. The circuit's obligations use the host's weights only through its unembedding, output bias and final LayerNorm, and the bound also uses its variance, so the proofs never load host weights. Third, we instantiate the theorem as a multi-token refusal rule, a key gate with a counting bound on triggering by uniformly random prompts, and a watermark with false-positive rate at most e^(−m/8) for a uniformly random secret code independent of the reading. Grafted into OPT-6.7B, the proved refusal circuit fires on 2480 of 2480 trigger positions in float32 and float16, and on the evaluation windows its float64 off-trigger deviation stays below 1.1% of each token's proved bound. The theorems cover the exact real-valued weights. For the circuits we instantiate we prove, under their hypotheses, that every circuit LayerNorm radicand is positive, so their guarantees hold for ordinary real-arithmetic execution with heads of positive dimension; floating-point storage and execution are measured, not proved. The artifact zip contains the Lean 4 development, the grafting experiments and the evidence files. The Lean weight modules of the seven benchmark snapshots are derived from a third-party repository without a license and are not redistributed; the artifact's regenerate_weights.sh rebuilds them from the public repository at a pinned commit and checks them against recorded checksums.