SMT Verification of Magic State Distillation Scales Linearly with Circuit Size

Nathan Didier & Victoria | September 24, 2026
Computation: Z3 SMT solver on Pauli-frame stabilizer constraints, tested to 1.6M variables
Source code: initial, round 4, extended, corrected stabilizers

1. The Question

Hugh's knowledge graph identified a gap in quantum error correction: if symbolic execution for stabilizer-based QECCs is extended to non-Clifford magic state distillation circuits, would integrating SMT solvers with tensor network contraction resolve the exponential blowup in entanglement tracking? The gap had 24 sources at 0.528 confidence, the densest unexplored region of the graph.

Magic state distillation is the bottleneck for universal fault-tolerant quantum computing. The 15-to-1 protocol takes 15 noisy T-states, applies a Clifford circuit based on the [[15,1,3]] quantum Reed-Muller code, measures 14 stabilizers, and outputs one T-state with cubically reduced error. Concatenating this protocol (feeding 15 outputs back in) amplifies the error suppression but multiplies the circuit size by 15 at each level. The question is whether formal verification of the concatenated circuit blows up exponentially or remains tractable.

2. The Approach

We bypass entanglement tracking entirely. Instead of tracking the full quantum state through the circuit (which is exponential for non-Clifford operations), we track how Pauli errors propagate through the stabilizer structure.

Each qubit's error state is represented as two Z3 boolean variables: X-error (bit flip) and Z-error (phase flip). Y-errors are the conjunction X AND Z. Clifford gates permute these errors deterministically. The stabilizer measurements impose parity constraints on the error variables. An undetectable error is one that satisfies all syndrome constraints while being nontrivial.

The SMT solver's job: determine satisfiability of the composed constraint system across concatenated distillation blocks. If the constraint system grows polynomially in the number of blocks, formal verification is tractable. If it grows exponentially, the blowup is real.

3. The [[15,1,3]] Quantum Reed-Muller Code

The [[15,1,3]] code is a CSS code with an asymmetric stabilizer structure. The 15 qubits are indexed by nonzero elements of GF(2)^4. The code is constructed from punctured Reed-Muller codes:

X stabilizers (4 generators): From the punctured first-order Reed-Muller code C_X = RM*(1,4), a [15, 4, 8] code. Each generator corresponds to a coordinate function r_i on GF(2)^4, with weight 8.

Z stabilizers (10 generators): From C_Z = RM*(1,4)^perp, the dual of the X stabilizer code, a [15, 10] code. The generators include 6 weight-4 stabilizers corresponding to the quadratic monomials r_i * r_j (i < j), plus 4 additional generators that are linear combinations in C_Z not contained in C_X. Note: C_Z is not RM(2,4). The punctured second-order Reed-Muller code RM*(2,4) = [15, 11, 3] is the Hamming code Ham(4), which is the space C_X^perp of all undetectable Z errors (stabilizers plus logical operators), not the stabilizer code itself.

This asymmetry is what gives the code its transversal T gate. The consequence for error detection: the 10 Z-stabilizers detect all X errors up to weight 2 (X distance = 7, from C_Z^perp = RM*(1,4) having minimum weight 7 after including the all-ones vector). The 4 X-stabilizers detect Z errors up to weight 2, but weight-3 Z errors can be undetectable: they are the minimum-weight codewords of C_X^perp = Ham(4) = [15, 11, 3], which has exactly 35 codewords of weight 3. These are the logical Z operators of the code.

Zero undetectable errors at weight 1 and 2 confirms the code distance d = 3. The 35 undetectable errors at weight 3 are all Z-type: they are the minimum-weight logical Z operators of the code. Zero X-only and zero mixed errors at weight 3 confirms the asymmetric structure. The 35 weight-3 logical Z operators directly reproduce the known distillation guarantee p_out ~ 35 p^3 [2].

4. Concatenation Scaling

Each concatenation round feeds 15 distillation outputs into one more distillation block. Round n has 15^(n-1) + ... + 15 + 1 blocks.

The cost per variable is constant at 6-11 microseconds from round 2 onward. The total solve time scales linearly with the number of variables. Z3 solved 1.6 million boolean constraints in 18 seconds. These results are reproduced identically with the corrected asymmetric stabilizers.

5. Circuit-Level Noise

The input-error model only tests errors on the T-states fed into the circuit. Real distillation circuits have gate errors throughout the Clifford operations. We extended the model to inject symbolic Pauli errors after each of the 28 CNOT gates in the distillation circuit. Each gate error is a pair of boolean variables on the control and target qubits. The total error on each qubit is the XOR of its input error and all gate errors it accumulated.

Circuit-level noise adds a constant factor of approximately 8x compared to input-only errors (62-67 us/var vs 6-11 us/var), but the scaling remains linear. The additional gate error variables increase the problem size per block but do not change the complexity class. Z3's constraint propagation handles the composed error structure without blowup.

6. Why It Works

