{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T19:50:46Z","timestamp":1784836246579,"version":"3.55.0"},"reference-count":92,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","funder":[{"DOI":"10.13039\/501100012166","name":"National Key R&D Program of China","doi-asserted-by":"crossref","award":["2023YFA1009403"],"award-info":[{"award-number":["2023YFA1009403"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3729293","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1068-1093","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Efficient Formal Verification of Quantum Error Correcting Programs"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-6548-4303","authenticated-orcid":false,"given":"Qifan","family":"Huang","sequence":"first","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, Beijing, China"},{"name":"University of Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9868-8477","authenticated-orcid":false,"given":"Li","family":"Zhou","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7628-1185","authenticated-orcid":false,"given":"Wang","family":"Fang","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-8436-3532","authenticated-orcid":false,"given":"Mengyu","family":"Zhao","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, Beijing, China"},{"name":"University of Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4847-702X","authenticated-orcid":false,"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[{"name":"University of Technology Sydney, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.70.052328"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-024-08449-y"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-022-05434-1"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Matthew Amy. 2018. Towards Large-scale Functional Verification of Universal Quantum Circuits. In Proceedings 15th International Conference on Quantum Physics and Logic QPL 2018 Halifax Canada 3-7th June 2018 (EPTCS Vol. 287) Peter Selinger and Giulio Chiribella (Eds.). 1\u201321. doi:10.4204\/EPTCS.287.1","DOI":"10.4204\/EPTCS.287.1"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.73.022334"},{"key":"e_1_3_2_7_2","first-page":"39","article-title":"The logic of quantum programs","author":"Baltag Alexandru","year":"2004","unstructured":"Alexandru Baltag and Sonja Smets. 2004. The logic of quantum programs. Proc. QPL (2004), 39\u201356. https:\/\/philsci-archive.pitt.edu\/1799\/","journal-title":"Proc. QPL"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-023-06927-3"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-022-04592-6"},{"key":"e_1_3_2_13_2","first-page":"53","volume-title":"Boogie 2011: First International Workshop on Intermediate Verification Languages","author":"Bobot Fran\u00e7ois","year":"2011","unstructured":"Fran\u00e7ois Bobot, Jean-Christophe Filli\u00e2tre, Claude March\u00e9, and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages. Wroclaw, Poland, 53\u201364. https:\/\/inria.hal.science\/hal-00790310"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41467-021-22274-1"},{"key":"e_1_3_2_15_2","article-title":"Isabelle marries dirac: A library for quantum computation and quantum information","author":"Bordg Anthony","year":"2020","unstructured":"Anthony Bordg, Hanna Lachnitt, and Yijun He. 2020. Isabelle marries dirac: A library for quantum computation and quantum information. Archive of Formal Proofs (2020).","journal-title":"Archive of Formal Proofs"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09584-7"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-024-07107-7"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.86.052329"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1103\/PRXQuantum.2.040101"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749904000067"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/18.681315"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.54.1098"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.95.022316"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571786.3573018"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1201\/9781003090052-7"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591270"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1063\/1.1499754"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656419"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.011"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02283036"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2021-07-06-497"},{"key":"e_1_3_2_38_2","unstructured":"Daniel Gottesman. 1997. Stabilizer Codes and Quantum Error Correction. arXiv:quant-ph\/9705052 [quant-ph]"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Markus Grassl and Martin Roetteler. 2013. Leveraging automorphisms of quantum codes for fault-tolerant quantum computation. In 2013 IEEE International Symposium on Information Theory. 534\u2013538. doi:10.1109\/ISIT.2013.6620283","DOI":"10.1109\/ISIT.2013.6620283"},{"key":"e_1_3_2_40_2","volume-title":"Digital systems design with FPGAs and CPLDs","author":"Grout Ian","year":"2011","unstructured":"Ian Grout. 2011. Digital systems design with FPGAs and CPLDs. Elsevier."},{"key":"e_1_3_2_41_2","unstructured":"Kesha Hietala Sarah Marshall Robert Rand and Nikhil Swamy. 2022. Q*: Implementing Quantum Separation Logic in F*. Programming Languages for Quantum Computing (PLanQC) 2022 Poster Abstract (2022). https:\/\/khieta.github.io\/files\/drafts\/qstar-planqc22.pdf"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Qifan Huang Li Zhou Wang Fang Mengyu Zhao and Mingsheng Ying. 2025. Artifact for Efficient Formal Verification of Quantum Error Correcting Programs\u2019. doi:10.5281\/zenodo.15248774","DOI":"10.5281\/zenodo.15248774"},{"key":"e_1_3_2_44_2","doi-asserted-by":"crossref","unstructured":"Qifan Huang Li Zhou Wang Fang Mengyu Zhao and Mingsheng Ying. 2025. Efficient Formal Verification of Quantum Error Correcting Programs. arXiv:2504.07732 [cs.PL]","DOI":"10.1145\/3729293"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446750"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","unstructured":"Aleks Kissinger and John van de Wetering. 2019. PyZX: Large Scale Automated Diagrammatic Reasoning. In Proceedings 16th International Conference on Quantum Physics and Logic QPL 2019 Chapman University Orange CA USA June 10-14 2019 (EPTCS Vol. 318) Bob Coecke and Matthew Leifer (Eds.). 229\u2013241. doi:10.4204\/EPTCS.318.14","DOI":"10.4204\/EPTCS.318.14"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1070\/RM1997v052n06ABEH002155"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/isit.2012.6284206"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12732-1"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/17\/8\/083026"},{"key":"e_1_3_2_52_2","unstructured":"Andrew J. Landahl Jonas T. Anderson and Patrick R. Rice. 2011. Fault-tolerant quantum computing with color codes. arXiv:1108.5738 [quant-ph]"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498697"},{"key":"e_1_3_2_54_2","unstructured":"Adrian Lehmann Ben Caldwell and Robert Rand. 2022. VyZX : A Vision for Verifying the ZX Calculus. arXiv:2205.05781 [quant-ph]"},{"key":"e_1_3_2_55_2","unstructured":"Adrian Lehmann Ben Caldwell Bhakti Shah and Robert Rand. 2023. VyZX: Formal Verification of a Graphical Quantum Language. arXiv:2311.11571 [cs.PL]"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","unstructured":"Anthony Leverrier and Gilles Z\u00e9mor. 2022. Quantum Tanner codes. In 2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS). 872\u2013883. doi:10.1109\/FOCS54457.2022.00117","DOI":"10.1109\/FOCS54457.2022.00117"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3624483"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2024.24"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2021.136"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7118596"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511976667"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1126\/science.1253742"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2018-08-06-79"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","unstructured":"Robert Rand Jennifer Paykin Dong-Ho Lee and Steve Zdancewic. 2018. ReQWIRE: Reasoning about Reversible Quantum Circuits. In Proceedings 15th International Conference on Quantum Physics and Logic QPL 2018 Halifax Canada 3-7th June 2018 (EPTCS Vol. 287) Peter Selinger and Giulio Chiribella (Eds.). 299\u2013312. doi:10.4204\/EPTCS.287.17","DOI":"10.4204\/EPTCS.287.17"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","unstructured":"Robert Rand Jennifer Paykin and Steve Zdancewic. 2017. QWIRE Practice: Formal Verification of Quantum Circuits in Coq. In Proceedings 14th International Conference on Quantum Physics and Logic QPL 2017 Nijmegen The Netherlands 3-7 July 2017. (EPTCS Vol. 266) Bob Coecke and Aleks Kissinger (Eds.). 119\u2013132. doi:10.4204\/EPTCS.266.8","DOI":"10.4204\/EPTCS.266.8"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.340.14"},{"key":"e_1_3_2_69_2","unstructured":"Robert Rand Aarthi Sundaram Kartik Singhal and Brad Lackey. 2021. Static Analysis of Quantum Programs via Gottesman Types. arXiv:2101.08939 [quant-ph]"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevX.11.041058"},{"key":"e_1_3_2_71_2","unstructured":"C. Ryan-Anderson N. C. Brown M. S. Allman B. Arkin et al. 2022. Implementing Fault-tolerant Entangling Gates on the Five-qubit Code and the Color Code. arXiv:2208.01863 [quant-ph]"},{"key":"e_1_3_2_72_2","doi-asserted-by":"crossref","unstructured":"Bhakti Shah William Spencer Laura Zielinski Ben Caldwell Adrian Lehmann and Robert Rand. 2024. ViCAR: Visualizing Categories with Automated Rewriting in Coq. arXiv:2404.08163 [cs.PL]","DOI":"10.4204\/EPTCS.429.13"},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.1996.0136"},{"key":"e_1_3_2_74_2","doi-asserted-by":"publisher","DOI":"10.1109\/18.771249"},{"key":"e_1_3_2_75_2","unstructured":"Aarthi Sundaram Robert Rand Kartik Singhal and Brad Lackey. 2022. Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs. http:\/\/rand.cs.uchicago.edu\/files\/heisenberg_logic_2023.pdf"},{"key":"e_1_3_2_76_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_77_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523431"},{"key":"e_1_3_2_78_2","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2022. The Coq Proof Assistant. doi:10.5281\/zenodo.5846982","DOI":"10.5281\/zenodo.5846982"},{"key":"e_1_3_2_79_2","unstructured":"The MathComp Analysis Development Team. 2024. MathComp-Analysis: Mathematical Components compliant Analysis Library. https:\/\/github.com\/math-comp\/analysis. Since 2017. Version 1.0.0."},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.2013.2292061"},{"key":"e_1_3_2_81_2","doi-asserted-by":"publisher","unstructured":"Dominique Unruh. 2019. Quantum Hoare Logic with Ghost Variables. In 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201313. doi:10.1109\/LICS.2019.8785779","DOI":"10.1109\/LICS.2019.8785779"},{"key":"e_1_3_2_82_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_3_2_83_2","volume-title":"Towards Large-Scale Quantum Computing. Ph.D. Dissertation","author":"Wu Anbang","year":"2024","unstructured":"Anbang Wu. 2024. Towards Large-Scale Quantum Computing. Ph.D. Dissertation. UC Santa Barbara. https:\/\/www.proquest.com\/dissertations-theses\/towards-large-scale-quantum-computing\/docview\/3050756793\/se-2"},{"key":"e_1_3_2_84_2","unstructured":"Anbang Wu Gushu Li Hezi Zhang Gian Giacomo Guerreschi Yuan Xie and Yufei Ding. 2021. QECV: Quantum Error Correction Verification. arXiv:2111.13728 [quant-ph]"},{"key":"e_1_3_2_85_2","unstructured":"Xiaosi Xu Simon Benjamin Jinzhao Sun Xiao Yuan and Pan Zhang. 2023. A Herculean task: Classical simulation of quantum computers. arXiv:2302.08880 [quant-ph]"},{"key":"e_1_3_2_86_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_2_87_2","volume-title":"Foundations of Quantum Programming","author":"Ying Mingsheng","year":"2024","unstructured":"Mingsheng Ying. 2024. Foundations of Quantum Programming (second edition ed.). Morgan Kaufmann."},{"key":"e_1_3_2_88_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_3_2_89_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.129.030501"},{"key":"e_1_3_2_90_2","doi-asserted-by":"publisher","unstructured":"Li Zhou Gilles Barthe Justin Hsu Mingsheng Ying and Nengkun Yu. 2021. A Quantum Interpretation of Bunched Logic amp; Quantum Separation Logic. In 2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201314. doi:10.1109\/LICS52264.2021.9470673","DOI":"10.1109\/LICS52264.2021.9470673"},{"key":"e_1_3_2_91_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571222"},{"key":"e_1_3_2_92_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"},{"key":"e_1_3_2_93_2","unstructured":"Jacob Zweifler Kesha Hietala and Robert Rand. 2022. QuantumLib: A Library for Quantum Computing in Coq."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729293","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:04:20Z","timestamp":1784196260000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729293"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":92,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729293"],"URL":"https:\/\/doi.org\/10.1145\/3729293","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}