Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:2504.07732 · Proceedings of the ACM on Programming Languages

Efficient Formal Verification of Quantum Error Correcting Programs

Qifan Huang, Li Zhou, Wang Sheng Fang, Mengyu Zhao, Mingsheng Ying

Published Jun 10, 2025• 15 citations
arXivHTMLPDF

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.

DOI
10.1145/3729293

Related papers

QECV: Quantum Error Correction Verification

Anbang Wu, Gushu Li, Hezi Zhang +3 more

Quantum Error Correction (QEC) is essential for fault-tolerant quantum copmutation, and its implementation is a very sophisticated process involving both quantum and classical hardware. Formulating and verifying the decomposition of logical operations into physical ones is a challenge in itself. In this paper, we propose QECV, a verification framework that can efficiently verify the formal correctness of stabilizer codes, arguably the most important class of QEC codes. QECV first comes with a concise language, QECV-Lang, where stabilizers are treated as a first-class object, to represent QEC programs. Stabilizers are also used as predicates in our new assertion language, QECV-Assn, as logical and arithmetic operations of stabilizers can be naturally defined. We derive a sound quantum Hoare logic proof system with a set of inference rules for QECV to efficiently reason about the correctness of QEC programs. We demonstrate the effectiveness of QECV with both theoretical complexity analysis and in-depth case studies of two well-known stabilizer QEC codes, the repetition code and the surface code.

arXiv:2111.13728•Nov 26, 2021•0 citations

End-to-End Formalization of Quantum Error Correction

Mattias Ehatamm, Yi Lee, Xiaodi Wu +1 more

Quantum error-correcting codes (QECCs) sit between noisy quantum hardware and reliable computation, so the code parameters used in practice must be trustworthy. The single number that summarizes a code's strength is its distance, yet certifying a distance lower bound is NP-hard in general, placing it beyond the reach of pen-and-paper proofs as well as direct proof-assistant scripting. As a result, distance values in the literature come either from non-scaling hand proofs, or from unverified solvers that leave a trust gap exactly where the code is supposed to provide a guarantee. We present Lean-QEC, the first Lean 4 formalization of stabilizer-code theory that delivers end-to-end, machine-checked distance certificates at industrial code sizes. Lean-QEC formalizes the linear algebra of qubit states, the Pauli group, stabilizer codes, the binary symplectic representation, classical coding theory, and the CSS and Bivariate Bicycle families. To break the combinatorial barrier, Lean-QEC translates the distance condition into a Boolean satisfiability formula through a verified reduction. The pipeline scales through a BitVec-flattened encoding that replaces Lean's Matrix representation, and an error-location encoding that reduces the variable count from $n$ to $k\lceil \log_2 n\rceil$. With these, we obtain automatically-generated Lean-checked distance proofs for a large range of industrially viable qLDPC codes within the Bivariate Bicycle and Generalized Bicycle families, including [[90, 8, 10]] and [[70, 6, 9]] BB codes, with the formulation scaling up to 144 qubits when performed outside the Lean kernel. The resulting library is reusable and is designed to plug into broader Lean-based efforts toward end-to-end verification of fault-tolerant quantum computation.

quant-pharXiv:2605.16523•May 19, 2026•0 citations

Formal Specification of Quantum Error Correction Codes

Jincheng Zhang

This paper presents a novel approach to quantum error correction (QEC) by formally specifying QEC codes using mathematical logic. The core idea is to translate the mathematical definitions and properties of QEC codes into logical formulas, enabling automated verification and facilitating the design of new, more efficient codes. This approach moves beyond intuitive understanding and provides a rigorous, verifiable framework. The paper outlines the methodology, demonstrates its application with a simplified example, and highlights the potential benefits of this formal specification technique for QEC research and development. The focus is on building a foundation for automated code design and analysis, crucial for the practical implementation of large-scale quantum computers. This work contributes to a more robust and trustworthy approach to QEC, addressing the challenges of complexity and verification inherent in traditional design methods.

•Aug 29, 2026•0 citations

Analyzing Decoders for Quantum Error Correction

Abtin Molavi, Feras Saad, Aws Albarghouthi

Quantum error correction (QEC) enables reliable computation on noisy hardware by encoding logical information across many physical qubits and periodically measuring parities to detect errors. A decoder is the classical algorithm that uses these measurements to infer which error most likely occurred, so that the system can correct it. The decoder's accuracy-how rarely it makes the wrong guess-directly determines the scale of quantum computation that can be reliably executed. With a wealth of competing decoding algorithms, a QEC system designer needs reliable methods to evaluate them. Today, the dominant approach is to evaluate decoders using Monte Carlo simulation. However, simulation has several drawbacks such as requiring many samples to produce low variance estimates. In this work, we develop a new systematic analysis for evaluating decoders. We introduce a novel formal semantics of a core language for QEC programs that captures the de facto standard Stim circuit format, providing a principled theoretical foundation for the emerging space of fault-tolerant quantum systems design. Given a QEC program and a decoder, our verifier can quantify both the decoder accuracy and the decoder robustness to drift in physical error rate. Our approach has two key components: (i) a structured search over the space of possible errors; and (ii) a constrained polynomial optimization kernel. A thorough empirical evaluation of our approach suggests that it can outperform simulation, especially in low error rate regimes, and that it can be deployed to quantify decoder robustness over an interval of physical error rates.