The key insight is that the Pauli frame representation decomposes the verification problem into independent blocks connected by single-bit logical error channels. Each distillation block's stabilizer constraints form a local system of 14 parity checks on 30 boolean variables. The blocks interact only through a single boolean per block: did a logical error occur? This gives the full constraint system a block-diagonal structure with rank-1 connections.

Z3 exploits this structure through unit propagation and boolean constraint propagation (BCP). Each block's constraints are resolved locally, and the inter-block connections propagate in one pass. The solver never needs to backtrack across block boundaries because the local structure is fully determined by BCP.

This is fundamentally different from tracking the full quantum state, which would require 2^n complex amplitudes and produce constraints that are globally coupled through entanglement. The Pauli frame avoids entanglement tracking entirely by representing errors as classical bit strings that compose under XOR. The non-Clifford character of the T-gate is irrelevant to the error propagation: what matters is how errors interact with the stabilizer measurements, and that interaction is purely classical.

7. What This Resolves

Hugh's gap asked whether SMT solvers combined with tensor networks could resolve the exponential blowup in entanglement tracking for magic state distillation verification. The answer is stronger than expected:

You don't need tensor networks at all. The Pauli frame representation makes the problem polynomial without any additional compression. SMT solvers verify magic state distillation at linear cost per variable, constant cost per block, across five concatenation levels totaling 1.6 million variables and 54,241 distillation blocks.

The exponential blowup in "entanglement tracking" is real but irrelevant: you don't need to track entanglement to verify distillation. You need to track how errors propagate through the stabilizer structure, which is a classical boolean satisfiability problem with block-diagonal constraint structure.

8. Implications

For formal verification of quantum circuits: The Pauli frame + SMT approach can formally verify the error properties of arbitrarily deep concatenated distillation protocols. This provides machine-checkable guarantees for the error suppression properties that fault-tolerant quantum computing relies on.

For threshold estimates: The ability to verify distillation at scale means threshold calculations for concatenated protocols can be checked by SAT solvers rather than trusted by analogy. Non-standard error models (correlated noise, leakage, non-Markovian effects) can be incorporated as additional boolean constraints without changing the scaling.

For the surface code vs qLDPC debate: The same Pauli frame + SMT approach applies to any stabilizer code. Verifying qLDPC distillation protocols at scale is equally tractable, removing one barrier to formal comparison of code families.

9. Limitations

The Pauli frame model tracks error propagation, not the full quantum state. It cannot verify properties that depend on coherent superposition or entanglement structure (e.g., the fidelity of the output magic state relative to the ideal T-state). It verifies that the stabilizer structure detects errors correctly and that the distillation protocol's error suppression guarantee holds under the specified noise model.

The model assumes independent Pauli errors (depolarizing channel). Correlated errors, non-Pauli noise, and coherent errors require extensions to the boolean framework. Correlated Pauli errors can be modeled by adding joint constraints between qubits; non-Pauli noise requires a different representation entirely.

The CNOT schedule used in the circuit-level noise test is representative, not the exact encoding circuit for the [[15,1,3]] code. The scaling result (linear cost per variable) is robust to the specific circuit because the block-diagonal structure is a property of the stabilizer code, not the encoding circuit.

Status

Output type: Computation. Outcome: RESULT. SMT verification of magic state distillation scales linearly with circuit size across five concatenation levels (1.6M variables, 18s solve time, corrected asymmetric stabilizers). The Pauli frame representation eliminates the need for entanglement tracking or tensor network contraction. The exponential blowup identified in Hugh's gap does not occur under this approach. Circuit-level noise adds a constant factor (8x) without changing the scaling class. The corrected [[15,1,3]] code properties (35 Z-only undetectable weight-3 errors, zero X-only, zero mixed) and the distillation error coefficient (35 p^3) are reproduced exactly.

References

[1] Google Quantum AI. "Quantum error correction below the surface code threshold." Nature 638, 920-926 (2025). link

[2] Bravyi, S., Kitaev, A. "Universal quantum computation with ideal Clifford gates and noisy ancillas." Physical Review A 71, 022316 (2005).

[3] Gottesman, D. "Fault-tolerant quantum computation with constant overhead." Quantum Info. Comput. 14 (2014). link

[4] Bravyi, S. et al. "High-threshold and low-overhead fault-tolerant quantum memory." Nature 627, 778-782 (2024). link

[5] Xu, Q. et al. "Constant-overhead fault-tolerant quantum computation with reconfigurable atom arrays." Nature Physics 20, 1084-1090 (2024).

[6] Xie, H. et al. "Noise-Agnostic Unbiased Quantum Error Mitigation for Logical Qubits." PRL 136, 010603 (2026).

[7] de Moura, L., Bjorner, N. "Z3: An Efficient SMT Solver." TACAS 2008.

[8] Gottesman, D. "The Heisenberg representation of quantum computers." Group 22 (1998). link

[9] Zhang, G. et al. "Constant-Overhead Magic State Injection into qLDPC Codes." arXiv:2505.06981 (2025). link

Nathan Didier & Victoria | Phartmaceutical Research Division | September 24, 2026