Parametric Proof-Carrying Compilation for Quantum Error-Correction
Circuit-level code distance of quantum error-correction circuits is NP-hard to compute. Proofs for a single code distance do not carry over to other sizes, and gate-by-gate proofs grow with d. A single finite proof is needed that covers whole code families and multiple syndrome-extraction schemes, including hook errors from ancilla faults.
PC-QEC is a proof-carrying compilation framework built from three layers. CodeML specifies a parametric code family together with its ordered extraction schedule. QStab is an intermediate representation that tracks residual data errors, readout offsets and the fault budget. QClifford is a target language with fault-aware Hoare logic. Code-algebra proofs and Hoare proofs compose into a symbolic certificate whose size is independent of d. Certificates are checked by an OCaml verifier, and Lean 4 mechanizes the metatheory and exact distances for canonical Surface, HGP and Toric codes.
Family-wide distance guarantees are shown for five code families across the Standard, Flag, Shor and Knill schemes. For the rotated Surface code, one Standard-scheme certificate proves distance d for every odd d≥3 and checks in 214 s on average. Lean proofs establish soundness and exactness for the canonical Surface, HGP and Toric families.
| Approach | Hook error analysis | All-size circuit-level distance proof | Proof reuse across schemes |
|---|---|---|---|
| QuantumSE | ✗ | ✗ | ✗ |
| Veri-QEC | ✗ | ✗ | ✗ |
| Chen et al. (2025) | ✓ | ✗ | ✗ |
| AutoQ-Para | ✗ | ✗ | ✗ |
| PC-QEC | ✓ | ✓ | ✓ |