Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally requires significant effort. To address this challenge, we present Qafny, an automated proof system based on the program verifier Dafny and designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations modeled within a classical separation logic framework. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs and specifications into Dafny for automated verification purposes. We then illustrate the utility of Qafny's automated capabilities in efficiently verifying important quantum algorithms, including quantum-walk algorithms, Grover's algorithm, and Shor's algorithm.

翻译：由于量子程序的概率性/非确定性行为，强烈建议对其进行形式化验证以确保其正确实现规范。然而，形式化验证传统上也需耗费大量精力。为应对这一挑战，我们提出了Qafny——一个基于程序验证器Dafny、专为验证量子程序设计的自动化证明系统。Qafny的核心采用类型引导的量子证明系统，将量子操作转换为在经典分离逻辑框架内建模的经典数组操作。我们证明了该证明系统的可靠性与完备性，并实现了一个原型编译器，可将Qafny程序及规范转换为Dafny代码以实现自动化验证。最后，我们通过高效验证量子行走算法、Grover算法和Shor算法等重要量子算法，展示了Qafny自动化验证能力的实用性。