cs.PLCross-listedarXiv:2603.20127•Mar 23, 2026•0 citations

Verifying Fault-Tolerance of Quantum Error Correction Codes

Kean Chen, Yuhao Liu, Wang Sheng Fang +5 more

Abstract Quantum computers have advanced rapidly in qubit count and gate fidelity. However, large-scale fault-tolerant quantum computing still relies on quantum error correction code (QECC) to suppress noise. Manually or experimentally verifying the fault-tolerance property of complex QECC implementation is impractical due to the vast error combinations. This paper formalizes the fault-tolerance of QECC implementations within the language of quantum programs. By incorporating the techniques of quantum symbolic execution, we provide an automatic verification tool for quantum fault-tolerance. We evaluate and demonstrate the effectiveness of our tool on a universal set of logical operations across different QECCs.

arXiv:2501.14380•Lecture notes in computer science•Jan 1, 2025•7 citations

Error Mitigation of Fault-Tolerant Quantum Circuits with Soft Information

Zeyuan Zhou, Shaun Pexton, Aleksander Kubica +1 more

Quantum error mitigation (QEM) is typically viewed as a suite of practical techniques for today's noisy intermediate-scale quantum devices, with limited relevance once fault-tolerant quantum computers become available. In this work, we challenge this conventional wisdom by showing that QEM can continue to provide substantial benefits in the era of quantum error correction (QEC), and in an even more efficient manner than it does on current devices. We introduce a framework for logical-level QEM that leverages soft information naturally produced by QEC decoders, requiring no additional data, hardware modifications, or runtime overhead beyond what QEC protocols already provide. Within this framework, we develop and analyze three logical-level QEM techniques: post-selection and runtime abort policies, probabilistic error cancellation, and zero-noise extrapolation. Our techniques reduce logical error rates by more than 100x while discarding fewer than 0.1% of shots; they also provide in situ characterization of logical channels for QEM protocols. As a proof of principle, we benchmark our approach using a surface-code architecture and two state-of-the-art decoders based on tensor-network contraction and minimum-weight perfect matching. We evaluate logical-level QEM on random Clifford circuits and molecular simulation algorithms and find that, compared to previous approaches relying on QEC only or QEC combined with QEM, we can achieve up to 87.4% spacetime overhead savings. Our results demonstrate that logical-level QEM with QEC decoder soft information can reliably improve logical performance, underscoring the efficiency and usefulness of QEM techniques for fault-tolerant quantum computers.

