Formal verification has been proven instrumental to ensure that quantum programs implement their specifications but often requires a significant investment of time and labor. To address this challenge, we present Qafny, an automated proof system designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations. By modeling these operations as proof rules within a classical separation logic framework, Qafny provides automated support for the reasoning process that would otherwise be tedious and time-consuming. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs both into the Dafny programming language and into executable quantum circuits. Using Qafny, we demonstrate how to efficiently verify prominent quantum algorithms, including quantum-walk algorithms, Grover's search algorithm, and Shor's factoring algorithm, with significantly reduced human efforts.

翻译：形式化验证已被证明是确保量子程序实现其规约的关键手段，但通常需要投入大量时间和人力。为应对这一挑战，我们提出Qafny——一种专为验证量子程序设计的自动化证明系统。其核心采用类型引导的量子证明系统，将量子操作转化为经典数组操作。通过将这些操作建模为经典分离逻辑框架中的证明规则，Qafny为原本繁琐耗时的推理过程提供自动化支持。我们证明了该证明系统的可靠性与完备性，并实现了一个原型编译器，可将Qafny程序同时转化为Dafny编程语言及可执行的量子电路。利用Qafny，我们展示了如何高效验证包括量子行走算法、Grover搜索算法和Shor质因数分解算法在内的典型量子算法，显著降低了人力成本。