# Techniques: Verifying Fault-Tolerance of Quantum Error Correction Codes

## What the paper contributes (one paragraph)
The paper formalises the fault-tolerance of quantum error correction code (QECC) implementations in the language of classical-quantum programs and builds an automated tool that proves, or disproves, whether a given gadget is fault-tolerant up to a chosen number of faults. It extends program semantics to model faulty executions, then supplies two discretisation theorems showing that continuous input states and continuous error channels can be reduced to discrete logical basis states and Pauli errors. This lets a quantum symbolic execution engine, built on the stabiliser formalism and an SMT solver, reason about every fault combination. New transition rules exploit memory-less and conservative repeat-until-success loops, and a two-party framework absorbs non-Clifford components so magic state distillation can be checked. The method is sound and complete under stated loop assumptions, and on failure it returns the error propagation path. It is demonstrated on preparation, gate, measurement, and error correction gadgets across colour, surface, toric, and Reed-Muller codes.

## Techniques offered
- **Fault-tolerance verification of QECC gadgets** - an automatic tool that takes a QECC gadget implementation and either proves it fault-tolerant up to t faults or returns a fault pattern that violates the criterion.
  - guarantee: sound and complete static proof for memory-less loops, sound for conservative loops; on failure returns a witnessing fault instantiation.
  - quote: "If the repeat-until-success statements in \(S\) are memory-less, then our fault-tolerance verification is both sound and complete."
- **Quantum symbolic execution with faults** - a symbolic execution engine over the stabiliser formalism that injects symbolic Pauli faults and discharges the fault-tolerance condition to an SMT solver.
  - guarantee: exhaustive over all fault combinations within the bound; returns a fault instantiation witnessing any failure.
  - quote: "Having discretized the inputs and errors, we can now establish a symbolic execution framework based on the quantum stabilizer formalism to reason about fault-tolerance of QECC implementations."
- **Error and input discretisation theorems** - theorems reducing continuous code-space inputs to discrete logical basis states and arbitrary fault channels to Pauli channels, making the verification tractable.
  - guarantee: equivalence reduction (continuous case holds if and only if the finite discretised case holds).
  - quote: "In this section, we introduce two new discretization theorems that allow us to analyze and verify quantum fault-tolerance on \cqprog{} in a systematic way."
- **Two-party framework for non-Clifford magic state distillation** - a reformulation that absorbs non-Clifford components into one party's input so the remaining Clifford execution can be verified, extending the method to magic state distillation.
  - guarantee: sound verification of magic state preparation under memory-less or conservative loops.
  - quote: "To better illustrate the idea of fault-tolerant magic state distillation, we reformulate it in a \textbf{two-party framework} in \cref{fig:magicstate}."

## Where it could apply
- Target primitive(s): state preparation, logical gates (CNOT, transversal Clifford), logical measurement, error correction gadgets, and magic state distillation.
- Target application group(s): error_correction, platforms_tooling.
- Code family / hardware assumptions: stabiliser CSS codes including colour code, rotated surface code, toric code, and quantum Reed-Muller code; gadgets must use stabiliser (Clifford) operations, with non-Clifford parts handled via the two-party framework.

## Caveats
The tool verifies gadget implementations that are expressed as classical-quantum programs with stabiliser operations; non-Clifford components are only handled through the two-party distillation reformulation. Completeness holds only for memory-less repeat-until-success loops (conservative loops give soundness only). Scalability is limited by the SMT solver: large instances such as the [[49,1,7]] rotated surface code CNOT gadget time out, and verifying some gadgets takes tens of hours.