Qafny: A Quantum-Program Verifier

TL;DR

Qafny provides a type-guided, locus-based framework for automatically verifying quantum programs by translating quantum operations to classical array reasoning within a separation-logic setting. It introduces a trio of core ideas—Locus, Type, and State—to statically track entanglement and qubit positions, enabling automated proofs of quantum conditionals and loops (via the F and U transformers) and proving type soundness and relative completeness. The system includes a Dafny-based compiler and a translation to Sep, enabling verification with classical tools, and demonstrates automated verification on key algorithms such as GHZ, quantum walk, Grover, and Shor, with case studies showing composability and rapid prototyping. Together, these contributions connect quantum program verification to classical Hoare/separation logic, delivering automation and scalability advantages for HCQ program verification with practical impact for algorithm design and correctness guarantees.

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.

Figures (46)

• Figure 1: GHZ Examples. $x[t_1,t_2)\mapsto \ket{\overline{0}}$ means $\overline{0}$ is a bitstring of length $t_2\texttt{-} t_1$. $x[t_1,t_2)\mapsto \mathop{\mathrm{\text{$\sum$}}}\limits_{d=0}^{1}{}{\ket{\overline{d}}}$ means $\overline{d}$ is a bitstring of length $t_2\texttt{-} t_1$ and $d\in[0,1]$ is a bit. $*$ is the separation conjunction. In (c), black parts are Qafny programs, while blue and gray parts are Qafny state predicates.
• Figure 5: Qafny element syntax. Each range $x[n,m)$ in a locus represents the number range $[n,m)$ in physical qubit array $x$. Loci are finite lists, while type environments and states are finite sets. The operations after "concatenated op" are concatenations for loci, type environments, and quantum states.
• Figure 6: Detailed automated proof for a loop-step in GHZ. Constructed from the bottom up.
• Figure 7: Snippets from quantum order finding in Shor's algorithm; full proof in appx:shors. $\texttt{ord}({a,N})$ gets the order of $a$ and $N$. $\texttt{rnd}({r})$ rounds $r$ to the nearest integer. We interpret integers as bitstrings in $\ket{i}$ and $\ket{a^{i}\;\texttt{\%}\;N}$. The right column presents the types of all loci involved.
• Figure 9: Selected semantic rules. $\{\space| c |\space\}$ turns basis $c$ to an integer.

Theorems & Definitions (12)

• Definition 1: Well-formed Qafny state
• Theorem 2: Qafny type soundness
• Theorem 3: proof system soundness
• Theorem 4: proof system relative completeness
• Definition 5: Well-formed locus domain
• Definition 6: Well-formed state predicate
• Theorem 7: Qafny to SQIR Compilation Correctness
• Definition 8: Well-formed oqasm state
• Theorem 9
• Theorem 10