Formal Verification of Quantum Programs: Theory, Tools and Challenges

TL;DR

The survey surveys formal verification methods for quantum programs, including quantum weakest preconditions, quantum Hoare logic, quantum computation tree logic, path sums, and the ZX-calculus, and connects these theories to practical verification tools and languages. It discusses design choices for verification frameworks, highlighting trade-offs between environment integration, interactivity, and executability, and outlines key limitations such as no-cloning, limited classical functionality, and ancilla management. The paper reviews verifiable quantum programming languages (e.g., SQIR, QHLProver, CoqQ, IMD, QBricks) and related tools (QPMC, Feynmann, QMDDs, PyZX, CertiQ, QSharpCheck), illustrating how formal reasoning is applied to both textbook and non-textbook algorithms. It then uses complex algorithms like HHL and Binary Welded Trees to illustrate current verification capabilities and the substantial challenges ahead, emphasizing the need for scalable, user-friendly tools capable of handling measurements, classical data, and dynamic initialization. Overall, the work highlights that progress in formal verification is essential for the reliable deployment of quantum software as hardware scales, and it identifies concrete directions for future research and tool development.

Abstract

Over the past 27 years, quantum computing has seen a huge rise in interest from both academia and industry. At the current rate, quantum computers are growing in size rapidly backed up by the increase of research in the field. Significant efforts are being made to improve the reliability of quantum hardware and to develop suitable software to program quantum computers. In contrast, the verification of quantum programs has received relatively less attention. Verifying programs is especially important in the quantum setting due to how difficult it is to program complex algorithms correctly on resource-constrained and error-prone quantum hardware. Research into creating verification frameworks for quantum programs has seen recent development, with a variety of tools implemented using a collection of theoretical ideas. This survey aims to be a short introduction into the area of formal verification of quantum programs, bringing together theory and tools developed to date. Further, this survey examines some of the challenges that the field may face in the future, namely the development of complex quantum algorithms.

Figures (14)

• Figure 1: An example of a Kripke structure with $S = \{s_0, s_1, s_2\}$.
• Figure 2: A computation tree for the automata given in Figure \ref{['fig:model']} that shows the CTL operation $\textbf{E}(q \textbf{U}p)$. The proposition $q$ holds in states $s_0$ and $s_1$, but the proposition $p$ holds in state $s_2$.
• Figure 3: The Hadamard node (left), green spider (middle) and red spider (right) with their matrix representation. The vertices can have more than one edge enter and exit them, but for simplicity we consider the case when only one edge enters a vertex. The spiders represent rotations on an axis, with the green spider rotating around the $Z$-axis and the red spider rotating around the $X$-axis. Note that when $\alpha = 0$, the spiders are simply identity operators and when $\alpha = \pi$ the spiders represent the pauli-$Z$ and pauli-$X$ gate respectively.
• Figure 4: A number of different rewrite rules Backens17. It is important to note that the colours of spiders can be swapped (so green spiders replace red spiders and vice versa). The summation of scalars is modulo $2\pi$.
• Figure 5: Derivation of two Hadamard gates being equivalent to the identity operation using the rules of the ZX-calculus. The derivation uses instances of the rewrite rules given in Figure \ref{['fig:rewrite']}. Firstly, the Hadamard gates are decomposed and then the red spiders are merged. Two of the spiders are swapped and then the green spiders are merged. This combined green spider can be removed by the identity rule and the final red spiders can be similarly merged and removed. An alternative way of proving the Hadamard gate is self-inverse can be found in Backens17.

Theorems & Definitions (3)

• definition 1
• definition 2
• definition 3