Formal Verification of Quantum Programs]Formal Verification of Quantum Programs: Theory, Tools and Challenges

Marco Lewis
Sadegh Soudjani
Paolo Zuliani

Newcastle University

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. The importance of 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 developments of complex quantum algorithms.

§ INTRODUCTION

Quantum computers are capable of solving a variety of problems much faster than classical computers, as seen in Deutsch-Jozsa's and Grover's algorithms <cit.>. With recent results from Google <cit.> and the Hefei National Laboratory
<cit.>, it is becoming more realistic that large-scale quantum computers will be used by academics and companies alike. Within the next few years, we expect to see a quantum computer with the ability to perform computations on 100s or potentially 1,000 quantum bits (otherwise known as qubits), with IBM aiming to debut a 1,121 qubit computer in 2023.[
These planned devices are by no means ideal, as they are Noisy Intermediate-Scale Quantum (NISQ) <cit.> computers that are limited by having hundreds of qubits but no error correction. The quantum threshold theorem  provides the theoretical justification as for why arbitrarily long quantum computations are possible in principle, albeit it assumes quantum error correction.

The problem of error in quantum computers needs to be solved to make large-scale quantum computers usable. There are three potential reasons why an incorrect value is measured during a computation on a quantum circuit.
The first is due to the innate randomness when measuring qubits within quantum computers: When a qubit is measured, it commonly collapses into one of its two `basis' states.
Most quantum algorithms will only return the correct result with high probability (for example, consider the probability that Grover's algorithm will return the marked element of a database). Therefore, there is still a chance of measuring incorrect results, but this can be solved by running a quantum circuit multiple times and returning the results that is measured the most (as the correct result will be measured most of the time).

Another source of error is the hardware. Hardware error occurs when qubits are interfered with by gates or sources from outside of the system. Qubits may change state when going through a gate in a different way to what is expected, often referred to as gate infidelity.
Alternatively, errors can occur at readout when qubits are measured incorrectly. To prevent errors that change the phase or bit value of a qubit, error-correcting codes can be used <cit.> (see for example  <cit.> for a thorough investigation of the various techniques for achieving fault-tolerant quantum computing).

The final source of error is from within the software. This can occur at various stages, whether that would be when a programmer codes the algorithm incorrectly or if the compiled circuit is flawed.
To solve the error that comes within software, tools need to be developed to verify programs and compiled circuits.
By reducing errors within hardware and software, it can be guaranteed that readout distributions match those predicted by quantum theory.

This article is focused on the error caused by software and how to prevent it through the usage of formal verification. That involves the study and development of tools to verify programs and systems. Recent decades have seen the successful development of automatic provers capable of proving properties about programs or mathematical theories with the press of a button. Examples of such tools[Some can be found competing at competitions including SMT-COMP (<https://smt-comp.github.io/>) for SMT solvers and ARCH (<https://cps-vo.org/group/ARCH>) for hybrid model checkers.]
include SMT (Satisfiability Modulo Theories) solvers: Z3 , Yices2  and dReal ; stochastic, discrete model checkers:  and  STORM ; non-deterministic, discrete model checkers: nuSMV  and SPIN ; and stochastic, non-deterministic hybrid model checkers: ProbReach , SpaceEx  and Uppaal .

Developing tools that ensure quantum software is correct is vital for quantum computers. This will allow quantum processors to eventually be used in safety-critical systems, where assurances about programs are crucial.

The goal of this survey is to introduce the formal verification techniques and tools that have been developed to prevent errors and bugs within quantum programs.
This includes summarising some of the theories that verification tools for quantum programs are based on and investigating implementations of these tools. Future hurdles for verifying complex quantum algorithms and routes for further research are also discussed.

Note that this article is mainly discussing techniques for verifying programs. Verification is important in other areas of computer science, such as communication, security, program equivalence and concurrency.
In this article, discussion will be given on some of these variations. Otherwise, readers are referred to <cit.> for verification in quantum security, to <cit.> for verification in quantum communication, and to <cit.> for verification in concurrent quantum systems.
Finally, a recent survey <cit.> provides an in-depth discussion on lower level verification (circuit equivalence) and details on quantum programming languages. In contrast, our article focuses on designing verification frameworks and how more complex quantum algorithms need to be verified.

The organisation of the paper is as follows.
Section <ref> gives an overview of quantum computing and some background on the fundamentals of model checking and deductive verification.
Section <ref> discusses the various formal verification techniques that have been extended or created to check quantum programs.
Section <ref> considers what is desirable in verifiable quantum programming languages.
Section <ref> discusses the most recent verifiable tools for verifying quantum programs with relation to the topics discussed in the previous section.
Section  gives examples of non-textbook algorithms and details what hurdles need to be overcome to verify them.

§ BACKGROUND

This section introduces the fundamental concepts of quantum computing and the field of formal verification.
Whilst there are many techniques for formal verification, this section focuses on the two most popular ones: model checking and deductive verification.

§.§ Quantum Computing

Nielsen and Chuang's volume <cit.> is the standard textbook for quantum computing, but this section introduces the core ideas that are needed for the rest of the paper. In quantum mechanics, there are four quantum postulates[But only three of them are strictly needed: see “Four Postulates of Quantum Mechanics Are Three”, G. Carcassi et al., Phys. Rev. Lett. 126, 110402, 2021.] that give us the rules and behaviours that make up quantum systems.

Firstly, a quantum system is represented by a Hilbert space (a complex vector space with inner product) often referred to as a state space. A system's state is described by a unit vector within the Hilbert space. A qubit, the simplest quantum computing system, is represented by

\begin{align*}
\ket{\psi} &= \alpha \ket{0} + \beta \ket{1} \\
&= \alpha \begin{pmatrix} 1 \\ 0 \end{pmatrix} + \beta
\begin{pmatrix} 0 \\ 1\end{pmatrix}
\end{align*}

where  $\alpha$ and $\beta$ are complex numbers that satisfy $|\alpha|^2 + |\beta|^2 = 1$. The dual of a vector is represented by $\bra{\psi} = \ket{\psi}^{T}$.

Secondly, the state space of a composite quantum system is represented by the tensor product of the individual quantum systems. So a system with $n$ quantum systems is represented by ${\ket{\psi_1} \otimes \ket{\psi_2} \otimes \dots \otimes \ket{\psi_n}}$.

A 2-qubit system spans a 4-dimensional vector space. This system can represent the Bell state $\frac{1}{\sqrt{2}}(\ket{0}\otimes\ket{0} + \ket{1}\otimes\ket{1}) = \frac{1}{\sqrt{2}}(\ket{00} + \ket{11})$, where the state is represented by the vector $(\frac{1}{\sqrt{2}},0,0,\frac{1}{\sqrt{2}})^T$.

Thirdly, a closed (no interaction with its surrounding environment) quantum system evolves through applications of unitary operators on the quantum state $\ket{\psi}$. A unitary operator $U$ is a (linear) transformation such that its inverse is its adjoint $U^{-1} = U^\dagger$. The state after evolution is $U \ket{\psi}$; we recall that unitary operators are norm-preserving transformations.

Finally, when a quantum system is measured, the quantum state randomly collapses into one of the states in an orthonormal basis $\{\ket{o_1}, \dots, \ket{o_n}\}$. With the quantum state being $\ket{\psi} = \sum_{i=1}^{n} \alpha_i \ket{o_i}$ and $\sum_{i=1}^{n} |\alpha_i|^2=1$, the probability of the state collapsing to $\ket{o_j}$ is $P(o_j) = |\alpha_j|^2$. After measurement, the quantum state is $\frac{\alpha_j}{|\alpha_j|}{\ket{o_j}}$. It should be noted that measurement can be represented by a set of Hermitian operators $M = \{M_j : 0 \leq j \leq n \}$, where $M_j = \ket{o_j}\bra{o_j}$ is the projector over the one-dimensional space spanned by $\ket{o_j}$.

A quantum state is said to be in superposition when it cannot be represented by a single state within an orthonormal basis. I.e. $\ket{\psi}$ is in a superposition in the basis $\{\ket{o_1}, \dots, \ket{o_n}\}$ when $\ket{\psi} \neq \alpha_j \ket{o_j}$ for all $j$.
Two (or more) quantum systems are entangled when the composite quantum state cannot be written as a tensor product of the individual quantum systems.

The Bell state $\frac{1}{\sqrt{2}}(\ket{00} + \ket{11})$ cannot be represented by some $\ket{\psi_1} \otimes \ket{\psi_2}$, whereas $\frac{1}{\sqrt{2}}(\ket{00} + \ket{01}) = \ket{0} \otimes \frac{1}{\sqrt{2}} (\ket{0} + \ket{1})$.

Whilst representation of a quantum system commonly uses the vector notation given above, it is possible to define the system using a density matrix notation. Given a finite ensemble of quantum systems $\{p_i, \ket{\phi_i}\}$ where the probability of the system being in (pure) state $\ket{\phi_i}$ is $p_i$, the system can be represented by $\rho = \sum_i p_i \ket{\phi_i}\bra{\phi_i}$. This representation changes how the postulates are given. For example, the unitary evolution of the system is given by the so-called super-operator $U \rho U^\dagger$, where $U$ is a unitary transformation. The trace of a matrix is the sum of the diagonal elements $tr(A) = \sum_i A_{ii}$ and is used in various aspects when working with density matrices (such as measurement).

§.§ Model Checking and Verification

Verifying software with model checking involves modelling the software through a formal representation. Then desired behaviour is specified through an appropriate logic. Once these two components are created, model checking algorithms can be used to check whether the model follows the specified behaviour. In this section, we study the temporal behaviour of software and systems. Models are created using Kripke structures and behaviours are specified using a temporal logic. More details can be found in .

Kripke structures model software or systems by describing transitions between states in a similar way to finite state machines. But Kripke structures also model properties that hold in each state.
Formally, a Kripke structure is given by a tuple $M = (S, S_0, R, L)$ where

* $S$ is a finite set of states;

* $S_0 \subseteq S$ is the initial state;

* $R \subseteq S \times S$ is a total transition relation, where for all $s \in S$, there exists $s' \in S$ such that $(s, s') \in R$;

* $L: S \rightarrow 2^{AP}$ is a labelling function that gives the set of propositions ($p \in AP$) that hold within a given state.

A common type of logic used to specify behaviour is temporal logic, which can be used to describe what propositions may hold about the system over time. Examples of temporal logics include Linear Temporal Logic (LTL) , Computation Tree Logic (CTL)  and the $\mu$-calculus .
The definition of CTL is given and briefly studied as it will be useful for understanding Section <ref>.
Terms in CTL are given by state formulae, $\theta$, and temporal operators, $T$, that only exist bound with path quantifier. These formulae are defined inductively by

\begin{align*}
&\theta ::= p
\text{ || }\lnot \theta
\text{ || } \theta \lor \theta
\text{ || } \textbf{E} T
\text{ || } \textbf{A} T
\\
& T ::= \textbf{X} \theta
\text{ || } \textbf{F} \theta
\text{ || } \textbf{G} \theta
\text{ || } \theta \textbf{U} \theta {,}
\end{align*}

where $p \in AP$ is an atomic proposition in the model. The terms X (“next”), F (“eventually”), G (“always”) and  U (“until”) denote basic temporal operations. The operators F and G are obtained from U simply as $\textbf{F}\theta = \textit{true}\, \textbf{U}\, \theta$ and $\textbf{G}\theta = \neg \textbf{F} \neg\theta $, where $\textit{true}$ is the atomic proposition true in all states. The terms A (for all paths) and E (there exists a path) are path quantifiers. It should be noted that CTL can be described with a subset of temporal and logical expressions as it is possible to create formulae from different terms. For example, the statements "there is no path such that eventually $\theta$ holds" and "for all paths $\lnot \theta$ always holds" are equivalent and specified in CTL by $\lnot \textbf{EF} \theta = \textbf{AG} (\lnot \theta)$.

Figure <ref> gives a model and the relative computation tree is given in Figure <ref> with an example CTL operation.

The Kripke structure starts in the state s_0, which can only transition to state s_1. When in the s_1, the state can either loop and stay in s_1 or transition to the state s_2. Finally, when in s_2, the state can stay there by looping or transition to s_0.

An example of a Kripke structure with $S = \{s_0, s_1, s_2\}$.

A state transition tree of the previous figure. The root of the tree is s_0 and it transitions downwards to the valid states it can reach. The root and its child (s_1) are highlighted in yellow as the first proposition holds in those states. Then the right child (s_2) and its right child (s_2) are highlighted in blue as the second proposition holds in those states. All other nodes are not highlighted as these do not adhere to the CTL formula.

A computation tree for the automata given in Figure <ref> 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$.

The model checking problem is to find all valid states that satisfy a temporal logic formula. (Alternatively, one could just ask whether the formula is true in the initial state.) Given $M$ (a Kripke structure) and $\theta$ (a temporal logic formula), then find all $s \in S$ such that $M$ and $s$ models $\theta$, the semantics of which is denoted by $M, s \models \theta$. To apply this to the example in Figure <ref>, then ${M, s_2 \models p \iff p \in L(s_2)}$.

A reason for choosing model checking as a verification technique is that it efficiently searches over all possible states of a Kripke structure in a completely automated way.
However, the main issue of model checking is the state explosion problem <cit.>.
Due to the design of the Kripke structure, an increase in the size of the system can increase the number of states in the structure massively. This can make it very difficult for the system to be verified quickly.
Over the last few decades a number of methods have been developed to address the state explosion problem. For example, bounded model checking (BMC) <cit.> only considers finite computation trees, effectively meaning that the system is only checked up to a certain point in time.

Another technique is CounterExample-Guided Abstraction Refinement (CEGAR) <cit.>, which starts by creating an abstract model that simulates the original (concrete) model. The abstract system is then model checked against a given universally path-quantified temporal logic property. If the property is satisfied then we are done, since the abstract model encompasses all the possible behaviours of the concrete model. If instead a counterexample to the property is returned, then this is compared in the concrete model: if it is an actual counterexample, then the model checking fails since this is a “real” bug of the concrete model. Otherwise, the counterexample is spurious and the abstraction is refined so that the counterexample no longer fails inside the abstraction. The newly-obtained abstraction is then model checked again – the process is repeated until the property is either verified or a concrete counterexample is found <cit.>.

§.§ Deductive Verification

For a full review of deductive verification the reader is referred to, <cit.>.
Unlike model checking, which exhaustively explores the possible states that software can be in, deductive verification formally verifies programs through logical inference. Further model checking can ensure certain properties about software automatically, whereas deductive verification can be used to verify complex properties about programs in a way that is understandable by humans. For example, a subroutine can be shown to always return a certain result no matter the input by using deductive verification.
The Floyd-Hoare logic <cit.> is studied below as an example and will be useful later.

A program is given some preconditions, assumptions and rules that can be used for verification, and postconditions, goals or requirements to meet after the program has run with the given preconditions. A program is valid if the postconditions can be inferred from the preconditions given using inference rules.
This is often written in the form of a Hoare triple denoted by $\{P\}S\{Q\}$, where $P$ is a precondition, $Q$ is a postcondition and $S$ is a program statement. A Hoare triple is considered valid if a sequence of inference rules can be used to generate it. The basic inference rules are given in Equation <ref>.

\begin{align}
\begin{aligned}
{\assert{P} \textbf{ skip }\assert{P}}
&\text{ (Skip)}\\
{\assert{P[a/x]} x:=a \assert{P}}
&\text{ (Assign)}\\
&\frac{\assert{P} S_1 \assert{Q}, \assert{Q} S_2 \assert{R}}
{\assert{P} S_1; S_2 \assert{R}}
&\text{ (Composition)} \\
&\frac{\hoare{b \land P}{S_1}{Q}, \hoare{\lnot b \land P}{S_2}{Q}}
{\hoare{P}{\textbf{if }b\textbf{ then }S_1\textbf{ else }S_2}{Q}}
&\text{ (Conditional)}\\
&\frac{\hoare{P \land b}{S}{P}}
{\hoare{P}{\textbf{while }b\textbf{ do } S}{\lnot b \land P}}
&\text{ (While)}\\
&\frac{P_2 \rightarrow P_1, \hoare{P_2}{S}{Q_2}, Q_2 \rightarrow Q_1}
&\text{ (Consequence)}
\end{aligned}
\label{eq:hoarerules}
\end{align}

The proof of a program or system can be created from the Hoare triple and the use of inference rules. These proofs are converted into proof obligations, which are mathematical formulas that are checked using one of a variety of software tools.
The most common tools for software verification are theorem provers and SMT (Satisfiability Modulo Theory) solvers. Theorem provers <cit.> allow programmers to write the obligations that are to be met in a completely formal environment. Then lemmas and theorems about these obligations can be derived from definitions created within the tool. Normally, the process of proving an obligation is interactive and so the programmer will write the proof with assistance from the tool.

In comparison, SMT solvers  convert obligations into logical formulas over a theory, such as, the natural numbers, rationals and bit vectors. Alongside a statement the user wishes to assert, the solver can automatically check if the formulas are valid. If not, the solver can provide a counterexample.

Deductive verification still suffers from scalability issues similar to model checking.
Unlike model checking, it requires programmers to have a deeper understanding of why the obligations are correct. This is both an advantage and a setback, since it can take a long time to prove complex obligations that could be solved automatically using model checking. However, it is possible to create human-readable proofs as to why a program is correct.

For examples of some of the most used theorem provers, the reader is referred to <cit.>; an introduction to SMT solvers is given in <cit.> and a deeper study is given in .

§ FORMAL QUANTUM VERIFICATION METHODS

This section aims to introduce the theoretical ideas that have been used in pursuit of the verification of quantum programs. While this section covers some theories, it is not a complete list. Further theories include quantum Markov chains <cit.> and quantum automata <cit.>, which are given a brief introduction in a previous survey <cit.> with further references therein.

§.§ Quantum Weakest Precondition

In deterministic programming, the weakest precondition <cit.> gives a method of transforming the problem of checking whether a program is valid in Hoare logic into a problem of determining whether a precondition implies the said weakest precondition.
More formally for deterministic programs, given a program $S$ and a predicate postcondition $Q$, then the weakest precondition $\text{wp}(S)(Q)$ is the precondition to $S$ such that for all preconditions $P$ with $\{P\}S\{Q\}$, then ${P\implies \text{wp}(S)(Q)}$.

Whilst a probabilistic version of the Hoare logic has been developed and can be used as a means to verify quantum programs <cit.>, D'Hondt and Panangaden <cit.> demonstrated one can develop a quantum Hoare-style logic using density matrices. This then allows for the notion of a quantum weakest precondition.
The difference in definition is that now the program $S$ is a quantum program, the predicate $Q$ is a Hermitian operator (which is positive and has bounded eigenvalues) and valid predicate preconditions $P$ must satisfy $\text{tr}(P\rho) \leq \text{tr}(Q (S\rho))$ for all density matrices $\rho$. Thus, the quantum weakest precondition $\text{wp}(S)(Q)$ is defined such that for all valid preconditions $P$, $\text{tr}(P\rho) \leq \text{tr}(\text{wp}(S)(Q)\rho))$ for all density matrices $\rho$.

With this notion, it is possible to change the verification problem of quantum programs to that of calculating quantum preconditions. In a sense, the quantum weakest precondition gives the most “general” precondition for a postcondition, meaning that as long as we have a “specific” precondition we can always reach the same postcondition as the “general” precondition.
The quantum weakest precondition is a concept that can see usage in different verification systems depending on the language and design used. In Section , we will see an example of its usage.

§.§ Quantum Hoare Logic

Ying <cit.> has been developing the Quantum Hoare Logic (QHL) over the last decade, as an extension of the standard Floyd-Hoare logic. Introduced in his original work, the classical while-language is extended to a quantum version and the Floyd-Hoare logic is amended to verify the extension. The quantum-while language is:

\begin{align*}
S ::= & \textbf{ skip}
\text{ | } q := 0
\text{ | } \bar{q} := U \bar{q}
\text{ | } S_1 ; S_2
\text{ | } \textbf{measure } M[\bar{q}] : \bar{S}
\text{ | } \textbf{while } M[\bar{q}] = 1 \textbf{ do } S.
\end{align*}

The commands do the following operations: skip does nothing, ${q := 0}$ initialises a qubit, $\bar{q} :=U \bar{q}$ performs a unitary operation on a number of qubits, ${S_1 ; S_2}$ is composition of statements, $\textbf{measure } M[\bar{q}] : \bar{S}$ measures some qubits and performs a program from $\bar{S}$ depending on the result and $\textbf{while } M[\bar{q}] = 1 \textbf{ do } S$ performs $S$ until a "false" measurement is read.

The quantum-while language stands out because it does not define programs in terms of describing quantum circuits. This allows for an imperative approach for writing quantum programs, rather than the very low-level idea of constructing a circuit. Another feature to highlight is the use of measurement within the language. The measure command replaces the classical if statement and the while statement requires measurement on a set of qubits during each iteration.

The Quantum Hoare Logic then extends the Hoare triple $\{P\} S\{Q\}$ to handle the quantum-while language.
Inference rules can be used to create Hoare triples for quantum programs depending on the statement. Beyond that, the notion of weakest precondition can be used to generate valid Hoare triples. If a desired postcondition is wanted, then rules can be used to find the weakest precondition for a program.
The correctness of evaluating the Quantum Hoare Logic on a program and the condition that evaluation terminates (notions of partial and total correctness respectively) are given in .

Work has continued on this logic over the last decade to further improve it and create an implementation, as will be seen in Section <ref>.
As an example of an improvement to be made on the grammar, it is clear to see that there is no classical functionality defined. This prevents some quantum algorithms, such as Shor's algorithm <cit.>, being fully implemented within the quantum-while language. A recent work <cit.> has extended the quantum-while language to include classical variables and the logic has been reworked to show the extension is verifiable.
Another version of Quantum Hoare logic has been proposed in , which is not designed around the usage of weakest precondition. Further, this other version verifies Selinger's QPL , a quantum programming language based on flowcharts and featuring classical bits as well as if statements.

Here we give an example of using Quantum Hoare logic and the quantum weakest precondition to verify Deutsch's algorithm. Given $f:\{0,1\} \rightarrow \{0,1\}$, recall that Deutsch's algorithm determines the value of $f(0) \oplus f(1)$ with a single evaluation of $f$. It should be noted that this example does not make use of an ancillary qubit for the sake of simplicity. We begin by writing Deutsch's algorithm in the quantum-while language:

\begin{equation*}
\textit{Deutsch}=[q:=0; q:=Hq; q:=O_fq; q:=Hq; \textbf{measure } M[q] : \textbf{skip}, \textbf{skip}]
\end{equation*}

Here, $H$ is the single-qubit Hadamard gate and $O_f$ is the quantum oracle defined by the matrix

\begin{equation*}\begin{pmatrix} (-1)^{f(0)} & 0 \\ 0 & (-1)^{f(1)} \end{pmatrix}\end{equation*}

Further, the measurement operators $M$ consist of measurements on the computational basis:

\begin{equation*}
\Big\{
M_0 = \begin{pmatrix} 1 & 0 \\ 0 & 0 \end{pmatrix},
M_1 = \begin{pmatrix} 0 & 0 \\ 0 & 1 \end{pmatrix}
\Big\}
\end{equation*}

The result of receiving either measurement outcome in the measurement statement is to simply skip. Using the definition of the weakest precondition for Quantum Hoare Logic, we wish to find the weakest precondition of the postcondition $\textit{Post}=(1-f(0)\oplus f(1))\ket{0}\bra{0} + (f(0)\oplus f(1)) \ket{1}\bra{1}$. This postcondition states that $q$ should be in the appropriate state depending on the value of $f(0) \oplus f(1)$. Here, we will calculate the weakest precondition of the measurement statement and leave the rest of the calculation for the Deutsch program in Appendix <ref>.

From Proposition 7.1 in <cit.>, we have that

\begin{equation*}
wp.(\textbf{measure } M[\bar{q}]:\bar{S}).P := \sum_m M^\dagger_m (wp.(S_m).P) M_m
\end{equation*}

and so for our case, we have

\begin{equation*}
wp.(\textbf{measure } M[q]:\textbf{skip},\textbf{skip}).\textit{Post} := M^\dagger_0 (wp.(\textbf{skip}).\textit{Post}) M_0 + M^\dagger_1 (wp.(\textbf{skip}).\textit{Post}) M_1.
\end{equation*}

Further to this, the weakest precondition of skip is simply $wp.(\textbf{skip}).P = P$. Thus, we have that

\begin{align*}
wp.(\textbf{measure } M[q]:\textbf{skip},\textbf{skip}).\textit{Post} & := M^\dagger_0 (\textit{Post}) M_0 + M^\dagger_1 (\textit{Post}) M_1 \\
& = (1-f(0)\oplus f(1))\ket{0}\bra{0} + (f(0)\oplus f(1)) \ket{1}\bra{1}\\
& = \textit{Post}
\end{align*}

giving the Hoare triple $\{\textit{Post}\} \textbf{measure } M[q]:\textbf{skip},\textbf{skip} \{\textit{Post}\}$.

Following the rules for quantum weakest precondition of the Quantum Hoare Logic,
the resulting Hoare triple for the entire program is $\{ I \} \textit{Deutsch} \{ \textit{Post} \}$, where $I$ is the single qubit identity operator. This weakest precondition means that Deutsch can have any valid precondition and it will always produce the correct result.

§.§ Quantum Computation Tree Logic

Various notions of extending Computation Tree Logic (CTL) to the quantum case have been studied, and implemented into model checking algorithms. For example, <cit.> investigated a quantum extension of probabilistic CTL (PCTL). Recently, in <cit.> the authors created a different extension of CTL that uses the concept of fidelity (which measures how much a density matrix state is changed after being acted on by a super-operator). Other temporal logics have been studied both as quantum extensions of the original logic  and how temporal logics can model behaviour in quantum systems  (see  for a survey on model checking quantum systems). In this section, the notion of quantum computation tree logic given in <cit.> is presented.

The Quantum Computation Tree Logic (QCTL) is a temporal logic used to reason about the behaviour of a quantum Kripke structure. This type of structure is made of states and relations between these states, where states combine quantum states and variable assignments.
The logic is created by combining the decidable fragment of the exogenous quantum propositional logic (dEQPL)  with the classical CTL used in model checking.
In <cit.>, it is shown that QCTL is sound and (weakly) complete. Further, an algorithm was developed that checks if a QCTL formula is satisfiable by extending an algorithm used for model checking CTL. The grammar for QCTL is:

\begin{align*}
\theta & ::= \gamma
\text{ | } (\theta \sqsupset \theta)
\text{ | }  \textbf{EX}\theta
\text{ | }  \textbf{AF}\theta
\text{ | }  \textbf{E}[\theta\textbf{U}\theta]\\
& \text{where $\gamma$ is a dEQPL formula.}
\end{align*}

The $\sqsupset$ symbol denotes quantum implies and is different from the classical version. Note that QCTL uses a subset of the temporal logic operations from CTL and the other temporal logics can be derived from this subset.

Unlike some of the other formal methods discussed in this section, this logic would be used in a similar way to the model checking described in Section <ref>. This would involve converting properties of a quantum program or circuit into the QCTL language.
By providing a specification for the program, the QCTL formula can be checked for model satisfiability using the algorithm given in <cit.>. The other QCTLs introduced at the start of this section <cit.> found use in model checking quantum Markov chains. We now give two examples of QCTL <cit.> formulae.

Denote $\Box \alpha $ as $(\textstyle{\int} \alpha) = 1$. This is a dEQPL formula that states a classical formula $\alpha$ holds with probability 1 after measuring all qubits. The following formula is used in  as the formula for verifying a single bit version of the BB84 protocol <cit.>:

\begin{equation*}
(\Box (b_A \Leftrightarrow b_B)) \sqsupset \textbf{A}[(\boxminus (\Box e)) \textbf{U} ((\Box e) \sqcap ((\Box k) \equiv (\textstyle{\int} m = 1)))] .
\end{equation*}

The formula means "If Alice and Bob are in the same basis $(\Box (b_A \Leftrightarrow b_B))$, then down all (quantum) paths the protocol has not ended ($\boxminus (\Box e))$) until it has ended $(\Box e)$ and the generated key is equal to the value of the qubit used ($(\Box k) \equiv (\textstyle{\int} m = 1)$)".

As a second example, consider Deutsch's algorithm. Denote $b = f(0) \oplus f(1)$ as a classical bit. Further, use $m$ as a classical bit to say when the algorithm has performed the measurement operation and let $q$ denote the qubit used for the algorithm. We then have the following formula:

\begin{equation*}
\textbf{A}[(\boxminus (\Box m)) \textbf{U} ((\Box m) \sqcap ((\Box b) \equiv (\textstyle{\int} q = 1)))] .
\end{equation*}

The formula reads "for all (quantum) paths ($\textbf{A}$), the qubit is not measured ($\boxminus (\Box m)$) until it is measured ($\Box m$) and the measured qubit gives us the correct result with certainty (${(\Box b) \equiv (\textstyle{\int} q = 1)}$)".

§.§ Path Sums

Path sums are a representation of unitary operators in terms of a summation of exponential polynomials with different quantum states. This representation was used in <cit.> to show the equivalence of quantum programs.
Equation (<ref>) shows a path sum represented as a unitary operator. Note that $\mathbf{x} = (x_1, \dots , x_n)$ is a collection of Boolean variables or constants (the input signature), $P$ is a (phase) polynomial with inputs $\mathbf{x}$ and $\mathbf{y}$, and $f : \mathbb{Z}_2^n \times \mathbb{Z}_2^m \rightarrow \mathbb{Z}_2^n$ is a multi-variable Boolean function (the output signature):

\begin{equation} \label{eq:psums}
U : \ket{\mathbf{x}} \rightarrow \frac{1}{\sqrt{2^m}} \sum_{\mathbf{y} \in \mathbb{Z}_2^m} e^{2 \pi i P(\mathbf{x},\mathbf{y})} \ket{f(\mathbf{x},\mathbf{y})}.
\end{equation}

Path sums are used to represent the semantics of Clifford$+R_k$ circuits[See Appendix <ref> for information on Clifford circuits.] for a fixed $k$.
Reduction rules can be applied to decrease the size of the circuit and so it is easy to check the equivalence of quantum circuits.
Experiments in <cit.> have shown that Clifford$+T$ circuits with a large number of qubits and gates can be efficiently and automatically verified.
This gives a useful representation to efficiently verify quantum circuits. However, it will require support through a translation tool to be used to verify circuits written in a high-level programming language, which could include classical components.

The path sum representation of the Pauli gates are listed below:

\begin{align*}
X & : \ket{x} \rightarrow \ket{1-x} \\
Y & : \ket{x} \rightarrow e^{2\pi i \frac{(2x + 1)}{4}}\ket{1-x} \\
Z & : \ket{x} \rightarrow e^{2\pi i \frac{x}{2}}\ket{x}
\end{align*}

§.§ The ZX-Calculus

The ZX-calculus <cit.> can be utilised as an alternate form of verification. The ZX-calculus is a graphical tool designed to convert quantum circuits into a graphical model and back again (but not all graphs are quantum circuits). These graphical models or networks model wires in the form of edges and some operations in the form of vertices.

The ZX-calculus consists of three main vertices: the Hadamard node, green spiders and red spiders (shown in Figure ). Using a set of rewrite rules, it is possible to add or remove various vertices.
This allows the creation of optimised circuits and comparison between circuits.

[] (0) at (0.5, 15.25) ;
[] (1) at (0.5, 16.25) ;
[style=had] (2) at (0.5, 15.75) ;

(0.center) to (2);
(2) to (1.center);

\begin{equation*}
\frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix}
\end{equation*}

[style=gn] (31) at (4.25, 13.75) $\alpha$;
[] (32) at (4.25, 13.25) ;
[] (33) at (4.25, 14.25) ;

(32.center) to (31);
(31) to (33.center);

\begin{equation*}
\begin{pmatrix} 1 & 0 \\ 0 & e^{i\alpha} \end{pmatrix}
\end{equation*}

[style=rn] (31) at (4.25, 13.75) $\alpha$;
[] (32) at (4.25, 13.25) ;
[] (33) at (4.25, 14.25) ;

(32.center) to (31);
(31) to (33.center);

\begin{equation*}
e^{\frac{i\alpha}{2}}\begin{pmatrix} \cos{\frac{\alpha}{2}} & -i\sin{\frac{\alpha}{2}} \\
-i\sin{\frac{\alpha}{2}} & \cos{\frac{\alpha}{2}} \end{pmatrix}
\end{equation*}

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.
The Hadamard node is a yellow square. The green spider node is a green circle containing an alpha symbol inside it. Similarly, the red spider node is a red circle with the same alpha symbol. All the nodes have two wires (lines) entering from the northern and southern points of the nodes.

An example of a simple ZX-graph and the use of rewrite rules is given in Appendix .

While this a useful tool for this purpose, it is an example in highlighting the difference in what the other tools described are trying to achieve. The ZX-calculus is useful for optimising circuits and showing the equivalence of circuits. It can be used to verify properties of simple circuits, such as the teleportation protocol <cit.>, however it can not be used to prove complex properties about the execution of circuits.

§ DESIGN OF VERIFICATION FRAMEWORKS AND QUANTUM PROGRAMMING LANGUAGES

In this section, several trade-offs and properties that are desired from a programming language for quantum verification are given. Whilst the trade-offs are similar to what classical theorem provers need to consider, different requirements need to be met for the language due to the nature of quantum computation. These criteria will later be used to highlight the differences of the available verification frameworks for quantum programming.

§.§ Trade-offs

This concerns the environment in which the programmer creates their programs. There are a few options available when considering this. Firstly, the language could be embedded within an available theorem prover. This gives the benefits of the host language, as well as access to libraries and community support. Further, someone familiar with the environment would be able to pick up the language fairly easily. However, embedding within a theorem prover does mean that the quantum verifier also suffers from the limitations of the said theorem prover.

An alternative is to create a new environment dedicated to the verification of quantum programs from scratch. This gives more freedom in being able to meet the specification the designer creates. On the downside, it may take longer to develop than other methods. It will take longer to fully build a dedicated tool for the verification of programs versus building off or extending a well-known tool.

Another approach is to extend a quantum programming language with a verification framework. This would allow both programs to be verified and executable on a simulator or quantum hardware. However, the choice of language needs to be considered and the framework would need to be updated whenever the underlying language gets updated.

Interactive vs Automated
Here, one needs to consider whether the user should interact with the proofs they are constructing and how much should a tool automate the process of generating the proof. One can design a fully interactive prover, a fully automated prover or a mix between the two.

If the framework is designed to be interactive, then it may take more man-hours to construct proofs. However, this brings the benefit of the user obtaining a better understanding as to how a program is (or is not) valid.
On the other hand, an automated-focused framework could only require the push of a button to prove programs, possibly leaving the user in the dark as to why the program is correct.

The size of systems requiring verification are a factor in which type of tool to use. A large system might not be suitable for an interactive approach requiring the use of an automated approach. In , the authors highlight the use of model checkers and SMT solvers for the verification of avionics systems. The case studies provided contain systems with reachable state spaces of up to $1.5 \times 10^{37}$ states.

Executability and Separability
Another property to consider is what should be executable within the framework. This will depend on the environment chosen for the framework and how mixed the specification is with the programs created.
If a program is to be run on quantum hardware, the specification and verification of a program needs to be separated from its definition. This is because the verification of quantum programs occurs classically (at least for now) whereas programs would be executed on quantum hardware. This puts the separation between the definition and execution of programs and proofs as a high priority.

Running programs on a simulator is quite different. The reason for running a quantum program on a simulator is to check the outcomes of the program. With a verification framework, this becomes unnecessary. Thus, the separation between program and proof could be avoided if this approach is taken.

§.§ Limitations of Quantum Programs

Due to the difference in nature between quantum and classical computing, quantum programming languages have different requirements to classical ones. In <cit.> a discussion on a number of bugs to avoid when implementing a quantum programming language is given. Here a few of the ideas presented in <cit.> are discussed as are some other thoughts. The paper goes into more details on common bugs that programmers may create due to human error, but this is omitted.

One of the key properties to meet is that the no-cloning theorem <cit.> is adhered to. The rules that quantum mechanics follow do not allow for the copying of arbitrary quantum data. Therefore, any quantum programming language should have inbuilt functionality to forbid (perfect) cloning. For example, if programs and proofs are mixed within the language, then the no-cloning theorem can be built within the language.

Limited Classical Functionality
A useful approach of designing a quantum computer is by having a classical computer being able to access a small quantum processor, known as quantum random access memory (QRAM), in a similar way to a graphics processing unit (GPU) <cit.>.
The quantum part of the computer should perform purely quantum operations, having very little classical functionality within it. Because of this restriction, quantum programming languages need to be designed so that there is very limited classical functionality within the language as to avoid affecting the quantum system.

It should be noted though that there are some nice features that can come with having classical functionality. For instance, oracles implement classical functions into a quantum circuit and having classical functionality would allow for easy implementation of oracles. Silq <cit.> implements this in an easy-to-do way. Striking the right balance of how much classical functionality to have is therefore very important to consider.

Depending on the amount of classical functionality, there are two ways to verify a program with quantum and classical components. One method is to combine a quantum and classical verifier with each handling the verification of separate parts of the program. The alternative would be for the verifier to have suitable logic to handle classical and quantum functionality together.

Ancillary Cleaning
Ancillaries are qubits that are introduced into the system in an initial state, used for a computation temporarily and then returned to their initial state. This process of returning the ancillary to its initial state is known as cleaning and is important for programmers or language designers to take into account. In classical computation, ancillary bits can be easily removed automatically by the processor through garbage collection, since classical bits can be discarded without affecting the state of the program.
However, if ancillary qubits are not cleaned, there is the potential for measurement outcomes to be affected due to entanglement between the main qubits and the ancillary ones. It should be decided by the designers whether programs should automatically uncompute ancillaries or if the programmer should perform this task.

A key feature in the programming language Silq <cit.> is that ancillaries are automatically uncomputated. Whether this feature will be seen in future verifiable programming languages is uncertain. From a verification perspective it would be advantageous to verify properties of ancillary qubits. For example, one such property is verifying that an ancillary qubit returns to its initial state so that it can be removed from the computation.

Algorithm Milestones
Designers of quantum languages often show the capabilities of their language by implementing a quantum algorithm. One should think of each algorithm as a milestone that should be reached. The lowest milestone to reach is being able to implement the Deutsch-Jozsa algorithm <cit.> or the quantum teleportation protocol  as these are fairly well-known algorithms. The next milestone would be to write either Grover's <cit.> or the Quantum Phase Estimation algorithm (many of these mentioned can be found in <cit.>).
This is because both involve some form of iteration and are slightly more complex than the Deutsch-Jozsa  and teleportation algorithms. The hardest algorithms to implement would be some of the 7 algorithms implemented in Quipper <cit.>, which includes quantum walks on Binary Welded Trees <cit.> and the Ground State Estimation algorithm <cit.>.

For verifiable quantum programming languages, it is also necessary to be able to prove these programs run correctly. Many quantum programming languages are already able to implement several of the common “textbook” algorithms and a variety of algorithms in other fields, such as quantum chemistry <cit.>. So far, verifiable languages have only been able to prove about "textbook" algorithms. Whether they can prove facts about more advanced algorithms is yet to be seen. In Section  we discuss two non-textbook algorithms and their challenges to verification.

§ VERIFIABLE QUANTUM PROGRAMMING LANGUAGES

Here various quantum programming languages that can verify programs are discussed, highlighting their trade-offs, where they excel and their limitations. At the end of this section, other quantum verification tools, whose focus is not on the formal verification of programs, are briefly discussed.

§.§ SQIR (and QWire)

The languages QWire <cit.>
and SQIR (Small Quantum Intermediate Representation) <cit.>
are domain specific languages built in the Coq interactive theorem prover <cit.>.
QWire was one of the first quantum programming languages to be released with verifiable programs, while SQIR is a more recent language that has various improvements over QWire. These improvements include shorter code, better handling of ill-typed programs and the separation of semantics for unitary and non-unitary (measurement) operations.

SQIR uses the various functionalities of Coq to act as a proof assistant for writing proofs about quantum programs. In order to verify a program, firstly the program is defined using a dedicated type, with qubits being referred to by a numerical value. Programs can be defined by one of two types:
which only contains unitary operations; or
which allows for measurement.
Classical subroutines cannot be performed within a SQIR program, but it is possible to generate circuits using classical parameters.

Theorems can then be conjectured about the program. Unitary SQIR uses state vectors as part of the semantics, whereas full SQIR extends this to density matrices. The user proves the theorem with the assistance of the Coq framework.
This format separates programs from how they are specified/proved.
No-cloning is satisfied through the use of unitary gates and measurement being the only operations allowed in the language.

An example program and proof can be seen in Figure <ref>. Whilst the example given is quite trivial, it is possible to make generalisations about what can be proven. The creators of SQIR have already proven some properties about Grover's algorithm, notably the probability of measuring a marked element after $T$ steps being $\sin^2((2T+1) \arcsin(\sqrt{k/2^n}))$ (where $n$ is the number of qubits and $k$ is the number of marked elements).

Definition Program : base_ucom 2 := H 0; X 0; CNOT 0 1; X 0.

Local Open Scope R_scope.

Definition xor_state : Matrix (2^2) (1^2) : =
1/√(2) .* (|0,1> .+ |1, 0>).

Theorem Prog_Correct: uc_eval Program x (|0,0>) = xor_state.
unfold Program; simpl.
unfold xor_state; simpl.
autorewrite with eval_db; simpl; try lia.

The SQIR program has two definitions and a theorem. The definitions are Program, which describes the two qubit quantum circuit that is being used, and xor-state, which defines the expected output state. The theorem, Prog-Correct, says that if the Program evaluates two qubits in the zero state, then the resulting state is the xor-state. The theorem also has a proof that this result actually hold.
A simple program and proof written in SQIR, which transforms the state $\ket{00}$ into $\frac{1}{\sqrt{2}}(\ket{01} + \ket{10})$.

Coq requires interaction from the user for theorem proving, but there is some automation when reducing matrices as seen in the ${solve\_matrix}$ function given in Figure  (solve_matrix is a tactic that attempts to simplify a matrix equality using a variety of sub-tactics).
Further, SQIR benefits from a number of gates already implemented and verified within the language.
With its capabilities, SQIR has been able to prove properties about most textbook algorithms, including Grover's, the Quantum Phase Estimation and Shor's algorithms.

The key issue that may hinder SQIR is that circuits require a predefined number of qubits. Should ancillary qubits be required in the circuit, the user must define these at the start, rather than introducing them when required.

§.§ QHLProver

The Quantum Hoare Logic, as described previously in Section <ref>, has been implemented into the Isabelle/HOS proofing tool <cit.>. This implementation uses a slightly simpler version of the quantum-while language, omitting the initialisation term $q:=0$.

A full documentation of the implementation is available in the Isabelle Archive of Formal Proofs (AFP) <cit.>. This implementation is referred to as QHLProver. By using Isabelle, verification is not fully automated, but some automation is used to make manual proving easier when handling complex matrices, which are used to define gates and oracles.
An example can be seen in Figure <ref>, showing how a program is validated within the Isabelle framework.

An Isabelle theorem titled prog-partial-correct. This theorem states the partial correctness of a CNOT operation with initial qubit state |10> evaluating to the qubit state |11>. This is proven using the lemmas described in the caption and the "by auto" command.
Documentation of a simple program that implements a single CNOT gate and checks that the state $\ket{10}$ is transformed to $\ket{11}$.
The lemmas qp-pre and qp-post prove that the predicates are valid, well-com-cnot confirms that the program is a valid and prog-partial-deduct proves the deduction.
It would be possible to prove more general properties about CNOT, such as its effect on a general quantum state, but this requires experience with Isabelle and the QHLProver library. The full Isabelle theory file for this example is available in this repository:

QHLProver is similar to SQIR in a few ways. The way programs are proved is akin to that of Coq, where programs, states
and density matrices
are defined and then theorems can be conjectured about them. It also suffers the flaw of SQIR where programs require a predefined number of qubits and so ancillary qubits need to be defined at the start of computation.

Programs are written using a specific type (com), which encodes the terms of quantum-while, and the predicates used within the pre- and post-conditions are density matrices. These all need to be verified for a specific triple to be correct as seen in Figure <ref>.

Unlike SQIR, which defines programs as quantum circuits, QHLProver uses an extension of the quantum-while language to define programs. Whilst there is no theory written for no-cloning within the documentation, no-cloning is adhered to due to the simple grammar that only allows for unitary operations and measurement.

As mentioned previously, there is no classical functionality in the quantum-while language and this is reflected within the Isabelle implementation. Classical parameters are used to extend gates to operate on a subset of qubits. Constructing oracles for different algorithms is done by writing functions defined in terms of natural numbers to booleans, which are then used to create a complex matrix from the matrix indexes.

QHLProver suffers from a lack of implemented and verified logic gates. Currently, the language implements the Pauli gates, Hadamard gates and some gates used within Grover's algorithm. Out of the common quantum gates, only the Hadamard gate is verified. This makes it difficult to create new programs as the user must verify simple gates (such as CNOT).

§.§ Isabelle Marries Dirac

A recent work <cit.> provides another instance of verified quantum computing using the Isabelle theorem prover. Unlike QHLProver's use of the quantum-while language and Hoare logic, Isabelle Marries Dirac (IMD)
uses the standard matrix formalisation approach of quantum computing to prove properties about algorithms and protocols. Because of this, IMD is closer to a verifiable mathematical library, rather than a verifiable programming language. An example can be seen in Figure .

The circuit circ is defined as a complex matrix. It is defined as a NOT gate on the first qubit followed by a CNOT gate. This is then used in the lemma circ-result, which says that circ = |11>. This is proven using the definition of circ, an assertion that |0>x|0> = |00> and the evolution of the quantum state (from |00> to |10> to |11>).
Documentation of a simple CNOT program similar to that of QHLProver. The circuit performs a NOT-gate on the first qubit and then the CNOT gate with the first qubit as control. The lemma circ-result uses the circuit definition and how the state evolves through each transition to show the resulting state.
The full Isabelle theory file for this example is available in this repository: <https://github.com/marco-lewis/IMD_CNOT>.

Firstly, matrices are defined to have a fixed size, whether through a variable $n$ or a value. Ancillaries are needed to be defined by the user and taken into account when defining matrices.
Fortunately, programs in IMD are defined using the dot and Kronecker product of matrices. This makes it easier to add in ancillary definitions.

Since IMD is a mathematical library, classical functionality is possible so long as proofs are developed in the Isabelle theorem prover. Oracles are constructed in a similar way to QHLProver, where the matrix value at an index is determined by a function with indexes as input.
Various properties about measurement are implemented within the library such as the probability that a given outcome is certain.
It is possible to prove properties about not just standard algorithms (the Deutsch-Jozsa algorithm) but also different quantum information theoretic results such as quantum teleportation. More results are discussed in <cit.>.

Further, Echenim and Mhalla <cit.> have used IMD and density matrices from QHLProver to prove properties about projective measurements (measuring qubits in a basis different from the computational basis $\{\ket{0}, \ket{1}\}$). They continued to develop more information theory results by proving the CHSH inequality <cit.>.
As can be seen, the featured libraries have more proofs relating to mathematical concepts of quantum computing that cannot be implemented in a programming language.
The documentation for IMD and the extension <cit.> are available in the Archive of Formal Proofs <cit.>.

§.§ QBricks

QBricks <cit.>
is a circuit-based verifiable quantum programming language built in the Why3 framework.
The language is purposefully built so that the writing of programs is separated from the specification to be proved about the program.
Programs are written using QBricks-DSL, which is a domain specific language, and the specifications are written in QBricks-SPEC. Figure  gives the specification and definition for the oracle used in the Deutsch-Jozsa algorithm.[At the time of writing, a tutorial article is being written by the team.]

val function deutsch_oracle (f: bitvec -> int)(n:int): circuit
requires(not (constant_bin f n)) -> balanced_bin f n
ensureswidth result = n+1
ensuresforall x: bitvec. forall  y: matrix complex.  is_a_ket_l y 1 ->
path_sem result (kronecker (bv_to_ket x) y) =
kronecker (bv_to_ket x)  (xor_qbits (ket 1 (f x)) y)

See https://github.com/Qbricks/qbricks.github.io/blob/main/Case_studies/deutsch-jozsa.mlw for the implementation of deutsch_oracle.
The definition of a Deutsch-Jozsa oracle within the QBricks language <cit.>. The require statements note the preconditions of the oracle (there is at least 1 qubit and if $f$ is not constant then it is balanced). The first ensures statements maintains the width of the oracle from input to output. The second ensures statement gives the usual definition of a quantum oracle ($O\ket{x}\ket{y} = \ket{x}\ket{f(x) \oplus y}$) from necessary preconditions. This function can be used later to prove properties about the Deutsch-Jozsa algorithm. Full documentation is available at <https://github.com/Qbricks/qbricks.github.io>.

The verification process of programs uses the ideas of the weakest precondition, path sums and quantum Hoare logic to generate proof obligations, building on previous works to suit the requirements of the language. These obligations are then proved using automatic SMT solvers such as Alt-Ergo <cit.> and Z3 <cit.>.
QBricks still requires some interactivity from the user when writing the specification, but as mentioned these are mostly proved automatically.

The language features a vast array of functionalities, including the capability of introducing ancillary qubits in the middle of code, unlike SQIR and QHLProver. The framework adheres to the no-cloning theorem as it only allows certain unitary operations within its DSL.

QBricks still has some limitations though. Currently, there are no in-built capabilities to measure qubits within QBricks-DSL.
Further, QBricks is not designed to interact with classical data, but classical parameters can be used in the generation of circuits.

Despite these limitations, so far QBricks has been able to verify properties for the Phase Estimation and Shor's algorithms, which are the most complex algorithms verified by languages so far.

§.§ Related Verification Tools

This tool is a module in the Python language that implements the ZX-calculus <cit.>.
Still currently under development, PyZX is able to convert back and forth between circuits and ZX graphs. This allows circuits to be simplified and optimised using the rules of the ZX-calculus.
PyZX is not designed for reasoning about programs, but is useful for checking the equivalence of circuits.

This is a verification framework developed for Qiskit <cit.> that verifies if a compiled circuit is the same as the circuit that is programmed by the user <cit.>.
Interestingly, it makes use of Z3 and other SMT solvers to perform this verification automatically, requiring the user to only input a few lines of specification. While this uses automatic verification, again it should be highlighted that this is used for verifying circuit equivalence, similarly to PyZX, and not for reasoning about programs.

This tool extends Q# with a means of testing programs <cit.>.
Users can initialise qubits, notably their phase, and a number of different postconditions to be met by the resulting qubits. With this, the user can then define parameters that are used to run the tests. When run, test cases are randomly generated, executed on the program and checked they meet the postconditions given. This makes it very easy to quickly test a few properties of a program. However, this tool is designed for testing purposes and not for formal verification of programs. Despite this, it may find use for simpler programs that do not need to be verified extensively[In early 2021, Microsoft added some testing and debugging functionality to Q#: <https://docs.microsoft.com/en-us/azure/quantum/user-guide/testing-debugging?tabs=tabid-vs2019>].

§ VERIFYING COMPLEX QUANTUM ALGORITHMS

Whilst many standard quantum algorithms have been verified in a number of the tools described above, specific techniques will be needed to verify complex algorithms. Here we study the problems that arise for verifying the Harrow-Hassidim-Lloyd algorithm <cit.> and the Binary Welded Tree quantum walk algorithm <cit.>.

§.§ The Harrow-Hassidim-Lloyd Algorithm

The Harrow-Hassidim-Lloyd (HHL) <cit.>  quantum algorithm solves linear systems of equations. Specifically, given a sparse, Hermitian matrix $\mathbf{A}$ and unit vector $\mathbf{b}$, find $\mathbf{x}$ such that $\mathbf{Ax} = \mathbf{b}$.[Although it is possible to change a linear system problem that uses a non-Hermitian matrix to one that uses a Hermitian matrix (details are within <cit.>).]
Using a matrix $\mathbf{A}$ as described above, the classical Conjugate-Gradient method can be used to find $\mathbf{x}$ in time $O(N\kappa s \log{(1/\epsilon)})$, where $N$ is the size of $\mathbf{A}$, $\kappa$ is the condition number of $\mathbf{A}$, $s$ denotes how sparse $\mathbf{A}$ is and $\epsilon$ is the error . In the case of the HHL algorithm, the actual output is an approximation of $\mathbf{x}$ using a measurement matrix $\mathbf{M}$. This approximation can be found classically in $O(N \kappa \text{poly}(1/\epsilon))$. The run time of HHL is $O(\log{(N)} \kappa^2 s^2 / \epsilon^3)$ and returns the answer with high probability, providing an exponential speedup with respect to $N$.
The circuit for the HHL algorithm is given in Figure <ref> and some Silq code is presented in Figure <ref>.

$\ket{0}$         [wires=3, steps=6, style=dashed]repeat until measure 1             R                      $\ket{1}$

$\ket{0}$     p             [wires=2]QPE     -1     [wires=2]QPE^†                 $\ket{0}$

$\ket{0}$     n     B                         M          $\ket{x}$

The circuit begins with 3 quantum registers: the ancillary of 1 qubit, the estimation register of p qubits, and the vector register of size n. Each register is initialised to 0. The B gate is applied to the vector register, then a QPE gate is applied to the vector and estimation register. Using the estimation register as a control, an rotation gate R is applied to the ancillary qubit. After that, the QPE routine is reversed and the ancillary qubit is then measured. These steps are all contained in a box that repeats until a 1 is measured, which then applies an M gate and measurement on the vector register. This results in the final state 10x (where x is the final vector).
The quantum circuit for the HHL algorithm.

// Init b
b_q := orB(b_q);

// QPE
eigen_qs := H_n[prec](eigen_qs);
b_q := qpe_ham_loop[n, prec](eigen_qs, t, hamU, b_q);
eigen_qs := reverse(qft[prec])(eigen_qs);

// Controlled rotation
anc := control_rot[n, prec](eigen_qs, approx_lambda, t/(2*pi), anc);

// Inverse QPE
eigen_qs := qft[prec](eigen_qs);
b_q := qpe_ham_loop[n, prec](eigen_qs, t, revhamU, b_q);
eigen_qs := H_n[prec](eigen_qs);

// Measure ancillary
repeat_loop = not(measure(anc));

Main loop body for the HHL algorithm written in Silq. Full code available at <https://github.com/marco-lewis/silq-hhl>.
A sample of source code from silq-hhl/hhl.slq.

Here we give a brief explanation of how the HHL algorithm works. Let $N = 2^n$ and the $N$-length unit vector $\mathbf{b}$ be represented by the quantum state $\ket{b} = \sum_{i= 0}^{N-1} \mathbf{b}_i \ket{i}$. This is loaded into a $n$-qubit register using an operator $B$. Hamiltonian simulation is used to represent $\mathbf{A}$ in a quantum phase estimation call. The unitary matrix $U$ in quantum phase estimation is $e^{-i\mathbf{A}t}$ for HHL and rotates $\ket{b} = \sum_{j} \beta_j \ket{\mu_j}$ around the eigenvectors of $\mathbf{A}$, which are $\mathbf{\mu_j}$ and $\ket{\mu_j}$ being their quantum state representation (similarly to $\ket{b}$).

Performing the quantum phase estimation ($QPE$) call entangles the eigenvalue representations of $\mathbf{A}$ in a new quantum register with their associated eigenvectors. This gives a quantum state of the form $\sum_j \ket{\lambda_j}\ket{\mu_j}$. The eigenvalues are then embedded into the phase of the quantum state using controlled rotations on an ancillary qubit (using an operator $R$), leaving the quantum state as $\sum_j \ket{\lambda_j}\ket{\mu_j}(C\ket{0} + \frac{1}{\lambda_j}\ket{1}$).

The quantum phase estimation routine is undone and the ancillary qubit is then measured. If it returns $\ket{0}$, then the entire quantum state is dumped and the algorithm is run again. If it returns $\ket{1}$, then the register that previously contained $\ket{b}$ now contains $\ket{x} = \sum_j \frac{\beta_j}{\lambda_j} \ket{\mu_j}$, a representation of $\mathbf{x}$. This can then be measured after applying $\mathbf{M}$, which changes the basis that $\ket{x}$ is measured in.

The HHL algorithm has a number of features that will make formal verification of an implementation challenging. Some of these features are not common in the standard algorithms and are discussed.

Repeat until Success
One of the key aspects involved in this algorithm is the Repeat until Success loop that is dependent on the measurement of an ancillary qubit.
This feature is also an aspect of Shor's algorithm <cit.>, since there are possibilities for a measured result to be invalidated through classical checks.
QHLProver is the only suitable verification framework that can handle  loops dependent on measurement outcomes. This is achieved through the verification of the while statement in the quantum-while language.

As mentioned the HHL algorithm features the quantum phase estimation algorithm. This would need to be verifiable first before much progress could be made on the HHL algorithm. However, it is also important to consider what properties of quantum phase estimation need to be proved for different algorithms.
For HHL, it will be important to show that $\mathbf{b}$ has a representation under the eigenvectors of $\mathbf{A}$.
It will also be important to consider how the eigenvalue representations affects the phase of the quantum state. Verification will be needed here to prevent side effects within a program.

Hamiltonian Simulation Approximation
Hamiltonian simulation is used to give a unitary approximation of the evolution of a Hamiltonian system. This technique has been used with matrices of different types for different purposes (as is the case in HHL). A verification tool will need to ensure that an implementation of an approximation is actually a good approximation of the behaviour that is expected.
Techniques for verifying that implementations of a Hamiltonian are correct have not yet been studied (to the best of our knowledge). None of the tools given have verified an example of Hamiltonian simulation. Tools embedded within theorem provers might be able to perform this verification but this will require separate study.

§.§ Walking on Binary Welded Trees

The problem statement of the Binary Welded Tree (BWT) algorithm <cit.> is that there are two trees, of the same depth, that are joined together by a weld at their leaves. The task is to walk from one root node (the entrance node) to the root node on the other tree (the exit node). When at a node, you only have local knowledge, where you cannot ask where you are on the tree but you can identify edges you have been down. For trees of depth $n$, one can walk to the weld and then walk down edges randomly until the exit node is reached. This is referred to as a random walk and has a worst case run time of $O(2^n)$, as one may visit almost every node in the tree.[One can achieve a polynomial classical algorithm, but this uses global knowledge of the walkers position on the graph.] The random quantum approach allows the walker to traverse down all edges from a node by entering a superposition of staying at the current node and traversing to a new node. This quantum approach achieves an exponential speed up in comparison to the classical approach, running in $O(\text{poly}(n))$ and the quantum system will collapse to the root of the other tree with high probability.

Each leaf node in the weld is connected to two leaves on the other tree. Further, the weld is designed such that it is cyclic and every leaf is in the cycle. An example of a binary welded tree is given in Figure <ref>. To identify edges at a node, they are coloured. Edges only need to have a unique colour to the other edges on attached nodes. There is no constraint on the number of colours used, but it is possible to colour a tree using only 4 colours (this can be seen in Figure <ref>).

Examples of a binary welded tree with 4 colours used to colour the edges.
Two binary trees of depth 3 are joined through a weld. The edges from the root to its children are coloured red and green. Then the edges to the leaves are coloured blue and yellow. The weld between the leaves of the tree are coloured red and green. The colouring given ensures that there are no two edges with the same colour entering a node.

Again, the reader should refer to <cit.> for full details on how the algorithm works. To explain briefly, a quantum register is used to represent the nodes and the register is initialised to the start node. The algorithm features a number of colour oracles that modify some ancillary register. A colour oracle returns a connected node if a node has an edge of that colour or the error state if not. Further, an additional qubit is used to flag the error state.

def Ham[n:!N](const G_or: !N x uint[n]->lifted uint[n], t:!R, node_reg:uint[n], neighbour_anc:uint[n], err_anc:B)

for col in [0..numOfCols)
// Perform first V_c oracle
[neighbour_anc, err_anc] := V(G_or, col, node_reg, neighbour_anc, err_anc);

// Simulation of T operation
[node_reg, neighbour_anc, err_anc] := sim_T(t, node_reg, neighbour_anc, err_anc);

// Perform second V_c oracle
[neighbour_anc, err_anc] := V(G_or, col, node_reg, neighbour_anc, err_anc);

return (node_reg, neighbour_anc, err_anc);

A section of Silq code <cit.> for the BWT Algorithm. The colours are looped over, $V$ represents the colour oracle function and $sim\_T$ represents the Hamiltonian simulation that takes places. The colour oracle is used twice to uncompute the ancillaries (full code available at <https://github.com/marco-lewis/silq-binary-welded-trees>).
A sample of source code from silq-binary-welded-trees/BWTAlgorithm.slq.

For a specific colour, the quantum register is put through the colour oracle. Then a rotation occurs through a Hamiltonian simulation. The entangled node register and ancillary register are rotated so that the connected node is slightly rotated into the quantum state. Then the colour oracle is reversed.
The algorithm loops through the colour oracles and repeats this loop a specified number of times. By selecting an appropriate time, the algorithm will stop and return the label of the root of the right tree with high probability. Figure <ref> shows a diagrammatic evolution of the quantum state for the first iteration through the colour oracles.

Initial state starting at the root node of the left tree

A root node with a 1 in.

Evolution with red oracle

A root node and a child node with a red edge, each with 1/2 written in.

Evolution with green oracle

A new child node is added to the root node with a green edge. The root node now has 1/4 written in as does this new node.

Evolution with blue oracle

New child nodes are formed from the children of the root node, each joined by a blue edge. These take half of the values from their parent nodes.

Evolution with yellow oracle

New child nodes are formed from the children of the root node, each joined by a yellow edge. Again these take half of the value from their parent nodes. The final tree is a root node (1/4), two children of the root (1/8 and 1/16) and their children (1/4, 1/8, 1/8 and 1/16 respectively).

Example of the first iteration performing the main procedure through each colour oracle. Inside each node is the probability of that node being measured. A variable can be set to change the proportion of probability moved to a connected node. In this example, half of the probability from a node is shared with its neighbour. Changing the order the oracles are called in would change the evolution of the system.

Through the description of the algorithm, one can see that there are various features that will be difficult to formally verify. Some of these features are discussed.

Loop Invariants
Unlike the measurement based loops in the HHL algorithm, the BWT algorithm features two classical loops: one for the colour oracles and one for repeating the process. This leads to very deep circuits being created and so making the verification process slow from simply unwinding the entire loop.
To verify these loops, either loop invariants need to be made or Bounded Model Checking could be used to unwind the procedure for a number of iterations.
QBricks already features an $iter$ statement for repeating a quantum circuit a finite number of items. Such a feature could be used to verify aspects of BWT, but this is expected to be a challenging task.

Quantum Objects - Nodes vs Qubits
Whereas most of the standard algorithms use qubits to represent values, the BWT algorithm works on a “quantum” graph. While physically this graph would be represented by  qubits, it would be helpful for verification to verify about the nodes and graph structure easily. QuantumOne <cit.> is a recent endeavour into verifying about quantum objects rather than qubits.

Oracle Implementation
In standard algorithms (Deutsch-Jozsa), oracles only refer to a single function with defined constraints. However the oracles for the BWT algorithm are more complex, depending on a classical variable from a loop and featuring an error flag. This provides difficulty in terms of defining the expected behaviour for the oracle function.

§ CONCLUSION

This paper provides the reader some insights into the current state of research for verification within quantum programming.
It should also demonstrate the importance of verification techniques keeping pace with the development of quantum hardware and software.

Given the various topics discussed, we list a few open problems. Whilst this is not an exhaustive list, it should give room for researchers to investigate problems within formal verification of quantum programs:

* Many of the tools listed can only perform verification up to a certain extent. For example, QBricks is unable to handle measurement of qubits and QHLProver is unable to initialise qubits in the middle of a program. Further, most tools do not have the means to verify classical data and operations. So, can a verifier, such as QBricks or a new tool, be used to verify programs with measurement and classical bits? Can properties of various verifiers be merged together or are there practical limits in terms of complexity?

* Languages in the NISQ-era have seen development and it would be worth investigating how theoretical frameworks can be applied to them. Some tools, such as CertiQ, already provide some verification for programming languages. Can a tool be made for the formal verification of programs written in a widely used language (or a subset of it), such as Q# ?

* We have seen examples of the complex quantum algorithms that are currently available. The question remains as to whether simple examples of these algorithms can be verified using tools currently available.

* Further, whilst general quantum programs have been discussed, a question remains over the verification of specific quantum techniques. For example, how to verify simulations of Hamiltonians or quantum loops with classical control?

A final point to highlight is that verifiable programming languages need to be developed to be easy to learn or use.
Non-verifiable languages have the benefit that users can quickly learn the syntax of the language and have access to dedicated documentation.
Those that require verification also require the user to learn the underlying tool that is used to write them if they have not used theorem provers before, e.g. Coq for SQIR and Isabelle for QHL. Making a tool that is easy to use and quick to learn would encourage more programmers to use them.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Abraham et alAbraham
et al2019]
authorpersonHéctor Abraham et al
titleQiskit: An Open-source Framework for Quantum

[Aharonov and Ben-OrAharonov and
authorpersonDorit Aharonov and
personMichael Ben-Or. year2008.
Fault-Tolerant Quantum Computation with Constant
Error Rate.
journalSIAM J. Comput. volume38,
number4 (year2008), pages1207–1282.

authorpersonMatthew Amy.
Towards Large-scale Functional Verification of
Universal Quantum Circuits.
journalElectronic Proceedings in Theoretical
Computer Science volume287, number287
(year2019), pages1–21.

[Ardeshir-Larijani, Gay, and
NagarajanArdeshir-Larijani et al2018]
authorpersonEbrahim Ardeshir-Larijani,
personSimon J. Gay, and personRajagopal Nagarajan.
Automated Equivalence Checking of Concurrent
Quantum Systems.
journalACM Trans. Comput. Logic
volume19, number4, Article articleno28
(dateNov. year2018), numpages32 pages.

[Arute et alArute
et al2019]
authorpersonFrank Arute et al
Quantum Supremacy using a Programmable
Superconducting Processor.
journalNature  volume574
(year2019), pages505–510.

[Backens, Perdrix, and WangBackens
et al2017]
authorpersonMiriam Backens, personSimon
Perdrix, and personQuanlong Wang.
A Simplified Stabilizer ZX-calculus.
journalElectronic Proceedings in Theoretical
Computer Science  volume236 (dateJan
year2017), pages1–20.

[Baltazar, Chadha, and MateusBaltazar
et al2008]
authorpersonPedro Baltazar, personRohit
Chadha, and personPaulo Mateus.
Quantum Computation Tree Logic — Model Checking
and Complete Calculus.
journalInternational Journal of Quantum
Information volume06, number02
(year2008), pages219–236.

[Barrett, Sebastiani, Seshia, and
TinelliBarrett et al2021]
authorpersonClark W. Barrett, personRoberto
Sebastiani, personSanjit A. Seshia, and
personCesare Tinelli. year2021.
Satisfiability Modulo Theories.
In booktitleHandbook of Satisfiability,
editorpersonArmin Biere, personMarijn
Heule, personHans van Maaren, and personToby
Walsh (Eds.). seriesFrontiers in Artificial Intelligence and
Applications, Vol. volume336. publisherIOS Press,

[Bengtsson, Larsen, Larsson, Pettersson, and
YiBengtsson et al1995]
authorpersonJohan Bengtsson,
personKim Guldstrand Larsen, personFredrik Larsson,
personPaul Pettersson, and personWang Yi.
UPPAAL - a Tool Suite for Automatic Verification
of Real-Time Systems. In booktitleHybrid Systems III:
Verification and Control, Proceedings of the DIMACS/SYCON Workshop on
Verification and Control of Hybrid Systems, October 22-25, 1995, Ruttgers
University, New Brunswick, NJ, USA (seriesLecture Notes
in Computer Science, Vol. volume1066),
editorpersonRajeev Alur, personThomas A.
Henzinger, and personEduardo D. Sontag (Eds.).
publisherSpringer, pages232–243.

[Bennett and BrassardBennett and
authorpersonCharles H. Bennett and
personGilles Brassard. year2014.
Quantum cryptography: Public key distribution and
coin tossing.
journalTheoretical Computer Science
volume560 (year2014), pages7–11.

Theoretical Aspects of Quantum Cryptography – celebrating 30 years
of BB84.

[Bennett, Brassard, Crépeau, Jozsa, Peres,
and WoottersBennett et al1993]
authorpersonCharles H. Bennett, personGilles
Brassard, personClaude Crépeau, personRichard
Jozsa, personAsher Peres, and personWilliam K.
Wootters. year1993.
Teleporting an unknown quantum state via dual
classical and Einstein-Podolsky-Rosen channels.
journalPhys. Rev. Lett.  volume70
(year1993), pages1895–1899.
Issue 13.

[Bhatia and KumarBhatia and Kumar2020]
authorpersonAmandeep Singh Bhatia and
personAjay Kumar. year2020.
On Relation Between Linear Temporal Logic and
Quantum Finite Automata.
journalJ. Log. Lang. Inf. volume29,
number2 (year2020), pages109–120.

[Bichsel, Baader, Gehr, and VechevBichsel
et al2020]
authorpersonBenjamin Bichsel,
personMaximilian Baader, personTimon Gehr, and
personMartin T. Vechev. year2020.
Silq: a high-level quantum language with safe
uncomputation and intuitive semantics. In
booktitleProceedings of the 41st ACM SIGPLAN
International Conference on Programming Language Design and Implementation,
PLDI 2020, London, UK, June 15-20, 2020,
editorpersonAlastair F. Donaldson and
personEmina Torlak (Eds.). publisherACM,

[Biere, Cimatti, Clarke, and ZhuBiere
et al1999]
authorpersonArmin Biere, personAlessandro
Cimatti, personEdmund M. Clarke, and personYunshan
Zhu. year1999.
Symbolic Model Checking without BDDs. In
booktitleTools and Algorithms for Construction and Analysis
of Systems, 5th International Conference, TACAS '99, Held as Part of the
European Joint Conferences on the Theory and Practice of Software, ETAPS'99,
Amsterdam, The Netherlands, March 22-28, 1999, Proceedings
(seriesLNCS, Vol. volume1579),
editorpersonRance Cleaveland (Ed.).
publisherSpringer, pages193–207.

[Bordg, Lachnitt, and HeBordg
et al2020a]
authorpersonAnthony Bordg, personHanna
Lachnitt, and personYijun He.
Certified Quantum Computation in Isabelle/HOL.
journalJournal of Automated Reasoning 2020 65:5
volume65 (date12 year2020),
Issue 5.

[Bordg, Lachnitt, and HeBordg
et al2020b]
authorpersonAnthony Bordg, personHanna
Lachnitt, and personYijun He.
Isabelle Marries Dirac: a Library for Quantum
Computation and Quantum Information.
journalArchive of Formal Proofs
(dateNov. year2020).
<https://isa-afp.org/entries/Isabelle_Marries_Dirac.html>, Formal
proof development.

[Bravyi and GossetBravyi and Gosset2016]
authorpersonSergey Bravyi and personDavid
Gosset. year2016.
Improved Classical Simulation of Quantum Circuits
Dominated by Clifford Gates.
journalPhys. Rev. Lett.  volume116
(dateJun year2016), pages250501.
Issue 25.

[Cao, Romero, Olson, Degroote, Johnson,
Kieferová, Kivlichan, Menke, Peropadre, Sawaya, Sim, Veis, and
Aspuru-GuzikCao et al2019]
authorpersonYudong Cao, personJonathan
Romero, personJonathan P. Olson, personMatthias
Degroote, personPeter D. Johnson, personMária
Kieferová, personIan D. Kivlichan, personTim Menke,
personBorja Peropadre, personNicolas P. D. Sawaya,
personSukin Sim, personLibor Veis, and
personAlán Aspuru-Guzik. year2019.
Quantum Chemistry in the Age of Quantum Computing.
journalChemical Reviews volume119,
number19 (year2019), pages10856–10915.

PMID: 31469277.

[Chadha, Mateus, Sernadas, and SernadasChadha
et al2009]
authorpersonRohit Chadha, personPaulo
Mateus, personAmílcar Sernadas, and personCristina
Sernadas. year2009.
Extending Classical Logic for Reasoning About
Quantum Systems.
In booktitleHandbook of Quantum Logic and Quantum
Structures, editorpersonKurt Engesser,
personDov M. Gabbay, and personDaniel Lehmann
(Eds.). publisherElsevier, addressAmsterdam,
pages325 – 371.

[Chareton, Bardin, Bobot, Perrelle, and
ValironChareton et al2020]
authorpersonChristophe Chareton,
personSébastien Bardin, personFrançois
Bobot, personValentin Perrelle, and
personBenoît Valiron. year2020.
Toward certified quantum programming.
journalCoRR  volumeabs/2003.05841

[Chareton, Bardin, Lee, Valiron, Vilmart, and
XuChareton et al2021]
authorpersonChristophe Chareton,
personSébastien Bardin, personDongho Lee,
personBenoît Valiron, personRenaud Vilmart, and
personZhaowei Xu. year2021.
titleFormal Methods for Quantum Programs: A Survey.
[arxiv]2109.06493 [cs.PL]

[Childs, Cleve, Deotto, Farhi, Gutmann, and
SpielmanChilds et al2003]
authorpersonAndrew M. Childs, personRichard
Cleve, personEnrico Deotto, personEdward Farhi,
personSam Gutmann, and personDaniel A. Spielman.
Exponential Algorithmic Speedup by a Quantum Walk.
In booktitleProceedings of the Thirty-Fifth Annual ACM
Symposium on Theory of Computing (San Diego, CA, USA)
(seriesSTOC '03). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Cimatti, Clarke, Giunchiglia, Giunchiglia,
Pistore, Roveri, Sebastiani, and TacchellaCimatti et al2002]
authorpersonAlessandro Cimatti,
personEdmund M. Clarke, personEnrico Giunchiglia,
personFausto Giunchiglia, personMarco Pistore,
personMarco Roveri, personRoberto Sebastiani, and
personArmando Tacchella. year2002.
NuSMV 2: An OpenSource Tool for Symbolic Model
Checking. In booktitleProceedings of the 14th International
Conference on Computer Aided Verification (seriesCAV
'02). publisherSpringer-Verlag, addressBerlin,
Heidelberg, pages359–364.

[Clarke and EmersonClarke and
authorpersonEdmund M. Clarke and
personE. Allen Emerson. year1982.
Design and synthesis of synchronization skeletons
using branching time temporal logic. In booktitleLogics of
Programs, editorpersonDexter Kozen (Ed.).
publisherSpringer Berlin Heidelberg, addressBerlin,
Heidelberg, pages52–71.

[Clarke, Grumberg, Jha, Lu, and VeithClarke
et al2000]
authorpersonEdmund M. Clarke, personOrna
Grumberg, personSomesh Jha, personYuan Lu, and
personHelmut Veith. year2000.
Counterexample-Guided Abstraction Refinement. In
booktitleComputer Aided Verification, 12th International
Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings
(seriesLNCS, Vol. volume1855),
editorpersonE. Allen Emerson and
personA. Prasad Sistla (Eds.). publisherSpringer,

[Clarke, Grumberg, and LongClarke
et al1994]
authorpersonEdmund M. Clarke, personOrna
Grumberg, and personDavid E. Long.
Model Checking and Abstraction.
journalACM Trans. Program. Lang. Syst.
volume16, number5 (year1994),

[Clarke, Grumberg, and PeledClarke
et al2001]
authorpersonEdmund M. Clarke, personOrna
Grumberg, and personDoron A. Peled.
booktitleModel checking.
publisherMIT Press.

[Clarke, Klieber, Nováček, and
ZulianiClarke et al2012]
authorpersonEdmund M. Clarke, personWilliam
Klieber, personMiloš Nováček, and
personPaolo Zuliani. year2012.
booktitleModel Checking and the State Explosion
publisherSpringer Berlin Heidelberg,
addressBerlin, Heidelberg, pages1–30.

[Clauser, Horne, Shimony, and HoltClauser
et al1969]
authorpersonJohn F. Clauser,
personMichael A. Horne, personAbner Shimony, and
personRichard A. Holt. year1969.
Proposed Experiment to Test Local Hidden-Variable
journalPhys. Rev. Lett.  volume23
(dateOct year1969), pages880–884.
Issue 15.

[Coecke and DuncanCoecke and Duncan2011]
authorpersonBob Coecke and personRoss
Duncan. year2011.
Interacting quantum observables: categorical
algebra and diagrammatics.
journalNew Journal of Physics
volume13, number4 (dateapr
year2011), pages043016.

[Conchon, Coquereau, Iguernlala, and
MebsoutConchon et al2018]
authorpersonSylvain Conchon, personAlbin
Coquereau, personMohamed Iguernlala, and
personAlain Mebsout. year2018.
Alt-Ergo 2.2. In booktitleSMT
Workshop: International Workshop on Satisfiability Modulo Theories.
addressOxford, United Kingdom.

[Davidson, Gay, Mlnarik, Nagarajan, and
PapanikolaouDavidson et al2012]
authorpersonTimothy A. S. Davidson,
personSimon J. Gay, personHynek Mlnarik,
personRajagopal Nagarajan, and personNick
Papanikolaou. year2012.
Model Checking for Communicating Quantum
journalInt. J. Unconv. Comput.
volume8, number1 (year2012),

[De Moura and BjørnerDe Moura and
authorpersonLeonardo De Moura and
personNikolaj Bjørner. year2008.
Z3: An Efficient SMT Solver. In
booktitleProceedings of the Theory and Practice of Software,
14th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (Budapest, Hungary)
publisherSpringer-Verlag, addressBerlin, Heidelberg,

[De Moura and BjørnerDe Moura and
authorpersonLeonardo De Moura and
personNikolaj Bjørner. year2009.
Satisfiability Modulo Theories: An Appetizer. In
booktitleSBMF '09 (seriesLNCS,
Vol. volume5902). publisherSpringer,

[Deutsch and JozsaDeutsch and
authorpersonDavid Deutsch and
personRichard Jozsa. year1992.
Rapid Solution of Problems by Quantum
journalProceedings of the Royal Society of London
Series A volume439, number1907
(dateDec. year1992), pages553–558.

[D'Hondt and PanangadenD'Hondt and
authorpersonEllie D'Hondt and
personPrakash Panangaden. year2006.
Quantum weakest preconditions.
journalMath. Struct. Comput. Sci.
volume16, number3 (year2006),

authorpersonEdsger W. Dijkstra.
Guarded Commands, Nondeterminacy and Formal
Derivation of Programs.
journalCommun. ACM volume18,
number8 (dateAug. year1975),

authorpersonBruno Dutertre.
Yices 2.2. In
booktitleComputer-Aided Verification (CAV'2014)
(seriesLecture Notes in Computer Science,
Vol. volume8559), editorpersonArmin
Biere and personRoderick Bloem (Eds.).
publisherSpringer, pages737–744.

authorpersonMnacho Echenim.
Quantum projective measurements and the CHSH
journalArchive of Formal Proofs
(dateMarch year2021).
Formal proof development.

[Echenim and MhallaEchenim and
authorpersonMnacho Echenim and personMehdi
Mhalla. year2021.
Quantum projective measurements and the CHSH
inequality in Isabelle/HOL.
(date3 year2021).

[Feng and YingFeng and Ying2020]
authorpersonYuan Feng and personMingsheng
Ying. year2020.
Quantum Hoare logic with classical variables.
journalCoRR  volumeabs/2008.06812

[Feng, Yu, and YingFeng
et al2013]
authorpersonYuan Feng, personNengkun Yu,
and personMingsheng Ying. year2013.
Model checking quantum Markov chains.
journalJ. Comput. System Sci.
volume79, number7 (year2013),
pages1181 – 1198.

[Frehse, Guernic, Donzé, Cotton, Ray,
Lebeltel, Ripado, Girard, Dang, and MalerFrehse et al2011]
authorpersonGoran Frehse, personColas Le
Guernic, personAlexandre Donzé, personScott
Cotton, personRajarshi Ray, personOlivier Lebeltel,
personRodolfo Ripado, personAntoine Girard,
personThao Dang, and personOded Maler.
SpaceEx: Scalable Verification of Hybrid Systems.
In booktitleComputer Aided Verification - 23rd International
Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings
(seriesLNCS, Vol. volume6806),
editorpersonGanesh Gopalakrishnan and
personShaz Qadeer (Eds.). pages379–395.

[Gao, Kong, and ClarkeGao
et al2013]
authorpersonSicun Gao, personSoonho Kong,
and personEdmund M. Clarke. year2013.
dReal: An SMT Solver for Nonlinear Theories over
the Reals. In booktitleAutomated Deduction - CADE-24 -
24th International Conference on Automated Deduction, Lake Placid, NY, USA,
June 9-14, 2013. Proceedings (seriesLNCS,
Vol. volume7898), editorpersonMaria Paola
Bonacina (Ed.). publisherSpringer, pages208–214.

authorpersonDaniel Gottesman.
The Heisenberg Representation of Quantum
journalarXiv e-prints (dateJuly

[Green, Lumsdaine, Ross, Selinger, and
ValironGreen et al2013]
authorpersonAlexander S. Green,
personPeter LeFanu Lumsdaine, personNeil J. Ross,
personPeter Selinger, and personBenoît Valiron.
Quipper: A Scalable Quantum Programming Language.
journalAcm Sigplan Notices volume48,
number6 (year2013), pages333–342.

authorpersonLov K. Grover.
A Fast Quantum Mechanical Algorithm for Database
Search. In booktitleProceedings of the Twenty-Eighth Annual
ACM Symposium on the Theory of Computing, Philadelphia, Pennsylvania, USA,
May 22-24, 1996, editorpersonGary L. Miller (Ed.).
publisherACM, pages212–219.

[Hähnle and HuismanHähnle and
authorpersonReiner Hähnle and
personMarieke Huisman. year2019.
Deductive Software Verification: From Pen-and-Paper
Proofs to Industrial Tools.
In booktitleComputing and Software Science - State
of the Art and Perspectives, editorpersonBernhard
Steffen and personGerhard J. Woeginger (Eds.).
seriesLecture Notes in Computer Science,
Vol. volume10000. publisherSpringer,

[Harrow, Hassidim, and LloydHarrow
et al2009]
authorpersonAram W. Harrow, personAvinatan
Hassidim, and personSeth Lloyd.
Quantum Algorithm for Linear Systems of Equations.
journalPhys. Rev. Lett.  volume103
(dateOct year2009), pages150502.
Issue 15.

[Hensel, Junges, Katoen, Quatmann, and
VolkHensel et al2021]
authorpersonChristian Hensel,
personSebastian Junges, personJoost-Pieter Katoen,
personTim Quatmann, and personMatthias Volk.
The probabilistic model checker Storm.
journalInternational Journal on Software Tools for
Technology Transfer (date7 year2021).

[Hietala, Rand, Hung, Li, and
HicksHietala et al2020]
authorpersonKesha Hietala, personRobert
Rand, personShih-Han Hung, personLiyi Li,
and personMichael Hicks. year2020.
Proving Quantum Programs Correct.
journalarXiv e-prints (dateOct.
[arxiv]2010.01240 [cs.PL]

authorpersonC. A. R. Hoare.
An Axiomatic Basis for Computer Programming.
journalCommun. ACM volume12,
number10 (year1969), pages576–580.

authorpersonGerard Holzmann.
booktitleThe SPIN Model Checker - primer and
reference manual (editionfirst ed.).
publisherAddison-Wesley Professional.

[Honarvar, Mousavi, and NagarajanHonarvar
et al2020]
authorpersonShahin Honarvar,
personMohammad Reza Mousavi, and personRajagopal
Nagarajan. year2020.
Property-Based Testing of Quantum Programs in Q#.
In booktitleProceedings of the IEEE/ACM 42nd International
Conference on Software Engineering Workshops (Seoul, Republic of Korea)
(seriesICSEW'20). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Huang and MartonosiHuang and
authorpersonYipeng Huang and
personMargaret Martonosi. year2019.
QDB: From Quantum Algorithms Towards Correct
Quantum Programs. In booktitle9th Workshop on Evaluation
and Usability of Programming Languages and Tools (PLATEAU 2018)
(seriesOpenAccess Series in Informatics (OASIcs),
Vol. volume67), editorpersonTitus Barik,
personJoshua Sunshine, and personSarah Chasins
(Eds.). publisherSchloss Dagstuhl–Leibniz-Zentrum fuer
Informatik, addressDagstuhl, Germany,

authorpersonYoshihiko Kakutani.
A Logic for Formal Verification of Quantum
Programs. In booktitleAdvances in Computer Science - ASIAN
2009. Information Security and Privacy,
editorpersonAnupam Datta (Ed.).
publisherSpringer Berlin Heidelberg, addressBerlin,
Heidelberg, pages79–93.

[Kissinger and van de WeteringKissinger and
van de Wetering2020]
authorpersonAleks Kissinger and personJohn
van de Wetering. year2020.
PyZX: Large Scale Automated Diagrammatic
Reasoning. In booktitleProceedings 16th International
Conference on Quantum Physics and Logic, Chapman University, Orange,
CA, USA., 10-14 June 2019 (seriesElectronic Proceedings
in Theoretical Computer Science, Vol. volume318),
editorpersonBob Coecke and personMatthew
Leifer (Eds.). publisherOpen Publishing Association,

authorpersonEmanuel Knill.
Conventions for quantum pseudocode.
(date6 year1996).

[Kondacs and WatrousKondacs and
authorpersonAttila Kondacs and personJohn
Watrous. year1997.
On the Power of Quantum Finite State Automata. In
booktitle38th Annual Symposium on Foundations of Computer
Science, FOCS '97, Miami Beach, Florida, USA, October 19-22, 1997.
publisherIEEE Computer Society, pages66–75.

authorpersonDexter Kozen.
Results on the propositional $\mu$-calculus. In
booktitleAutomata, Languages and Programming,
editorpersonMogens Nielsen and
personErik Meineche Schmidt (Eds.). publisherSpringer
Berlin Heidelberg, addressBerlin, Heidelberg,

[Kwiatkowska, Norman, and ParkerKwiatkowska
et al2011]
authorpersonMarta Z. Kwiatkowska,
personGethin Norman, and personDavid Parker.
PRISM 4.0: Verification of Probabilistic
Real-Time Systems. In booktitleComputer Aided Verification
- 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20,
2011. Proceedings (seriesLNCS,
Vol. volume6806), editorpersonGanesh
Gopalakrishnan and personShaz Qadeer (Eds.).
publisherSpringer, pages585–591.

[Liu, Zhan, Wang, Ying, Liu, Li, Ying, and
ZhanLiu et al2019a]
authorpersonJunyi Liu, personBohua Zhan,
personShuling Wang, personShenggang Ying,
personTao Liu, personYangjia Li,
personMingsheng Ying, and personNaijun Zhan.
booktitleFormal Verification of Quantum Algorithms
Using Quantum Hoare Logic.
publisherSpringer International Publishing,

[Liu, Zhan, Wang, Ying, Liu, Li, Ying, and
ZhanLiu et al2019b]
authorpersonJunyi Liu, personBohua Zhan,
personShuling Wang, personShenggang Ying,
personTao Liu, personYangjia Li,
personMingsheng Ying, and personNaijun Zhan.
Quantum Hoare Logic.
journalArchive of Formal Proofs
(dateMarch year2019).
<https://isa-afp.org/entries/QHLProver.html>, Formal proof

[Mateus, Ramos, Sernadas, and SernadasMateus
et al2009]
authorpersonPaulo Mateus, personJaime
Ramos, personAmílcar Sernadas, and personCristina
Sernadas. year2009.
booktitleTemporal Logics for Reasoning about Quantum
publisherCambridge University Press,

[Miller, Whalen, and CoferMiller
et al2010]
authorpersonSteven P. Miller,
personMichael W. Whalen, and personDarren D.
Cofer. year2010.
Software Model Checking Takes Off.
journalCommun. ACM volume53,
number2 (dateFeb. year2010),

[Nielsen and ChuangNielsen and
authorpersonMichael A. Nielsen and
personIsaac L. Chuang. year2016.
booktitleQuantum Computation and Quantum Information
(10th Anniversary edition).
publisherCambridge University Press.

[Paler and DevittPaler and Devitt2015]
authorpersonAlexandru Paler and
personSimon J. Devitt. year2015.
An Introduction into Fault-Tolerant Quantum
Computing. In booktitleProceedings of the 52nd Annual
Design Automation Conference (San Francisco, California)
(seriesDAC '15). publisherAssociation for
Computing Machinery, addressNew York, NY, USA, Article
articleno60, numpages6 pages.

[Paykin, Rand, and ZdancewicPaykin
et al2017]
authorpersonJennifer Paykin, personRobert
Rand, and personSteve Zdancewic.
QWIRE: A Core Language for Quantum Circuits.
journalSIGPLAN Not. volume52,
number1 (dateJan. year2017),

authorpersonAmir Pnueli.
The Temporal Logic of Programs. In
booktitleProceedings of the 18th Annual Symposium on
Foundations of Computer Science (seriesSFCS '77).
publisherIEEE Computer Society, addressUSA,

authorpersonJohn Preskill.
Quantum Computing in the NISQ era and beyond.
journalQuantum  volume2
(dateAug. year2018), pages79.

authorpersonJoschka Roffe.
Quantum error correction: an introductory guide.
journalContemporary Physics volume60,
number3 (year2019), pages226–245.

[Sanders and ZulianiSanders and
authorpersonJeff W. Sanders and
personPaolo Zuliani. year2000.
Quantum Programming. In
booktitleMathematics of Program Construction,
editorpersonRoland Backhouse and
personJosé Nuno Oliveira (Eds.).
publisherSpringer Berlin Heidelberg, addressBerlin,
Heidelberg, pages80–99.

authorpersonPeter Selinger.
Towards a quantum programming language.
journalMathematical Structures in Computer Science
volume14, number4 (year2004),

authorpersonJonathan R Shewchuk.
booktitleAn Introduction to the Conjugate Gradient
Method Without the Agonizing Pain.
typeTechnical Report. addressUSA.

[Shi, Tao, Li, Javadi-Abhari, Cross,
Chong, and GuShi et al2019]
authorpersonYunong Shi, personRunzhou
Tao, personXupeng Li, personAli Javadi-Abhari,
personAndrew W. Cross, personFrederic T. Chong,
and personRonghui Gu. year2019.
CertiQ: A Mostly-automated Verification of a
Realistic Quantum Compiler.
journalarXiv e-prints, Article
articlenoarXiv:1908.08963 (dateAug.
year2019), numpagesarXiv:1908.08963 pages.
[arxiv]1908.08963 [quant-ph]

[Shmarov and ZulianiShmarov and
authorpersonFedor Shmarov and personPaolo
Zuliani. year2015.
ProbReach: verified probabilistic
delta-reachability for stochastic hybrid systems. In
booktitleProceedings of the 18th International Conference on
Hybrid Systems: Computation and Control, HSCC'15, Seattle, WA, USA, April
14-16, 2015, editorpersonAntoine Girard and
personSriram Sankaranarayanan (Eds.).
publisherACM, pages134–139.

authorpersonPeter W. Shor.
Polynomial-Time Algorithms for Prime Factorization
and Discrete Logarithms on a Quantum Computer.
journalSIAM J. Comput. volume26,
number5 (year1997), pages1484–1509.

[Svore, Geller, Troyer, Azariah, Granade, Heim,
Kliuchnikov, Mykhailova, Paz, and RoettelerSvore et al2018]
authorpersonKrysta M. Svore, personAlan
Geller, personMatthias Troyer, personJohn Azariah,
personChristopher E. Granade, personBettina Heim,
personVadym Kliuchnikov, personMariia Mykhailova,
personAndres Paz, and personMartin Roetteler.
Q#: Enabling Scalable Quantum Computing and
Development with a High-level DSL. In
booktitleProceedings of the Real World Domain Specific
Languages Workshop, RWDSL@CGO 2018, Vienna, Austria, February 24-24, 2018.
publisherACM, pages7:1–7:10.

authorpersonThe Coq Development Team.
booktitleThe Coq Proof Assistant, version 8.12.0.

[Unnikrishnan and MarkhamUnnikrishnan and
authorpersonAnupama Unnikrishnan and
personDamian Markham. year2020.
Authenticated teleportation and verification in a
noisy network.
journalPhys. Rev. A  volume102
(dateOct year2020), pages042401.
Issue 4.

authorpersonDominique Unruh.
Quantum Relational Hoare Logic.
journalProc. ACM Program. Lang.
volume3, numberPOPL, Article articleno33
(dateJan. year2019), numpages31 pages.

[Voichick and HicksVoichick and
authorpersonFinn Voichick and
personMichael Hicks. year2021.
Toward A Quantum Programming Language for
Higher-Level Formal Verification. In booktitleInformal
Proceedings of the Workshop on Programming Languages and Quantum Computing

[Whitfield, Biamonte, and
Aspuru-GuzikWhitfield et al2011]
authorpersonJames D. Whitfield, personJacob
Biamonte, and personAlán Aspuru-Guzik.
Simulation of electronic structure Hamiltonians
using quantum computers.
journalMolecular Physics volume109,
number5 (year2011), pages735–750.

authorpersonFreek Wiedijk.
booktitleThe Seventeen Provers of the World:
Foreword by Dana S. Scott (Lecture Notes in Computer Science / Lecture Notes
in Artificial Intelligence).
publisherSpringer-Verlag, addressBerlin,

[Wootters and ZurekWootters and
authorpersonWilliam K. Wootters and
personWojciech H. Zurek. year1982.
A single quantum cannot be cloned.
journalNature volume299,
number5886 (year1982), pages802–803.

[Xu, Fu, Mei, and DengXu
et al2021]
authorpersonMing Xu, personJianling Fu,
personJingyi Mei, and personYuxin Deng.
An Algebraic Method to Fidelity-based Model
Checking over Quantum Markov Chains.
[arxiv]2101.04971 [cs.LO]

authorpersonMingsheng Ying.
Floyd-hoare logic for quantum programs.
journalACM Trans. Program. Lang. Syst.
volume33, number6 (year2011),

[Ying and FengYing and Feng2018]
authorpersonMingsheng Ying and personYuan
Feng. year2018.
titleModel Checking Quantum Systems — A Survey.
[arxiv]1807.09466 [quant-ph]

authorpersonNengkun Yu.
titleQuantum Temporal Logic.
[arxiv]1908.00158 [cs.LO]

[Zhong, Wang, Deng, Chen, Peng, Luo, Qin, Wu,
Ding, Hu, Hu, Yang, Zhang, Li, Li, Jiang, Gan, Yang, You, Wang, Li, Liu, Lu,
and PanZhong et al2020]
authorpersonHan-Sen Zhong, personHui Wang,
personYu-Hao Deng, personMing-Cheng Chen,
personLi-Chao Peng, personYi-Han Luo,
personJian Qin, personDian Wu, personXing
Ding, personYi Hu, personPeng Hu,
personXiao-Yan Yang, personWei-Jun Zhang,
personHao Li, personYuxuan Li, personXiao
Jiang, personLin Gan, personGuangwen Yang,
personLixing You, personZhen Wang,
personLi Li, personNai-Le Liu,
personChao-Yang Lu, and personJian-Wei Pan.
Quantum computational advantage using photons.
journalScience volume370,
number6523 (year2020), pages1460–1463.

[Zhu et alZhu et al2021]
authorpersonQingling Zhu et al
titleQuantum Computational Advantage via 60-Qubit 24-Cycle
Random Circuit Sampling.
[arxiv]2109.03494 [quant-ph]

§ CLIFFORD GATES

The Clifford gates <cit.> are the following gate operations:

\begin{equation}
\begin{matrix}
H = \frac{1}{\sqrt{2}}\begin{pmatrix}
1 & 1 \\
1 & -1
\end{pmatrix} &
S = \begin{pmatrix}
1 & 0 \\
0 & i
\end{pmatrix} &
CX = \begin{pmatrix}
1 & 0 & 0 & 0 \\
0 & 1 & 0 & 0 \\
0 & 0 & 0 & 1 \\
0 & 0 & 1 & 0
\end{pmatrix}
\end{matrix}
\end{equation}

Circuits that can be generated from Clifford gates are referred to as being in the Clifford group and can be simulated efficiently on a classical computer, as stated by the Gottesman-Knill theorem <cit.>. It is unknown if all Non-Clifford circuits (i.e. circuits containing operations that cannot be broken down to Clifford operations) can be simulated efficiently.
If this was the case, then quantum computers could be efficiently simulated on classical computers.

The operation $S$ can be generalised to $R_k$, where

\begin{equation}
R_k = \begin{pmatrix}
1 & 0 \\
0 & e^{\frac{2\pi i}{2^k}}
\end{pmatrix}
\end{equation}

and it can easily be seen that if $k\geq 2$, then $(R_k)^{2^{k-2}} = S$ (with $R_2 = S$). For $k \geq 3$, $R_k$ is a non-Clifford operation. The circuits generated by using Clifford gates and the $R_k$ gate (for a fixed $k$) are referred to as the Clifford$+R_k$ group.
In particular, denote $T = R_3 =
\begin{pmatrix}
1 & 0 \\
0 & e^{\pi i/4}
\end{pmatrix}$ and then $\text{Clifford}+R_3 = \text{Clifford}+T$. Algorithms for simulating Clifford$+T$ gates are discussed in <cit.>. The algorithms' runtimes are exponential based on the number of $T$ gates.

§ QUANTUM HOARE LOGIC EXAMPLE

As seen earlier, we have that $\{\textit{Post}\} \textbf{measure } M[q]:\textbf{skip},\textbf{skip} \{\textit{Post}\}$. We now calculate $wp.(q:=Hq).\textit{Post}$. For ease of notation, denote $c = 1-f(0)\oplus f(1)$ and $b = f(0)\oplus f(1)$ (so $\textit{Post} = (c\ket{0}\bra{0} + b \ket{1}\bra{1}$). Using the weakest precondition rules from Proposition 7.1 in <cit.>, we have

\begin{align*}
wp.(q:=Hq).\textit{Post} & = H^\dagger \textit{Post } H \\
& = H (c\ket{0}\bra{0} + b \ket{1}\bra{1}) H \\
& = c\ket{+}\bra{+} + b \ket{-}\bra{-}
\end{align*}

and so we have the Hoare triple $\{c\ket{+}\bra{+} + b \ket{-}\bra{-}\} q:=Hq \{\textit{Post}\}$. Next we find the weakest precondition of $q := O_f q$ for $\{c\ket{+}\bra{+} + b \ket{-}\bra{-}\}$. Using the same rule we have

\begin{align*}
wp.(q:=O_f q). (c\ket{+}\bra{+} + b \ket{-}\bra{-}) &= O_f^\dagger (c\ket{+}\bra{+} + b \ket{-}\bra{-}) O_f \\
&= O_f (c\ket{+}\bra{+} + b \ket{-}\bra{-}) O_f \\
&= ((-1)^{f(0)} \ket{0}\bra{0} + (-1)^{f(1)} \ket{1}\bra{1}) \\
& (c\ket{+}\bra{+} + b \ket{-}\bra{-}) \\
& ((-1)^{f(0)} \ket{0}\bra{0} + (-1)^{f(1)} \ket{1}\bra{1}) \\
&= c ((-1)^{f(0) + f(0)} \ket{0}\bra{0} + (-1)^{f(0) + f(1)} \ket{0}\bra{1} \\
& + (-1)^{f(1) + f(0)} \ket{1}\bra{0} + (-1)^{f(1) + f(1)} \ket{1}\bra{1}) \\
& + b ((-1)^{f(0) + f(0)} \ket{0}\bra{0} - (-1)^{f(0) + f(1)} \ket{0}\bra{1} \\
& - (-1)^{f(1) + f(0)} \ket{1}\bra{0} + (-1)^{f(1) + f(1)} \ket{1}\bra{1}) \\
& = \ket{0}\bra{0} + \ket{0}\bra{1} + \ket{1}\bra{0} + \ket{1} \bra{1} = \ket{+}\bra{+}.
\end{align*}

The penultimate equality holds by taking cases of $f$. If $f(0) \oplus f(1) = 0$, then $c = 1$, the associated density matrix term stays in $\ket{+}\bra{+}$ and the second term becomes a zero matrix as $b = 0$. A similar reasoning holds when $f(0) \oplus f(1) = 1$. Thus, we have the Hoare triple $\{\ket{+}\bra{+}\}q:=O_f q\{c\ket{+}\bra{+} + b \ket{-}\bra{-}\}$.

It is not hard to see that $\{\ket{0}\bra{0}\}q:=Hq\{\ket{+}\bra{+}\}$ with $\ket{0}\bra{0}$ being the weakest precondition of the given statement and postcondition.

Finally, we can use the weakest precondition rule for initialisation:

\begin{equation*}
\end{equation*}

For simplicity, we can drop the $q$ notation from the equation, since we only have a 1-qubit program. Thus, it is easy to see that

\begin{align*}
wp.(q:=0).\ket{0}\bra{0} &= \ket{0}\bra{0}\ket{0}\bra{0}\ket{0}\bra{0}+\ket{1}\bra{0}\ket{0}\bra{0}\ket{0}\bra{1} \\
&= \ket{0} \bra{0} + \ket{1} \bra{1} = I
\end{align*}

and therefore the Hoare triple $\{I\}q:=0\{\ket{0}\bra{0}\}$ holds.
By following the sequential rule, it is easy to see that $wp.(\textit{Deutsch}).\textit{Post} = I$ and we get the desired Hoare triple of $\{I\}\textit{Deutsch}\{\textit{Post}\}$.

§ ZX-CALCULUS EXAMPLE

Here we firstly give a few rewrite rules from <cit.> in Figure <ref>. Whilst many different rewrite rules can be used, these are a few key ones.

A number of different rewrite rules. 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$.

Rule 1: Hadamard nodes are the same as a concatenation of a red, green then red spiders (each with angle pi/2).

Rule 2: A green spider (angle a) followed by a red spider (angle pi) is the same as a red spider (pi) followed by a green spider (-a).

Rule 3: If two spiders, with angles a and b, are joined by a wire, then they can be merged into a single spider with angle a + b (mod 2*pi)

Rule 4: A spider with no angle (angle 0) is the same as just having a wire.

Using these rules, it is now possible to show optimisations of different circuits. For example, we can use the rewrite rules to show that applying two Hadamard gates to a circuit is the same as doing nothing (performing the identity operation). This derivation is given in Figure <ref>.

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>. 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.

Let H denote Hadmard node, R(a) red spiders with angle a and simlarlly G(a) for green spiders. Further "-" denotes wires outside of spider arguments (where they represent minus). We have that:

(-H-H-) = (-R(pi/2)-G(pi/2)-R(pi/2)-R(pi/2)-G(pi/2)-R(pi/2)-) = (-R(pi/2)-G(pi/2)-R(pi)-G(pi/2)-R(pi/2)-) = (-R(pi/2)-G(pi/2)-G(-pi/2)-R(pi)-R(pi/2)-) = (-R(pi/2)-G(0)-R(-pi/2)-) = (-R(pi/2)—R(-pi/2)-) = (–R(0)–) = (—–)