一句话：提出 Qafny c，将量子程序验证编译到经典验证器 Dafny，并验证 37 个量子程序。
量子程序因固有的概率性与叠加并行性而难以验证，现有量子程序验证仍处于早期阶段。本文提出 Qafny c，将量子程序验证编译到成熟的经典程序验证器 Dafny 中，以实现量子程序的形式化验证。其核心洞察是将量子程序验证与执行分离：先借助经典验证器的能力确保正确性，再将已认证的量子程序编译为可执行电路。作者使用 Qafny c 成功验证了 37 个不同的量子程序，据称这是目前最广泛的经形式化验证的量子程序集合。
Despite recent development of quantum program verification, it is still in its early stage, where many quantum programs are hard to verify due to their inherent probabilistic nature and parallelism in quantum superposition. We propose Qafny c , a system that compiles quantum program verification into a well-established classical program verifier Dafny, enabling the formal verification of quantum programs. The key insight behind Qafny c is the separation of quantum program verification from its execution, leveraging the strength of classical verifiers to ensure correctness before compiling certified quantum programs into executable circuits. Using Qafny c , we have successfully verified 37 diverse quantum programs by compiling their verification into Dafny. To the best of our knowledge, this is the most extensive formally verified set of quantum programs.
@article{paperbot3011,
title = {Embedding Quantum Program Verification into Dafny},
author = {Feifei Cheng and Sushen Vangeepuram and Henry Allard and Seyed Mohammad Reza Jafari and Alex Potanin and Liyi Li},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763157}
}