# Techniques: Efficient Formal Verification of Quantum Error Correcting Programs

## What the paper contributes (one paragraph)

The paper presents a formal verification framework for quantum error correcting (QEC) programs. It defines a dedicated assertion logic and Hoare-style program logic that use Pauli expressions as atomic propositions and add classical variables to model errors, syndromes and properties such as the maximum number of correctable errors, all interpreted over quantum logic with a sound proof system. It develops an efficient method to discharge the verification conditions: for Pauli errors these reduce to classical assertions solvable by SMT solvers, and for non-Pauli errors a heuristic algorithm eliminates non-commuting terms. The proof system is mechanised in the Coq proof assistant, yielding a verified verifier, and an automated tool, Veri-QEC, is implemented in Python using the Z3 and CVC5 SMT solvers with a parallel checking framework. The authors verify many fault-tolerant scenarios and supply a benchmark of 14 verified stabilizer codes ranging from 5 to 361 qubits.

## Techniques offered
- **formal verification of QEC programs (assertion logic and program logic)** - a Hoare-style program logic plus assertion logic, with a soundness proof, that proves a QEC program satisfies its correctness specification including conditions on errors such as the maximum correctable number.
  - guarantee: static proof of program correctness via a proof system whose soundness is established (and mechanised in Coq).
  - quote: "We define an assertion logic and a program logic specifically crafted for QEC programs and establish a sound proof system."
- **SMT-based verification-condition checking (equivalence checking of stabilizer specifications)** - a method that reduces the verification conditions generated for QEC codes to classical assertions discharged by SMT solvers for Pauli errors, with a heuristic algorithm handling non-Pauli errors.
  - guarantee: decision-procedure (SMT) discharge of verification conditions; unsat certifies the correctness property holds, sat returns a counterexample.
  - quote: "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."
- **machine-checked (Coq) verified verifier** - the program logic is formalised in the Coq proof assistant on top of CoqQ, so the verifier and pen-and-paper proofs of scalable codes are mechanically checked.
  - guarantee: machine-checked proof of the soundness of the proof system, ruling out a flawed logic.
  - quote: "We formalize the proposed program logic in Coq proof assistant, making it a verified QEC verifier."
- **automated QEC verifier (Veri-QEC tool) and verified-code benchmark** - an automated Python tool, Veri-QEC, that verifies fault-tolerant scenarios across stabilizer codes, packaged with a benchmark of 14 verified stabilizer codes.
  - guarantee: automated verification across error and fault-tolerant scenarios; benchmark of codes with verified properties.
  - quote: "Finally, we present a benchmark of 14 verified stabilizer codes."

## Where it could apply
- Target primitive(s): QEC programs and fault-tolerant logical circuits (stabilizer-code error correction cycles, syndrome decoding and correction, fault-tolerant Clifford and non-Clifford gate implementations); not VQE/QAOA/QPE/sampling.
- Target application group(s): error_correction, platforms_tooling.
- Code family / hardware assumptions: stabilizer codes including the rotated surface code, Steane code and repetition code (14 codes, 5 to 361 qubits); Clifford + T gate set; Pauli and limited non-Pauli (T, H) error models.

## Caveats
The gate set is restricted to Clifford + T and the projection-based logic cannot reason about probabilities; soundness is established but completeness for programs with while-loops remains open. The verified (Coq) and automatic (SMT) verifiers are separate tools rather than one unified solution. Tooling is open source (code and evaluated artefact available), so nothing is paywalled.