{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:33Z","timestamp":1780994613914,"version":"3.54.1"},"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":16,"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_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.70.052328"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-024-08449-y"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-022-05434-1"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.287.1"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.73.022334"},{"key":"e_1_2_2_6_1","volume-title":"Proc. QPL, 39\u201356","author":"Baltag Alexandru","year":"2004","unstructured":"Alexandru Baltag and Sonja Smets. 2004. The logic of quantum programs. Proc. QPL, 39\u201356. https:\/\/philsci-archive.pitt.edu\/1799\/"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-023-06927-3"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-022-04592-6"},{"key":"e_1_2_2_12_1","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_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41467-021-22274-1"},{"key":"e_1_2_2_14_1","unstructured":"Anthony Bordg Hanna Lachnitt and Yijun He. 2020. Isabelle marries dirac: A library for quantum computation and quantum information. Archive of Formal Proofs."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09584-7"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-024-07107-7"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.86.052329"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1103\/PRXQuantum.2.040101"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749904000067"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/18.681315"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.54.1098"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.95.022316"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571786.3573018"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_2_2_26_1","volume-title":"Beno\u00eet Valiron, Renaud Vilmart, and Zhaowei Xu.","author":"Chareton Christophe","year":"2023","unstructured":"Christophe Chareton, S\u00e9bastien Bardin, Dong Ho Lee, Beno\u00eet Valiron, Renaud Vilmart, and Zhaowei Xu. 2023. Formal Methods for Quantum Algorithms. In Handbook of Formal Analysis and Verification in Cryptography. CRC Press, 319\u2013422. https:\/\/cea.hal.science\/cea-04479879"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591270"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.1499754"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656419"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.011"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02283036"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.22331\/q-2021-07-06-497"},{"key":"e_1_2_2_37_1","unstructured":"Daniel Gottesman. 1997. Stabilizer Codes and Quantum Error Correction. arxiv:quant-ph\/9705052."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISIT.2013.6620283"},{"key":"e_1_2_2_39_1","volume-title":"Digital systems design with FPGAs and CPLDs","author":"Grout Ian","unstructured":"Ian Grout. 2011. Digital systems design with FPGAs and CPLDs. Elsevier."},{"key":"e_1_2_2_40_1","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 https:\/\/khieta.github.io\/files\/drafts\/qstar-planqc22.pdf"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","unstructured":"Qifan Huang Li Zhou Wang Fang Mengyu Zhao and Mingsheng Ying. 2025. Artifact for \u2019Efficient Formal Verification of Quantum Error Correcting Programs\u2019. https:\/\/doi.org\/10.5281\/zenodo.15248774 10.5281\/zenodo.15248774","DOI":"10.5281\/zenodo.15248774"},{"key":"e_1_2_2_43_1","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.","DOI":"10.1145\/3729293"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446750"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.318.14"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1070\/RM1997v052n06ABEH002155"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/isit.2012.6284206"},{"key":"e_1_2_2_49_1","volume-title":"States, Effects, and Operations Fundamental Notions of Quantum Theory: Lectures in Mathematical Physics at the University of Texas at Austin","author":"Kraus Karl","unstructured":"Karl Kraus, Arno B\u00f6hm, John D Dollard, and WH Wootters. 1983. States, Effects, and Operations Fundamental Notions of Quantum Theory: Lectures in Mathematical Physics at the University of Texas at Austin. Springer."},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/17\/8\/083026"},{"key":"e_1_2_2_51_1","volume-title":"Rice","author":"Landahl Andrew J.","year":"2011","unstructured":"Andrew J. Landahl, Jonas T. Anderson, and Patrick R. Rice. 2011. Fault-tolerant quantum computing with color codes. arxiv:1108.5738."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498697"},{"key":"e_1_2_2_53_1","unstructured":"Adrian Lehmann Ben Caldwell and Robert Rand. 2022. VyZX : A Vision for Verifying the ZX Calculus. arxiv:2205.05781."},{"key":"e_1_2_2_54_1","unstructured":"Adrian Lehmann Ben Caldwell Bhakti Shah and Robert Rand. 2023. VyZX: Formal Verification of a Graphical Quantum Language. arxiv:2311.11571."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS54457.2022.00117"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3624483"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2024.24"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2021.136"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","unstructured":"Assia Mahboubi and Enrico Tassi. 2022. Mathematical Components. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.7118596 10.5281\/zenodo.7118596","DOI":"10.5281\/zenodo.7118596"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"e_1_2_2_61_1","unstructured":"M.A. Nielsen and I.L. Chuang. 2010. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press. isbn:9781139495486"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","unstructured":"D. Nigg M. M\u00fcller E. A. Martinez P. Schindler M. Hennrich T. Monz M. A. Martin-Delgado and R. Blatt. 2014. Quantum computations on a topologically encoded qubit. Science 345 6194 (2014) 302\u2013305. https:\/\/doi.org\/10.1126\/science.1253742 10.1126\/science.1253742","DOI":"10.1126\/science.1253742"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.22331\/q-2018-08-06-79"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.287.17"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.266.8"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.340.14"},{"key":"e_1_2_2_68_1","unstructured":"Robert Rand Aarthi Sundaram Kartik Singhal and Brad Lackey. 2021. Static Analysis of Quantum Programs via Gottesman Types. arxiv:2101.08939."},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevX.11.041058"},{"key":"e_1_2_2_70_1","unstructured":"C. Ryan-Anderson N. C. Brown M. S. Allman and B. Arkin. 2022. Implementing Fault-tolerant Entangling Gates on the Five-qubit Code and the Color Code. arxiv:2208.01863."},{"key":"e_1_2_2_71_1","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."},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.1996.0136"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1109\/18.771249"},{"key":"e_1_2_2_74_1","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_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523431"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2022. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.5846982 10.5281\/zenodo.5846982","DOI":"10.5281\/zenodo.5846982"},{"key":"e_1_2_2_78_1","volume-title":"MathComp-Analysis: Mathematical Components compliant Analysis Library. https:\/\/github.com\/math-comp\/analysis Since","author":"MathComp Analysis Development The","year":"2017","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_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.2013.2292061"},{"key":"e_1_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785779"},{"key":"e_1_2_2_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_2_2_82_1","unstructured":"Anbang Wu. 2024. Towards Large-Scale Quantum Computing. Ph. D. Dissertation. UC Santa Barbara. isbn:9798382341804 https:\/\/www.proquest.com\/dissertations-theses\/towards-large-scale-quantum-computing\/docview\/3050756793\/se-2"},{"key":"e_1_2_2_83_1","volume-title":"Yuan Xie, and Yufei Ding.","author":"Wu Anbang","year":"2021","unstructured":"Anbang Wu, Gushu Li, Hezi Zhang, Gian Giacomo Guerreschi, Yuan Xie, and Yufei Ding. 2021. QECV: Quantum Error Correction Verification. arxiv:2111.13728."},{"key":"e_1_2_2_84_1","unstructured":"Xiaosi Xu Simon Benjamin Jinzhao Sun Xiao Yuan and Pan Zhang. 2023. A Herculean task: Classical simulation of quantum computers. arxiv:2302.08880."},{"key":"e_1_2_2_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_2_2_86_1","volume-title":"Foundations of Quantum Programming","author":"Ying Mingsheng","unstructured":"Mingsheng Ying. 2024. Foundations of Quantum Programming (second edition ed.). Morgan Kaufmann. isbn:978-0-443-15942-8"},{"key":"e_1_2_2_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_2_2_88_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.129.030501"},{"key":"e_1_2_2_89_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470673"},{"key":"e_1_2_2_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571222"},{"key":"e_1_2_2_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"},{"key":"e_1_2_2_92_1","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":[[2025,7,16]],"date-time":"2025-07-16T06:05:09Z","timestamp":1752645909000},"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"}}]}}