quant-pharXiv:2512.09863•Dec 11, 2025•0 citations
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.
Quantum Error Correction (QEC) is essential for fault-tolerant quantum copmutation, and its implementation is a very sophisticated process involving both quantum and classical hardware. Formulating and verifying the decomposition of logical operations into physical ones is a challenge in itself. In this paper, we propose QECV, a verification framework that can efficiently verify the formal correctness of stabilizer codes, arguably the most important class of QEC codes. QECV first comes with a concise language, QECV-Lang, where stabilizers are treated as a first-class object, to represent QEC programs. Stabilizers are also used as predicates in our new assertion language, QECV-Assn, as logical and arithmetic operations of stabilizers can be naturally defined. We derive a sound quantum Hoare logic proof system with a set of inference rules for QECV to efficiently reason about the correctness of QEC programs. We demonstrate the effectiveness of QECV with both theoretical complexity analysis and in-depth case studies of two well-known stabilizer QEC codes, the repetition code and the surface code.
Quantum error-correcting codes (QECCs) sit between noisy quantum hardware and reliable computation, so the code parameters used in practice must be trustworthy. The single number that summarizes a code's strength is its distance, yet certifying a distance lower bound is NP-hard in general, placing it beyond the reach of pen-and-paper proofs as well as direct proof-assistant scripting. As a result, distance values in the literature come either from non-scaling hand proofs, or from unverified solvers that leave a trust gap exactly where the code is supposed to provide a guarantee. We present Lean-QEC, the first Lean 4 formalization of stabilizer-code theory that delivers end-to-end, machine-checked distance certificates at industrial code sizes. Lean-QEC formalizes the linear algebra of qubit states, the Pauli group, stabilizer codes, the binary symplectic representation, classical coding theory, and the CSS and Bivariate Bicycle families. To break the combinatorial barrier, Lean-QEC translates the distance condition into a Boolean satisfiability formula through a verified reduction. The pipeline scales through a BitVec-flattened encoding that replaces Lean's Matrix representation, and an error-location encoding that reduces the variable count from nnn to k⌈log⁡2n⌉k\lceil \log_2 n\rceilk⌈log2​n⌉. With these, we obtain automatically-generated Lean-checked distance proofs for a large range of industrially viable qLDPC codes within the Bivariate Bicycle and Generalized Bicycle families, including [[90, 8, 10]] and [[70, 6, 9]] BB codes, with the formulation scaling up to 144 qubits when performed outside the Lean kernel. The resulting library is reusable and is designed to plug into broader Lean-based efforts toward end-to-end verification of fault-tolerant quantum computation.
This paper presents a novel approach to quantum error correction (QEC) by formally specifying QEC codes using mathematical logic. The core idea is to translate the mathematical definitions and properties of QEC codes into logical formulas, enabling automated verification and facilitating the design of new, more efficient codes. This approach moves beyond intuitive understanding and provides a rigorous, verifiable framework. The paper outlines the methodology, demonstrates its application with a simplified example, and highlights the potential benefits of this formal specification technique for QEC research and development. The focus is on building a foundation for automated code design and analysis, crucial for the practical implementation of large-scale quantum computers. This work contributes to a more robust and trustworthy approach to QEC, addressing the challenges of complexity and verification inherent in traditional design methods.
Quantum error correction (QEC) enables reliable computation on noisy hardware by encoding logical information across many physical qubits and periodically measuring parities to detect errors. A decoder is the classical algorithm that uses these measurements to infer which error most likely occurred, so that the system can correct it. The decoder's accuracy-how rarely it makes the wrong guess-directly determines the scale of quantum computation that can be reliably executed. With a wealth of competing decoding algorithms, a QEC system designer needs reliable methods to evaluate them. Today, the dominant approach is to evaluate decoders using Monte Carlo simulation. However, simulation has several drawbacks such as requiring many samples to produce low variance estimates. In this work, we develop a new systematic analysis for evaluating decoders. We introduce a novel formal semantics of a core language for QEC programs that captures the de facto standard Stim circuit format, providing a principled theoretical foundation for the emerging space of fault-tolerant quantum systems design. Given a QEC program and a decoder, our verifier can quantify both the decoder accuracy and the decoder robustness to drift in physical error rate. Our approach has two key components: (i) a structured search over the space of possible errors; and (ii) a constrained polynomial optimization kernel. A thorough empirical evaluation of our approach suggests that it can outperform simulation, especially in low error rate regimes, and that it can be deployed to quantify decoder robustness over an interval of physical error rates.
Abstract Quantum computers have advanced rapidly in qubit count and gate fidelity. However, large-scale fault-tolerant quantum computing still relies on quantum error correction code (QECC) to suppress noise. Manually or experimentally verifying the fault-tolerance property of complex QECC implementation is impractical due to the vast error combinations. This paper formalizes the fault-tolerance of QECC implementations within the language of quantum programs. By incorporating the techniques of quantum symbolic execution, we provide an automatic verification tool for quantum fault-tolerance. We evaluate and demonstrate the effectiveness of our tool on a universal set of logical operations across different QECCs.
Quantum error mitigation (QEM) is typically viewed as a suite of practical techniques for today's noisy intermediate-scale quantum devices, with limited relevance once fault-tolerant quantum computers become available. In this work, we challenge this conventional wisdom by showing that QEM can continue to provide substantial benefits in the era of quantum error correction (QEC), and in an even more efficient manner than it does on current devices. We introduce a framework for logical-level QEM that leverages soft information naturally produced by QEC decoders, requiring no additional data, hardware modifications, or runtime overhead beyond what QEC protocols already provide. Within this framework, we develop and analyze three logical-level QEM techniques: post-selection and runtime abort policies, probabilistic error cancellation, and zero-noise extrapolation. Our techniques reduce logical error rates by more than 100x while discarding fewer than 0.1% of shots; they also provide in situ characterization of logical channels for QEM protocols. As a proof of principle, we benchmark our approach using a surface-code architecture and two state-of-the-art decoders based on tensor-network contraction and minimum-weight perfect matching. We evaluate logical-level QEM on random Clifford circuits and molecular simulation algorithms and find that, compared to previous approaches relying on QEC only or QEC combined with QEM, we can achieve up to 87.4% spacetime overhead savings. Our results demonstrate that logical-level QEM with QEC decoder soft information can reliably improve logical performance, underscoring the efficiency and usefulness of QEM techniques for fault-tolerant quantum computers.