Efficient Formal Verification of Quantum Error Correcting Programs
arXiv:2504.07732 · doi:10.1145/3729293
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.
41 pages, 10 figures, 4 tables; v2: Extended version of the paper in PLDI 2025; Evaluated artifact at https://doi.org/10.5281/zenodo.15267327 v3: revise typos and inconsistencies
References in corpus (34)
- Quantum Computing in the NISQ era and beyond
- Improved Simulation of Stabilizer Circuits
- Suppressing quantum errors by scaling a surface code logical qubit
- Logical quantum processor based on reconfigurable atom arrays
- Quantum error correction below the surface code threshold
- High-threshold and low-overhead fault-tolerant quantum memory
- Experimental Quantum Computations on a Topologically Encoded Qubit
- Stim: a fast stabilizer circuit simulator
- Magic state distillation with low overhead
- Realization of an Error-Correcting Surface Code with Superconducting Qubits
- Quantum Low-Density Parity-Check Codes
- Interacting Quantum Observables: Categorical Algebra and Diagrammatics
- Quantum LDPC codes with positive rate and minimum distance proportional to n^{1/2}
- The XZZX Surface Code
- Fast simulation of stabilizer circuits using a graph state representation
- Unfolding the color code
- Towards Large-scale Functional Verification of Universal Quantum Circuits
- PyZX: Large Scale Automated Diagrammatic Reasoning
- A Verified Optimizer for Quantum Circuits
- A unified framework for magic state distillation and multi-qubit gate-synthesis with reduced resource cost
- QWIRE Practice: Formal Verification of Quantum Circuits in Coq
- A Deductive Verification Framework for Circuit-building Quantum Programs
- Quantum Relational Hoare Logic
- Improved quantum hypergraph-product LDPC codes
- ReQWIRE: Reasoning about Reversible Quantum Circuits
- Formal Verification of Quantum Programs: Theory, Tools and Challenges
- symQV: Automated Symbolic Verification of Quantum Programs
- Relational Proofs for Quantum Programs
- Certified Quantum Computation in Isabelle/HOL
- Symbolic Execution for Quantum Error Correction Programs
- Efficient Formal Verification of Quantum Error Correcting Programs
- Leveraging Automorphisms of Quantum Codes for Fault-Tolerant Quantum Computation
- Quantum Relational Hoare Logic with Expectations
- Gottesman Types for Quantum Programs