Qafny: A Quantum-Program Verifier

TL;DR

Qafny is an automated verification system that leverages classical logic tools to verify quantum programs, ensuring correctness of complex quantum algorithms efficiently.

Contribution

It introduces a novel type-guided proof system for quantum programs and integrates it with Dafny for automated verification.

Findings

Successfully verifies quantum algorithms like Grover's and Shor's.

Proves soundness and completeness of the quantum proof system.

Demonstrates efficiency in verifying complex quantum protocols.

Abstract

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.