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代码以实现自动化验证。最后，我们展示了Qafny在高效验证重要量子算法（包括量子游走算法、Grover算法和Shor算法）中的自动化能力。