Efficient Formal Verification of Quantum Error Correcting Programs
summary
An assertion-and-program logic with a sound proof system converts Pauli-error verification conditions into purely classical formulas solved by SMT solvers, and applies a heuristic for non‑Pauli cases; the proof system is mechanically checked in a Coq formalization and an automated tool Veri-QEC is implemented. The verifier proves 14 stabilizer codes, checks a surface-code instance with 121 physical qubits (distance 11) in ≈3.5 hours, and reaches ~360 qubits with region‑error constraints.
AI-written summary · about
chapters (13)
- 0:00Quantum error correction intro
- 1:25Stabilizer codes in QEC
- 3:34Quantum programs and QEC workflow
- 5:59Formal verification challenges
- 6:41Assertion logic for verification
- 9:13Program logic and proof system
- 10:39Efficient verification conditions
- 13:47Steane code case study
- 15:12Verification framework tools
- 16:58Performance benchmarks
- 17:39Comparison with tools
- 18:00Future directions
- 18:21Q&A
related talks
42mQuantum program analysis: Verification and Testing
22mCoqQ: Foundational Verification of Quantum Programs
15mToward A Quantum Programming Language for Higher Level Formal Verification
19mAvenues for Quantum Error Correction and Mitigation
29mEfficiently Verifying Quantum Programs with Few T Gates
13mQbC: Quantum Correctness by Construction
40mDemocratizing quantum formal verification: the path-sum way
22mQbC: Quantum Correctness by Construction