A compact proof for quantum error correction across code sizes

The challenge: faults in the protection system

Quantum error-correcting codes use repeated measurements to detect disturbances without directly measuring the encoded information. A code’s distance describes how many errors are needed to produce an undetected logical error in the idealized code. In an actual syndrome-extraction circuit, however, faults can occur during gates and measurements. A flipped readout can hide evidence of an error, and an ancilla fault can spread through a sequence of gates to affect several data qubits.

The paper studies circuit-level distance: the minimum number of specified fault injections that can produce a logical data error without setting off the circuit’s detectors. This is a guarantee about a defined circuit and fault model—not a prediction of how often a particular quantum processor will fail.

A proof that travels with the circuit

John Zhuoyang Ye and Jens Palsberg introduce PC-QEC, a framework for compiling quantum error-correction programs together with proofs. Its central goal is to handle a whole code family, whose circuits grow with code distance, using a finite symbolic proof rather than a separate, expanding argument for every size.

The framework connects two kinds of reasoning. First, code-algebra proofs identify which data-error patterns are genuinely logical errors. Second, fault-aware program proofs track how circuit operations and injected faults change those patterns. For the rotated Surface code, the argument uses parity checks called cuts: a logical error must cross many of them, while each allowed fault—including a propagated hook error—can cross only a limited number. Combining these facts rules out a logical error below a specified fault count.

The compiler’s proof obligations include the order in which stabilizer measurements couple to data qubits. That detail matters: changing the order can change how an ancilla fault spreads, even when the measured stabilizer operator is unchanged. The authors translate proofs across four extraction schemes—Standard, Flag, Shor and Knill—provided each implementation meets its declared fault and readout contract.

What the authors report

The paper reports family-wide guarantees for five code families across all four schemes. For the rotated Surface code, one Standard Scheme certificate proves a circuit-distance lower bound of d for every odd code distance d ≥ 3. The paper also gives a matching silent failure at d faults for that ordered schedule, making the distance equal to d under its definition. Checking the family certificate took an average of 214 seconds in the reported setup.

The other reported results vary by family and scheme. For example, the triangular color-code guarantee is a lower bound of at least the ceiling of d/3, rather than d. The paper also reports that extraction order can change certified distance in finite examples. These are formal results under the paper’s chosen definitions and contracts; they are not measurements of device error rates.

The authors use an OCaml verifier to check certificates. Lean 4 mechanizes metatheory and exact circuit-level distances for canonical Surface, hypergraph-product and Toric code programs. The authors state that a family certificate has size independent of code distance, while the expanded circuit and a gate-by-gate proof still grow with distance. In other words, the compact object is the symbolic argument, not the hardware circuit.

Scope and uncertainty

A certificate is only as meaningful as its assumptions. The fault model counts single-wire Pauli injections at operation operands; two faults on the inputs of a CNOT count as two. The readout contract also matters. Some Shor- and Knill-scheme family results require particular relative readout flips to be absent. These guarantees should not be read as covering every possible hardware noise process or every decoder.

Circuit distance is also not a logical error rate. The work does not, by itself, show that a physical device achieves a particular performance, nor does it establish full fault-tolerant computation. Rather, it offers a way to check a distance claim for a specified compiled circuit and family under explicit assumptions. The reported checking times depend on the implementation and test setup; they do not measure the cost of running the quantum circuits.

The source is an arXiv preprint, and the supplied evidence does not establish peer-review status. Its artifact is described as containing source code, certificates, measurements and reproduction scripts, but readers should consult the paper and artifact to assess the details independently. The key contribution is a method for carrying a formal argument through compilation—so that the circuit’s protection claim can be checked alongside the circuit itself.