Efficient Formal Verification of Quantum Error Correcting Programs

TL;DR

The paper tackles the challenge of efficiently verifying quantum error correcting programs, including non-Clifford and propagation errors, by developing a hybrid classical-quantum assertion logic and a backward-reasoning program logic. It introduces a Coq-formalized verifier and an SMT-based automatic verifier, Veri-QEC, and demonstrates scalability with 14 stabilizer codes, including large surface codes, under various fault-tolerant scenarios. The key innovations are the Pauli-expression based assertion language, the projection-based quantum logic foundation, and a practical VC handling strategy that reduces to SMT problems or uses heuristics for non-commuting cases. Taken together, the framework enables rigorous, scalable verification of QEC protocols and fault-tolerant primitives, offering a path toward reliable, hardware-wide quantum error correction in near- to far-term devices.

Abstract

Quantum error correction (QEC) is fundamental for suppressing noise in quantum hardware and enabling fault-tolerant quantum computation. In this paper, we propose an efficient verification framework for QEC programs. We define an assertion logic and a program logic specifically crafted for QEC programs and establish a sound proof system. We then develop an efficient method for handling verification conditions (VCs) of QEC programs: for Pauli errors, the VCs are reduced to classical assertions that can be solved by SMT solvers, and for non-Pauli errors, we provide a heuristic algorithm. We formalize the proposed program logic in Coq proof assistant, making it a verified QEC verifier. Additionally, we implement an automated QEC verifier, Veri-QEC, for verifying various fault-tolerant scenarios. We demonstrate the efficiency and broad functionality of the framework by performing different verification tasks across various scenarios. Finally, we present a benchmark of 14 verified stabilizer codes.

Figures (11)

• Figure 1: Overall structure of our verification framework for QEC programs.
• Figure 2: Operational semantics for QEC programs.
• Figure 3: Inference rules for reasoning about QEC programs. For simplicity, we write $-P$ for $(-1)^\mathbf{true}P\in PExp$, write $P_1-P_2$ for $P_1+(-1)^\mathbf{true}P_2\in PExp$, where $P, P_1, P_2\in PExp$, and write $\frac{1}{\sqrt{2}}$ for $\frac{\sqrt{2}}{2^1}\in SExp$.
• Figure 4: Time consumed when verifying surface code in sequential/parallel.
• Figure 5: Scheme of a rotated surface code with $d = 5$. Each coloured tile associated with the measure qubit in the center is a stabilizer (Flesh: $Z$ check, Indigo: $X$ check).

Theorems & Definitions (20)

• theorem 1: Closedness of Pauli expression under Clifford + $T$, c.f. sundaram2022hoare
• definition 1: Syntax of assertion language
• definition 2: Satisfaction relation
• definition 3: Entailment
• definition 4: Correctness formula
• theorem 2: Soundness
• definition 5: Correctness formula for QEC programs
• proposition 1
• proposition 2: Expressivity of $SExp$ and $PExp$
• theorem 3: Theorem 3.1