Artifact for 'Efficient Formal Verification of Quantum Error Correcting Programs'

This is the research artifact attached to the research paper 'Efficient Formal Verification for Quantum Error Correcting Programs'. Corresponding to the paper, the artifact consists of two modules: a verified QEC verifier developed in Coq, and a Python-based tool designed to automate the verification for quantum error correcting programs. The source codes and documentation of the verified QEC verifier are located in dirac-project-veriQEC.zip. Due to memory limit issues, we cannot provide a pre-packaged docker image because the excessively large amount of image (estimated size >16 G). We provide a dockerfile for reviewers to build by themselves. Indeed, we recommend that reviewers follow the instructions in the README to locally configure Opam and the Coq dependencies. The materials and documentation of the Python-based tool Veri-qec are located in Veri-qec.zip. We provide a detailed documentation, along with source codes and all evaluation results that support the claims in the paper. In addition we provide a docker container docker-veriqec.tar. Reviewers can choose to either directly load this docker container or build from the Dockerfile we provide in source codes.

Huang, Q., Zhou, L., Fang, W., Zhao, M., & Ying, M. (2025). Artifact for 'Efficient Formal Verification of Quantum Error Correcting Programs'. Zenodo. https://doi.org/10.5281/zenodo.15039214