<figure><img src="image_1.png" /></figure>

HAL
open science

Formal Methods for Quantum Algorithms

Christophe Chareton, Sébastien Bardin, Dong Ho Lee, Benoît Valiron,
Renaud Vilmart, Zhaowei Xu

► To cite this version:

Christophe Chareton, Sébastien Bardin, Dong Ho Lee, Benoît Valiron, Renaud Vilmart, et al. Formal Methods for Quantum Algorithms. Handbook of Formal Analysis and Verification in Cryptography, CRC Press; Taylor and Francis, pp.319-422, 2023, Prospect in Pure and Applied Mathematics, 9780367546656. cea-04479879

HAL Id: cea-04479879

https://cea.hal.science/cea-04479879

Submitted on 27 Feb 2024

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.
Formal Methods for Quantum Algorithms

Christophe Chareton, Sébastien Bardin, Dong Ho Lee, Benoît Valiron,
Renaud Vilmart, Zhaowei Xu

► To cite this version:

Christophe Chareton, Sébastien Bardin, Dong Ho Lee, Benoît Valiron, Renaud Vilmart, et al.. Formal Methods for Quantum Algorithms. Handbook of Formal Analysis and Verification in Cryptography, 1, CRC Press; Taylor and Francis, pp.319-422, 2023, Prospect in Pure and Applied Mathematics, 9780367546656. 10.1201/9781003090052-7.cea-04479879

HAL Id: cea-04479879

https://cea.hal.science/cea-04479879v1

Submitted on 27 Feb 2024

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Formal methods for quantum algorithms: A Survey

Christophe Chareton<sup>4</sup>, Sébastien Bardin<sup>4</sup>, Dongho Lee<sup>2,4</sup>, Benoit Valiron<sup>2</sup>, Renaud Vilmart<sup>3</sup>, and Zhaowei Xu<sup>1,5</sup>

<sup>1</sup>Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France

<sup>2</sup>Université Paris-Saclay, Inria, CentraleSupélec, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France

<sup>3</sup>Université Paris-Saclay, Inria, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France

<sup>4</sup>Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France

<sup>5</sup>University of Tartu, Estonia

Abstract

While recent progress in quantum hardware open the door for significant speedup in cryptog-
raphy as well as additional key areas (biology, chemistry, optimization, machine learning, etc),
quantum algorithms are still hard to implement right, and the validation of such quantum pro-
grams is a challenge. Moreover, importing the testing and debugging practices at use in classical
programming is extremely difficult in the quantum case, due to the destructive aspect of quantum
measurement. As an alternative strategy, formal methods are prone to play a decisive role in the
emerging field of quantum software. Recent works initiate solutions for problems occurring at
every stage of the development process: high-level program design, implementation, compila-
tion, etc. We review the induced challenges for an efficient use of formal methods in quantum
computing and the current most promising research directions.
# Formal methods for quantum algorithms: A Survey

Christophe Chareton<sup>4</sup>, Sébastien Bardin<sup>4</sup>, Dongho Lee<sup>2,4</sup>, Benoit Valiron<sup>2</sup>, Renaud Vilmart<sup>3</sup>, and Zhaowei Xu<sup>1,5</sup>

<sup>1</sup>Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France

<sup>2</sup>Université Paris-Saclay, Inria, CentraleSupélec, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France

<sup>3</sup>Université Paris-Saclay, Inria, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France

<sup>4</sup>Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France

<sup>5</sup>University of Tartu, Estonia

## Abstract

While recent progress in quantum hardware open the door for significant speedup in cryptography as well as additional key areas (biology, chemistry, optimization, machine learning, etc), quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. Moreover, importing the testing and debugging practices at use in classical programming is extremely difficult in the quantum case, due to the destructive aspect of quantum measurement. As an alternative strategy, formal methods are prone to play a decisive role in the emerging field of quantum software. Recent works initiate solutions for problems occurring at every stage of the development process: high-level program design, implementation, compilation, etc. We review the induced challenges for an efficient use of formal methods in quantum computing and the current most promising research directions.
# Contents

1 Introduction 5

2 General Background in Quantum Computing 6

2.1 Hybrid Computational Model 7

2.1.1 Hybrid Circuit Model 7

2.1.2 Quantum Data Registers 7

2.1.3 Separable and Entangled States 9

2.1.4 Quantum Circuits 9

2.1.5 Quantum Matrix Semantics and density operators 10

2.1.6 Other Models for Quantum Computations 13

2.2 Algorithms 13

2.2.1 Quantum Algorithms and Complexity 13

2.2.2 Quantum Algorithm Design 14

2.3 Challenges for Quantum Computation 16

2.3.1 Destructive Measurement and Non-Determinism 16

2.3.2 Quantum Noise 16

2.3.3 Efficient Compilation on Constrained Hardware 17

3 General Background on Formal Methods 17

3.1 Introduction 17

3.2 Principles 18

3.3 The Formal Method Zoo 18

4 Overview of Formal Methods in Quantum Computing 19

4.1 The Need for Formal Methods in Quantum Computing 20

4.2 Typology of Properties to Verify 20

4.2.1 Functional Specifications 20

4.2.2 Complexity specifications 21

4.2.3 Structural Constraints 21

4.2.4 Circuit Equivalence 22

5 Low-Level Verification: Compilation and Equivalence 23

5.1 ZX-Calculus and Quantomatic/PyZX 23

5.1.1 Semantical Model 23

5.1.2 Verified Properties 25

5.1.3 Algorithms and Tools 28

5.2 Path-Sum circuit Equivalence Verification 28

5.2.1 Semantical Model 28

5.2.2 Path-Sums Reduction 29

5.2.3 Verified Properties 30

5.3 Quantum abstract interpretation 30

5.4 Toward Integrated Verified Optimization: VOQC 31

5.4.1 Architecture 31

5.4.2 Optimization Procedure 32

5.5 Formally verified quantum compilation in an imperative setting: CertiQ 33
# Contents

1 Introduction 5

2 General Background in Quantum Computing 6

2.1 Hybrid Computational Model 7

2.1.1 Hybrid Circuit Model 7

2.1.2 Quantum Data Registers 7

2.1.3 Separable and Entangled States 9

2.1.4 Quantum Circuits 9

2.1.5 Quantum Matrix Semantics and density operators 10

2.1.6 Other Models for Quantum Computations 13

2.2 Algorithms 13

2.2.1 Quantum Algorithms and Complexity 13

2.2.2 Quantum Algorithm Design 14

2.3 Challenges for Quantum Computation 16

2.3.1 Destructive Measurement and Non-Determinism 16

2.3.2 Quantum Noise 16

2.3.3 Efficient Compilation on Constrained Hardware 17

3 General Background on Formal Methods 17

3.1 Introduction 17

3.2 Principles 18

3.3 The Formal Method Zoo 18

4 Overview of Formal Methods in Quantum Computing 19

4.1 The Need for Formal Methods in Quantum Computing 20

4.2 Typology of Properties to Verify 20

4.2.1 Functional Specifications 20

4.2.2 Complexity specifications 21

4.2.3 Structural Constraints 21

4.2.4 Circuit Equivalence 22

5 Low-Level Verification: Compilation and Equivalence 23

5.1 ZX-Calculus and Quantomatic/PyZX 23

5.1.1 Semantical Model 23

5.1.2 Verified Properties 25

5.1.3 Algorithms and Tools 28

5.2 Path-Sum circuit Equivalence Verification 28

5.2.1 Semantical Model 28

5.2.2 Path-Sums Reduction 29

5.2.3 Verified Properties 30

5.3 Quantum abstract interpretation 30

5.4 Toward Integrated Verified Optimization: VOQC 31

5.4.1 Architecture 31

5.4.2 Optimization Procedure 32

5.5 Formally verified quantum compilation in an imperative setting: CertiQ 33
6 Formal Quantum Programming Languages 33

6.1 Quantum Programming Languages Design 33

6.1.1 Structure of Quantum Algorithms 33

6.1.2 Requirements for Quantum Programming Languages 35

6.1.3 Review of the Existing Approaches 35

6.2 Formalizing the Operational Semantics 37

6.2.1 Quantum Lambda-Calculi 37

6.2.2 Monadic Semantics 38

6.3 Type Systems 40

6.3.1 Quantum Data and Type Linearity 40

6.3.2 Example: Quantum Teleportation 41

6.3.3 Extending the Type System to Support Circuits 42

6.3.4 Dependent types and Proofs of Programs 43

6.3.5 Discussion 44

7 High and Mid-Level Verification: Algorithms and Programs 44

7.1 Quantum Hoare Logic 44

7.1.1 Quantum Programming Language: Quantum WHILE-Programs 45

7.1.2 Quantum States, Operations and Predicates 46

7.1.3 Quantum Program Verification 46

7.1.4 Implementations and Extensions 48

7.1.5 Other Quantum Hoare Logics 48

Quantum Hoare Logic with ghost variables. 49

Quantum Hoare Logic with classical variables. 49

Robustness analysis 49

Quantum separation logic 49

Quantum relational Hoare logic 50

Quantum Hoare type theory 50

Quantum dynamic logic. 50

7.2 QBRICKS 51

7.2.1 Writing Quantum Circuits Functions in QBRICKS: QBRICKS-DSL 51

7.2.2 Parametrized Path-Sums 52

7.2.3 From Quantum Circuits to Path-Sums 53

7.2.4 Probabilistic Reasoning 53

7.2.5 Verified Properties 53

7.2.6 Deduction and Proof Support. 54

7.2.7 Implementation and Case Studies 54

7.3 SQIR 55

7.3.1 Programming Language 55

7.3.2 Matrix Semantics and Specifications 56

7.3.3 Implementation and Case Studies 56

7.3.4 Comparison Between QBRICKS and SQIR 56

7.4 Conclusion about Formal Verification of Quantum Programs 57
6 Formal Quantum Programming Languages 33

6.1 Quantum Programming Languages Design 33

6.1.1 Structure of Quantum Algorithms 33

6.1.2 Requirements for Quantum Programming Languages 35

6.1.3 Review of the Existing Approaches 35

6.2 Formalizing the Operational Semantics 37

6.2.1 Quantum Lambda-Calculi 37

6.2.2 Monadic Semantics 38

6.3 Type Systems 40

6.3.1 Quantum Data and Type Linearity 40

6.3.2 Example: Quantum Teleportation 41

6.3.3 Extending the Type System to Support Circuits 42

6.3.4 Dependent types and Proofs of Programs 43

6.3.5 Discussion 44

7 High and Mid-Level Verification: Algorithms and Programs 44

7.1 Quantum Hoare Logic 44

7.1.1 Quantum Programming Language: Quantum WHILE-Programs 45

7.1.2 Quantum States, Operations and Predicates 46

7.1.3 Quantum Program Verification 46

7.1.4 Implementations and Extensions 48

7.1.5 Other Quantum Hoare Logics 48

Quantum Hoare Logic with ghost variables. 49

Quantum Hoare Logic with classical variables. 49

Robustness analysis 49

Quantum separation logic 49

Quantum relational Hoare logic 50

Quantum Hoare type theory 50

Quantum dynamic logic. 50

7.2 QBRICKS 51

7.2.1 Writing Quantum Circuits Functions in QBRICKS: QBRICKS-DSL 51

7.2.2 Parametrized Path-Sums 52

7.2.3 From Quantum Circuits to Path-Sums 53

7.2.4 Probabilistic Reasoning 53

7.2.5 Verified Properties 53

7.2.6 Deduction and Proof Support. 54

7.2.7 Implementation and Case Studies 54

7.3 SQIR 55

7.3.1 Programming Language 55

7.3.2 Matrix Semantics and Specifications 56

7.3.3 Implementation and Case Studies 56

7.3.4 Comparison Between QBRICKS and SQIR 56

7.4 Conclusion about Formal Verification of Quantum Programs 57
<table><tr><td><b>8</b></td><td><b>Discussion and Bibliographical Notes</b></td><td><b>58</b></td></tr><tr><td>8.1</td><td>Deductive Verification</td><td>58</td></tr><tr><td>8.2</td><td>Model Checking</td><td>58</td></tr><tr><td>8.3</td><td>Type Checking</td><td>58</td></tr><tr><td>8.4</td><td>Runtime assertion Checking</td><td>59</td></tr><tr><td>8.5</td><td>Verification of Quantum Communication Protocols</td><td>60</td></tr><tr><td><b>9</b></td><td><b>Conclusion</b></td><td><b>60</b></td></tr><tr><td>9.1</td><td>Summary</td><td>60</td></tr><tr><td>9.2</td><td>Main Current Challenges</td><td>61</td></tr></table>
<table><tr><td><b>8</b></td><td><b>Discussion and Bibliographical Notes</b></td><td><b>58</b></td></tr><tr><td>8.1</td><td>Deductive Verification</td><td>58</td></tr><tr><td>8.2</td><td>Model Checking</td><td>58</td></tr><tr><td>8.3</td><td>Type Checking</td><td>58</td></tr><tr><td>8.4</td><td>Runtime assertion Checking</td><td>59</td></tr><tr><td>8.5</td><td>Verification of Quantum Communication Protocols</td><td>60</td></tr><tr><td><b>9</b></td><td><b>Conclusion</b></td><td><b>60</b></td></tr><tr><td>9.1</td><td>Summary</td><td>60</td></tr><tr><td>9.2</td><td>Main Current Challenges</td><td>61</td></tr></table>
# 1 Introduction

**Cryptography and quantum information.** Quantum computing dates back to 1982, when Richard Feynman raised the idea [69] of simulating quantum mechanics phenomena by storing information in particles and controlling them according to the laws of quantum mechanics. In the brief history of quantum computing, the description in 1994 by Peter Shor of an algorithm [174], performing the decomposition of prime integers in polynomial time on the size of the input, plays a major role. Indeed, it was the first-ever described quantum algorithm with a practical utility-breaking the RSA public key cryptosystems in a tractable manner.

In an asymmetric cryptosystem such as RSA, information is encrypted via a key that is a solution for a given mathematical function—the decomposition of a given integer into prime factors for the case of RSA. The security of such a protocol is based on the fundamental assumption that no potential eavesdropper has the means to compute this solution efficiently. Shor's algorithm is based on (1) a reduction of the prime factor decomposition problem into the *order-finding* problem and (2) an adequate use of quantum parallelism to perform modular exponentiation of integers over many different inputs in a single row, enabling a polynomial resolution of the *order-finding*. Thus, the computation time for performing the prime decomposition is reduced from exponential to polynomial, and therefore breaks RSA's fundamental assumption. Shor's original article [174] also presents a variation of the order-finding resolution algorithm, solving the discrete logarithm problem with similar performances. Doing so, it brings a procedure for breaking elliptic curve cryptosystems.

Symmetric-key cryptosystems are also challenged by quantum computing [163]. As an example, Simon's quantum algorithm [176] brings an exponential speedup for computing the period of a function (given the promise that this period indeed exists). Several applications in public-key cryptosystems were described, providing exponential gain in, e.g., distinguishing a three-round Feistel construction [118, 163], key recovering in the Evan Mansour encryption scheme [119] and attacking the CBC-MAC message authentication scheme [163].

Finally, Grover search quantum algorithm [84] brings a quadratic speedup in the search for a distinguished element in unstructured databases. Hence, while in this case the complexity gain is less decisive than for the procedures introduced above, its potential for cryptography is significant as it weakens any symmetric-key encryption system.

Thus, quantum computing challenges current cryptographic uses and practices. Shor's algorithm opened a research program for cryptographic solutions resisting the power of quantum computation, called *post-quantum cryptography* [39].

Interestingly the induced challenge also received answers from quantum information theory itself. Indeed, one of the major distinctive features of quantum information is that it cannot be read without being affected. This entails that an eavesdropper trying to access a quantum information exchange cannot help betraying her attempt. Based on this feature, one can encode a cryptographic key in a quantum message and, in case of eavesdropping, detect it a *posteriori*, renounce this particular key and try another sending. The study of *Quantum key distribution protocols* is an active research area [164, 22, 128, 134].

**Quantum computing and quantum software.** These cryptographic aspects are one of many applications studied in the young research field of quantum computing. Others are, e.g., machine learning [26, 166, 133], optimization [64], solving linear systems [87], etc. In all these domains there are quantum algorithms beating the best known classical algorithms by quadratic or even exponential factors, complexity-wise.

These algorithms are based on laws and phenomena specific to quantum mechanics (such as quantum superposition, entanglement, unitary operations). Therefore, implementing them requires
# 1 Introduction

**Cryptography and quantum information.** Quantum computing dates back to 1982, when Richard Feynman raised the idea [69] of simulating quantum mechanics phenomena by storing information in particles and controlling them according to the laws of quantum mechanics. In the brief history of quantum computing, the description in 1994 by Peter Shor of an algorithm [174], performing the decomposition of prime integers in polynomial time on the size of the input, plays a major role. Indeed, it was the first-ever described quantum algorithm with a practical utility-breaking the RSA public key cryptosystems in a tractable manner.

In an asymmetric cryptosystem such as RSA, information is encrypted via a key that is a solution for a given mathematical function—the decomposition of a given integer into prime factors for the case of RSA. The security of such a protocol is based on the fundamental assumption that no potential eavesdropper has the means to compute this solution efficiently. Shor's algorithm is based on (1) a reduction of the prime factor decomposition problem into the *order-finding* problem and (2) an adequate use of quantum parallelism to perform modular exponentiation of integers over many different inputs in a single row, enabling a polynomial resolution of the *order-finding*. Thus, the computation time for performing the prime decomposition is reduced from exponential to polynomial, and therefore breaks RSA's fundamental assumption. Shor's original article [174] also presents a variation of the order-finding resolution algorithm, solving the discrete logarithm problem with similar performances. Doing so, it brings a procedure for breaking elliptic curve cryptosystems.

Symmetric-key cryptosystems are also challenged by quantum computing [163]. As an example, Simon's quantum algorithm [176] brings an exponential speedup for computing the period of a function (given the promise that this period indeed exists). Several applications in public-key cryptosystems were described, providing exponential gain in, e.g., distinguishing a three-round Feistel construction [118, 163], key recovering in the Evan Mansour encryption scheme [119] and attacking the CBC-MAC message authentication scheme [163].

Finally, Grover search quantum algorithm [84] brings a quadratic speedup in the search for a distinguished element in unstructured databases. Hence, while in this case the complexity gain is less decisive than for the procedures introduced above, its potential for cryptography is significant as it weakens any symmetric-key encryption system.

Thus, quantum computing challenges current cryptographic uses and practices. Shor's algorithm opened a research program for cryptographic solutions resisting the power of quantum computation, called *post-quantum cryptography* [39].

Interestingly the induced challenge also received answers from quantum information theory itself. Indeed, one of the major distinctive features of quantum information is that it cannot be read without being affected. This entails that an eavesdropper trying to access a quantum information exchange cannot help betraying her attempt. Based on this feature, one can encode a cryptographic key in a quantum message and, in case of eavesdropping, detect it a *posteriori*, renounce this particular key and try another sending. The study of *Quantum key distribution protocols* is an active research area [164, 22, 128, 134].

**Quantum computing and quantum software.** These cryptographic aspects are one of many applications studied in the young research field of quantum computing. Others are, e.g., machine learning [26, 166, 133], optimization [64], solving linear systems [87], etc. In all these domains there are quantum algorithms beating the best known classical algorithms by quadratic or even exponential factors, complexity-wise.

These algorithms are based on laws and phenomena specific to quantum mechanics (such as quantum superposition, entanglement, unitary operations). Therefore, implementing them requires
a framework consisting of both a *dedicated hardware* (quantum computers) and a *dedicated software* (quantum programming languages and compilation toolchains).

In the last 20 years, several such languages have been proposed, such as QISKIT [153], Liqui|〉 [193], Q# [181], Quipper [83], PROJECTQ [180], etc. Still, the field is in its infancy, and many questions still need to be answered before we can reach the level of maturity observed for classic programming languages. Standing questions include, for example, introducing a foundational computing model and semantics for quantum programming languages, adequate programming abstractions and type systems, or the ability to interact with severely constrained hardware in an efficient way (optimizing compilers).

**Verification of quantum programs.** While testing and debugging are the common verification practice in classical programming, they become extremely complicated in the quantum case. Indeed, debugging and assertion checking are a priori very complicated due to the destructive aspects of quantum measurement (see Section 2.3.1 below). Moreover, the probabilistic nature of quantum algorithms seriously impedes system-level quantum testing. Finally, classical emulation of quantum algorithms is (strongly believed to be) intractable.

On the other hand, nothing prevents a priori the formal verification [44] of quantum programs, i.e. proving by (more or less) automated reasoning methods that a given quantum program behaves as expected for any input, or at least that it is free from certain classes of bugs.

*Interestingly, while formal methods were first developed for the classical case where they are still used with parsimony—mainly for safety-critical domains—as testing remains the main validation methods, their application to quantum computing could become more mainstream, due to the inherent difficulties of testing quantum programs.*

**Goal of this survey** This survey introduces both the requirements and challenges for formal methods in quantum programs specification and verification, and the existing propositions to overcome these challenges.

The first sections give the general background. In Section 2 we introduce the main concepts at stake with quantum computing and quantum algorithms. We provide a state of the art introduction for formal methods, given in Section 3. The specific requirements for formal reasoning in the quantum case are then developed in Section 4. Then we come to concrete quantum programming and formal verification material. In Section 5 we introduce several existing solutions for the formal verification of quantum compilation and the equivalence of quantum program runs. Generating such runs requires specific programming languages. The formal interpretation of quantum languages is introduced in Section 6. Then in Section 7 we present the main existing solutions for formally verified quantum programming languages. In Section 8 we introduce references for further usage of formal methods linked with quantum information, and we conclude this survey with a discussion in Section 9.

## 2 General Background in Quantum Computing

By many aspects, quantum computing constitutes a new paradigm. Making great use of quantum superposition and quantum entanglement, it requires to define proper versions for such fundamental concepts as data structures at stake in computation, or the elementary logical operations at use. We introduce the well-known hybrid quantum computation model in Section 2.1.
a framework consisting of both a *dedicated hardware* (quantum computers) and a *dedicated software* (quantum programming languages and compilation toolchains).

In the last 20 years, several such languages have been proposed, such as QISKIT [153], Liqui|〉 [193], Q# [181], Quipper [83], PROJECTQ [180], etc. Still, the field is in its infancy, and many questions still need to be answered before we can reach the level of maturity observed for classic programming languages. Standing questions include, for example, introducing a foundational computing model and semantics for quantum programming languages, adequate programming abstractions and type systems, or the ability to interact with severely constrained hardware in an efficient way (optimizing compilers).

**Verification of quantum programs.** While testing and debugging are the common verification practice in classical programming, they become extremely complicated in the quantum case. Indeed, debugging and assertion checking are a priori very complicated due to the destructive aspects of quantum measurement (see Section 2.3.1 below). Moreover, the probabilistic nature of quantum algorithms seriously impedes system-level quantum testing. Finally, classical emulation of quantum algorithms is (strongly believed to be) intractable.

On the other hand, nothing prevents a priori the formal verification [44] of quantum programs, i.e. proving by (more or less) automated reasoning methods that a given quantum program behaves as expected for any input, or at least that it is free from certain classes of bugs.

*Interestingly, while formal methods were first developed for the classical case where they are still used with parsimony–mainly for safety-critical domains–as testing remains the main validation methods, their application to quantum computing could become more mainstream, due to the inherent difficulties of testing quantum programs.*

**Goal of this survey** This survey introduces both the requirements and challenges for formal methods in quantum programs specification and verification, and the existing propositions to overcome these challenges.

The first sections give the general background. In Section 2 we introduce the main concepts at stake with quantum computing and quantum algorithms. We provide a state of the art introduction for formal methods, given in Section 3. The specific requirements for formal reasoning in the quantum case are then developed in Section 4. Then we come to concrete quantum programming and formal verification material. In Section 5 we introduce several existing solutions for the formal verification of quantum compilation and the equivalence of quantum program runs. Generating such runs requires specific programming languages. The formal interpretation of quantum languages is introduced in Section 6. Then in Section 7 we present the main existing solutions for formally verified quantum programming languages. In Section 8 we introduce references for further usage of formal methods linked with quantum information, and we conclude this survey with a discussion in Section 9.

## 2 General Background in Quantum Computing

By many aspects, quantum computing constitutes a new paradigm. Making great use of quantum superposition and quantum entanglement, it requires to define proper versions for such fundamental concepts as data structures at stake in computation, or the elementary logical operations at use. We introduce the well-known hybrid quantum computation model in Section 2.1.
Quantum computers are not intended to, and will not, replace classical ones. One should better
see the opening of a new field, with possibilities to solve new problems. Section 2.2 presents these
new problems and introduces quantum algorithms design.

As a new software technology, quantum computing comes with specific challenges and difficul-
ties. These specificities are closely related to the particular needs for formal reasoning in quantum
computing. They are introduced in Section 2.3.

**2.1 Hybrid Computational Model**

Let us first introduce the main concepts at stake in quantum programming. They concern the ar-
chitecture of quantum computers, the structure of quantum information and quantum programs, and
their formal interpretation.

**2.1.1 Hybrid Circuit Model**

The vast majority of quantum algorithms are described within the context of the *quantum co-
processor model* [113], i.e. an hybrid model where a *classical computer* controls a *quantum co-
processor* holding a quantum memory, as shown in Figure 1. In particular, the classical computer
performs control operations (**if...else** statements, loops, etc). The co-processor can apply a fixed set
of elementary operations (buffered as *quantum circuits*) to update and query (*measure*) the quantum
memory. Importantly, while measurement allows retrieving classical (probabilistic) information
from the quantum memory, it also modifies it (*destructive effect*).

<figure><img src="image_2.png" /><figcaption>Figure 1: Scheme of the hybrid model</figcaption></figure>

Major *quantum programming languages* such as Quipper [83], Liqui|〉[193], Q# [181], PRO-
JECTQ [180], SILQ [27], and the rich ecosystem of existing quantum programming frameworks
[154] follow this hybrid model.

**2.1.2 Quantum Data Registers**

The following paragraphs introduce several definitions and notations for quantum data registers. In
particular, we follow the standard *Dirac notation*. For more details about this content, we refer the
reader to the standard literature [140].

**Kets and basis-kets.** While in classical computing the state of a bit is one between two possible states (0 or 1), in quantum computing the state of a *quantum bit* (or *qubit*) is described by *amplitudes* over the two elementary values 0 and 1 (denoted $|0⟩$ and $|1⟩$), i.e. linear combinations of vectors $α_0|0⟩ + α_1|1⟩$ where $α_0$ and $α_1$ are any *complex values* satisfying $|α_0|^2 + |α_1|^2 = 1$. In a sense, amplitudes are generalization of probabilities.
Quantum computers are not intended to, and will not, replace classical ones. One should better
see the opening of a new field, with possibilities to solve new problems. Section 2.2 presents these
new problems and introduces quantum algorithms design.

As a new software technology, quantum computing comes with specific challenges and difficul-
ties. These specificities are closely related to the particular needs for formal reasoning in quantum
computing. They are introduced in Section 2.3.

**2.1 Hybrid Computational Model**

Let us first introduce the main concepts at stake in quantum programming. They concern the ar-
chitecture of quantum computers, the structure of quantum information and quantum programs, and
their formal interpretation.

**2.1.1 Hybrid Circuit Model**

The vast majority of quantum algorithms are described within the context of the *quantum co-
processor model* [113], i.e. an hybrid model where a *classical computer* controls a *quantum co-
processor* holding a quantum memory, as shown in Figure 1. In particular, the classical computer
performs control operations (**if ... else** statements, loops, etc). The co-processor can apply a fixed set
of elementary operations (buffered as *quantum circuits*) to update and query (**measure**) the quantum
memory. Importantly, while measurement allows retrieving classical (probabilistic) information
from the quantum memory, it also modifies it (*destructive effect*).

<figure><img src="image_2.png" /><figcaption>Figure 1: Scheme of the hybrid model</figcaption></figure>

Major *quantum programming languages* such as Quipper [83], Liqui|〉[193], Q# [181], PRO-
JECTQ [180], SILQ [27], and the rich ecosystem of existing quantum programming frameworks
[154] follow this hybrid model.

**2.1.2 Quantum Data Registers**

The following paragraphs introduce several definitions and notations for quantum data registers. In
particular, we follow the standard *Dirac notation*. For more details about this content, we refer the
reader to the standard literature [140].

**Kets and basis-kets.** While in classical computing the state of a bit is one between two possible states (0 or 1), in quantum computing the state of a *quantum bit* (or *qubit*) is described by *amplitudes* over the two elementary values 0 and 1 (denoted $|0⟩$ and $|1⟩$), i.e. linear combinations of vectors $α_0|0⟩ + α_1|1⟩$ where $α_0$ and $α_1$ are any *complex values* satisfying $|α_0|^2 + |α_1|^2 = 1$. In a sense, amplitudes are generalization of probabilities.
More generally, quantum states are defined in complex finite-dimensional Hilbert spaces<fnref n="1" />: the state of a qubit register of n qubits (called a ket of length n-dimension 2ⁿ) is a column vector with 2ⁿ rows, formed as a superposition of the 2ⁿ elementary basis vectors of length n (the “basis kets”), i.e. a ket is any linear combination of the form

$$|u\rangle_n = \sum_{k=0}^{2^n-1} \alpha_k |k\rangle_n \qquad (1)$$

such that $\sum_{k=0}^{2^n-1} |\alpha_k|^2 = 1$.

**Bit-vectors and basis kets.** Depending on the context, it may be more convenient to index the terms in the sum above with bit vectors instead of integers. We call bit vector of length n any sequence $x_0x_1...x_{n-1}$ of elements in $\{0,1\}$. Along this survey, we assume the implicit casting of these values to/from booleans (with the least significant bit on the right). For any positive n, we denote the set of bit vectors of size n by $BV_n$. We also surcharge notation $|j\rangle_n$ shown above with bit vector inputs. Formally, for any bitvector $\vec{x}$ of length n, $|\vec{x}\rangle_n = |\sum_{i=0}^{n-1} x_i * 2^{n-i-1}\rangle_n$. Hence, one can write state $|u\rangle_n$ from (1) as

$$|u\rangle_n = \sum_{\vec{x} \in BV_n} \alpha_{\sum_{i=0}^{n-1} x_i \cdot 2^{n-i-1}} |\vec{x}\rangle_n$$

It may also be convenient to represent basis kets through their index's binary writing. For example, the two qubits kets basis is equivalently given as $\{|0\rangle_2, |1\rangle_2, |2\rangle_2, |3\rangle_2\}$ or as $\{|00\rangle, |01\rangle, |10\rangle, |11\rangle\}$.

We omit the length index n from notation $|u\rangle_n$ when it is either obvious from the context or irrelevant. We also adopt the implicit convention of writing basis kets with either integer indexes k, i, j or bit-vector $\vec{x}$ and general kets with indexes u, v, w. Hence, in the following $|u\rangle$, $|v\rangle$, $|i\rangle$ and $|\vec{x}\rangle$ all designate kets, the last two having the additional characteristics of being basis kets.

When considering two registers of respective size m and n, the state of the compound system lives in the Kronecker product<fnref n="2" />—or tensor product—of the original state spaces: a general state is then of the form

$$\sum_{\vec{x} \in BV_m, \vec{y} \in BV_n} \alpha_{\vec{x}, \vec{y}} |\vec{x}\rangle_m \otimes |\vec{y}\rangle_n.$$

In particular, the state of a qubit register of n qubits lives in the tensor product of n state-spaces of one single qubit.

**Adjointness.** In the following we also use the adjoint transformation for matrices. The adjoint of matrix M with r rows and c columns is the matrix $M^\dagger$, with c rows and r columns and such that for any indexes j, k ∈ [0, c] × [0, r] [3], cell $M^\dagger(j, k)$ holds the conjugate value $M(k, j)^*$ of $M(k, j)$ (for any complex number c, its conjugate $c^*$ is the complex number with the same real part and the opposite imaginary part as c). The adjoint of a ket $|u\rangle_n$ is called a bra. It is a row vector with 2ⁿ columns denoted $\langle u|_n$—or simply $\langle u|$—and with indices the conjugates of those of $|u\rangle_n$. This bra-ket notation is particularly convenient for representing operations over vectors. Given a ket $|u\rangle$ and a bra $\langle v|$,

<footnote n="1">¹In the finite-dimensional case, Hilbert spaces are vector spaces equipped with an inner (scalar) product.</footnote>

<footnote n="2">²Given two matrices A (with r rows and c columns) and B, their Kronecker product is the matrix $A \otimes B = \begin{pmatrix} a_{11}B & \dots & a_{1c}B \\ \vdots & \ddots & \vdots \\ a_{r1}B & \dots & a_{rc}B \end{pmatrix}$. This operation is central in quantum information representation. It enjoys a number of useful algebraic properties such as associativity, bilinearity or the equality $(A \otimes B) \cdot (C \otimes D) = (A \cdot C) \otimes (B \cdot D)$, where · denotes matrix multiplication.</footnote>

<footnote n="3">³where, for any two integers i, j with $i < j$, $\llbracket i, j \rrbracket$ denote the induced interval, that is the set of integers k such that $i \le k < j$.</footnote>
More generally, quantum states are defined in complex finite-dimensional Hilbert spaces<fnref n="1" />: the state of a qubit register of n qubits (called a ket of length n-dimension 2ⁿ) is a column vector with 2ⁿ rows, formed as a superposition of the 2ⁿ elementary basis vectors of length n (the “basis kets”), i.e. a ket is any linear combination of the form

$$|u\rangle_n = \sum_{k=0}^{2^n-1} \alpha_k |k\rangle_n \qquad (1)$$

such that $\sum_{k=0}^{2^n-1} |\alpha_k|^2 = 1$.

**Bit-vectors and basis kets.** Depending on the context, it may be more convenient to index the terms in the sum above with bit vectors instead of integers. We call bit vector of length n any sequence $x_0x_1...x_{n-1}$ of elements in $\{0,1\}$. Along this survey, we assume the implicit casting of these values to/from booleans (with the least significant bit on the right). For any positive n, we denote the set of bit vectors of size n by $BV_n$. We also surcharge notation $|j\rangle_n$ shown above with bit vector inputs. Formally, for any bitvector $\vec{x}$ of length n, $|\vec{x}\rangle_n = |\sum_{i=0}^{n-1} x_i * 2^{n-i-1}\rangle_n$. Hence, one can write state $|u\rangle_n$ from (1) as

$$|u\rangle_n = \sum_{\vec{x} \in BV_n} \alpha_{\sum_{i=0}^{n-1} x_i \cdot 2^{n-i-1}} |\vec{x}\rangle_n$$

It may also be convenient to represent basis kets through their index's binary writing. For example, the two qubits kets basis is equivalently given as $\{|0\rangle_2, |1\rangle_2, |2\rangle_2, |3\rangle_2\}$ or as $\{|00\rangle, |01\rangle, |10\rangle, |11\rangle\}$.

We omit the length index n from notation $|u\rangle_n$ when it is either obvious from the context or irrelevant. We also adopt the implicit convention of writing basis kets with either integer indexes k, i, j or bit-vector $\vec{x}$ and general kets with indexes u, v, w. Hence, in the following $|u\rangle$, $|v\rangle$, $|i\rangle$ and $|\vec{x}\rangle$ all designate kets, the last two having the additional characteristics of being basis kets.

When considering two registers of respective size m and n, the state of the compound system lives in the Kronecker product<fnref n="2" />—or tensor product—of the original state spaces: a general state is then of the form

$$\sum_{\vec{x} \in BV_m, \vec{y} \in BV_n} \alpha_{\vec{x}, \vec{y}} |\vec{x}\rangle_m \otimes |\vec{y}\rangle_n.$$

In particular, the state of a qubit register of n qubits lives in the tensor product of n state-spaces of one single qubit.

**Adjointness.** In the following we also use the adjoint transformation for matrices. The adjoint of matrix M with r rows and c columns is the matrix $M^\dagger$, with c rows and r columns and such that for any indexes j, k ∈ [0, c] × [0, r], cell $M^\dagger(j, k)$ holds the conjugate value $M(k, j)^*$ of M(k, j) (for any complex number c, its conjugate $c^*$ is the complex number with the same real part and the opposite imaginary part as c). The adjoint of a ket $|u\rangle_n$ is called a bra. It is a row vector with 2ⁿ columns denoted $\langle u|_n$-or simply $\langle u|$-and with indices the conjugates of those of $|u\rangle_n$. This bra-ket notation is particularly convenient for representing operations over vectors. Given a ket $|u\rangle$ and a bra $\langle v|$,

<footnote n="1">¹In the finite-dimensional case, Hilbert spaces are vector spaces equipped with an inner (scalar) product.</footnote>

<footnote n="2">²Given two matrices A (with r rows and c columns) and B, their Kronecker product is the matrix $A \otimes B = \begin{pmatrix} a_{11}B & \dots & a_{1c}B \\ \vdots & \ddots & \vdots \\ a_{r1}B & \dots & a_{rc}B \end{pmatrix}$. This operation is central in quantum information representation. It enjoys a number of useful algebraic properties such as associativity, bilinearity or the equality $(A \otimes B) \cdot (C \otimes D) = (A \cdot C) \otimes (B \cdot D)$, where · denotes matrix multiplication.</footnote>

<footnote n="3">³where, for any two integers i, j with $i < j$, $\llbracket i, j \rrbracket$ denote the induced interval, that is the set of integers k such that $i \le k < j$.</footnote>
$|u\rangle\langle v|$ denotes their Kronecker product –or outer product. Furthermore, if $|u\rangle$ and $\langle v|$ have the same length, then $\langle v|u\rangle$ denotes their scalar product–also called inner product. In particular, in the case of basis states $|i\rangle$ and $\langle j|$, $\langle i|j\rangle = 1$ if $i = j$ and 0 otherwise and $|i\rangle\langle j|$ is the square matrix of width $2^n$ with null coefficient everywhere except for cell $(i, j)$ with coefficient 1. If $i = j$, then $|i\rangle\langle j|$ operates as the projector upon $|i\rangle$.

**Quantum measurement and Born rule.** The probabilistic law for measurement of kets is given by the so-called *Born rule*: for any $k \in \mathbb{N}, 2^n \le k$, measuring state $|u\rangle_n$ from Equation 1 results in $k$ with probability $|\alpha_k|^2$. The measurement is destructive: if the result were $k$, the state of the register is now $|k\rangle_n$ (with amplitude 1).

### 2.1.3 Separable and Entangled States

From Section 2.1.2, a quantum state vector of length $n$ is a superposition of basis elements with coefficients whose squared moduli sum to one. Then, tensoring $n$ quantum states $|u_j\rangle_1$ of length 1 results in a state $|u\rangle_n = \bigotimes_{j \in \{0,n\}} |u_j\rangle_1$ of length $n$. One can decompose back $|u\rangle_n$ into the family $\{|u_j\rangle\}_{j \in \{0,n\}}$: we say that $|u\rangle_n$ is a separable state. Note that the structure of quantum information introduced above contains states missing the property of being separable. As an example, the state

$$|\beta_{00}\rangle = \frac{1}{\sqrt{2}}(|00\rangle + |11\rangle)$$

cannot be written as a tensor product of two single-qubit states. This phenomenon is called entanglement, and $|\beta_{00}\rangle$ is an entangled state. It induces that one can store more quantum information in $n$ qubits altogether than separately.

**Example 2.1 (Bell states).** State $|\beta_{00}\rangle$ is a construction of particular interest in quantum mechanics and quantum computing. In their famous 1935 article [62], Einstein, Podolsky and Rosen argued for the incompleteness of quantum mechanics, based on considerations upon $|\beta_{00}\rangle$. In 1964 [21], J.S. Bell proposed an experiment to test the argument. It was based on statistics over experiments on the four following states:

$$ \begin{aligned} |\beta_{00}\rangle &= \frac{1}{\sqrt{2}}(|00\rangle_2 + |11\rangle_2) & |\beta_{01}\rangle &= \frac{1}{\sqrt{2}}(|01\rangle_2 + |10\rangle_2) \\ |\beta_{10}\rangle &= \frac{1}{\sqrt{2}}(|00\rangle_2 - |11\rangle_2) & |\beta_{11}\rangle &= \frac{1}{\sqrt{2}}(|01\rangle_2 - |10\rangle_2) \end{aligned} $$

These four states are now known as the Bell states (notation $\beta$ stands for the initial B) and are used in many quantum protocols, such as teleportation or superdense coding (see Section 5.1). We use them and their generation as a running example in the rest of this survey.

### 2.1.4 Quantum Circuits

Three kinds of operations may be applied to quantum memory, exemplified in Figure 2 with the circuit generating and measuring Bell states:

* the initialization phase allocates and initializes quantum registers (arrays of qubits) from classical data. In Figure 2 it is represented on the two first qubit wires as $|–>$, indexed by value $i_w$. It creates a quantum register in one of the basis states (that is, in the case of a two-qubit register, in one of the four basis states $|00\rangle, |01\rangle, |10\rangle, |11\rangle$),
$|u\rangle\langle v|$ denotes their Kronecker product –or outer product. Furthermore, if $|u\rangle$ and $\langle v|$ have the same length, then $\langle v|u\rangle$ denotes their scalar product–also called inner product. In particular, in the case of basis states $|i\rangle$ and $\langle j|$, $\langle i|j\rangle = 1$ if $i = j$ and 0 otherwise and $|i\rangle\langle j|$ is the square matrix of width $2^n$ with null coefficient everywhere except for cell $(i, j)$ with coefficient 1. If $i = j$, then $|i\rangle\langle j|$ operates as the projector upon $|i\rangle$.

**Quantum measurement and Born rule.** The probabilistic law for measurement of kets is given by the so-called *Born rule*: for any $k \in \mathbb{N}, 2^n \le k$, measuring state $|u\rangle_n$ from Equation 1 results in $k$ with probability $|\alpha_k|^2$. The measurement is destructive: if the result were $k$, the state of the register is now $|k\rangle_n$ (with amplitude 1).

### 2.1.3 Separable and Entangled States

From Section 2.1.2, a quantum state vector of length $n$ is a superposition of basis elements with coefficients whose squared moduli sum to one. Then, tensoring $n$ quantum states $|u_j\rangle_1$ of length 1 results in a state $|u\rangle_n = \bigotimes_{j \in \{0,n\}} |u_j\rangle_1$ of length $n$. One can decompose back $|u\rangle_n$ into the family $\{|u_j\rangle\}_{j \in \{0,n\}}$: we say that $|u\rangle_n$ is a separable state. Note that the structure of quantum information introduced above contains states missing the property of being separable. As an example, the state

$$|\beta_{00}\rangle = \frac{1}{\sqrt{2}}(|00\rangle + |11\rangle)$$

cannot be written as a tensor product of two single-qubit states. This phenomenon is called entanglement, and $|\beta_{00}\rangle$ is an entangled state. It induces that one can store more quantum information in $n$ qubits altogether than separately.

**Example 2.1 (Bell states).** State $|\beta_{00}\rangle$ is a construction of particular interest in quantum mechanics and quantum computing. In their famous 1935 article [62], Einstein, Podolsky and Rosen argued for the incompleteness of quantum mechanics, based on considerations upon $|\beta_{00}\rangle$. In 1964 [21], J.S. Bell proposed an experiment to test the argument. It was based on statistics over experiments on the four following states:

$$ \begin{aligned} |\beta_{00}\rangle &= \frac{1}{\sqrt{2}}(|00\rangle_2 + |11\rangle_2) & |\beta_{01}\rangle &= \frac{1}{\sqrt{2}}(|01\rangle_2 + |10\rangle_2) \\ |\beta_{10}\rangle &= \frac{1}{\sqrt{2}}(|00\rangle_2 - |11\rangle_2) & |\beta_{11}\rangle &= \frac{1}{\sqrt{2}}(|01\rangle_2 - |10\rangle_2) \end{aligned} $$

These four states are now known as the Bell states (notation $\beta$ stands for the initial B) and are used in many quantum protocols, such as teleportation or superdense coding (see Section 5.1). We use them and their generation as a running example in the rest of this survey.

### 2.1.4 Quantum Circuits

Three kinds of operations may be applied to quantum memory, exemplified in Figure 2 with the circuit generating and measuring Bell states:

* the initialization phase allocates and initializes quantum registers (arrays of qubits) from classical data. In Figure 2 it is represented on the two first qubit wires as $|–>$, indexed by value $i_w$. It creates a quantum register in one of the basis states (that is, in the case of a two-qubit register, in one of the four basis states $|00\rangle, |01\rangle, |10\rangle, |11\rangle$),
* the actual quantum computing part consists in transforming an initialized state. This is performed by applying a sequence of proper quantum operations, structured in a so-called *quantum circuit*. In Figure 2 this part is identified with a dashed box (itself sequenced with dotted boxes a. and b.),

* the extraction of useful information from a quantum computation is performed through the *measurement* operation, by which one probabilistically gets classical data from the quantum memory register. Measurement is represented, on each qubit it is applied to, as $\otimes$.

* In generalized circuits, not all wires in a register need to be initialized and measured. Hence in Figure 2 the transformations are performed over the two first wires of a wider register, and the additional wires are left untouched.

<figure><img src="image_3.png" /><figcaption>Figure 2: Generalized circuit to create and measure Bell states</figcaption></figure>

*Note that we reserve the term circuit for the pure quantum part (the dashed box in Figure 2). We call generalized circuit a process made of a circuit together with, possibly, initialization and measurements.*

Quantum circuits are built by *combining*, either in *sequence* or in *parallel*, a given set of elementary operations called *quantum gates*. In addition to sequence and parallelism, derived circuit combinators (controls, reversion, ancillas, etc) are often used in quantum circuit design (See Figure 9 in Section 6.1.1 for details). The circuit part of Figure 2 uses two different quantum gates, drawn in dotted boxes:

* the Hadamard gate $H$ (a.), which induces a state superposition on a given qubit,

* the *control not* gate, often written $CNOT$ (b.) and represented as $\oplus$. It is a binary gate, flipping the *target qubit* (in wire 2 in our case) when the *control qubit* (wire 1) has value 1.

### 2.1.5 Quantum Matrix Semantics and density operators

The transformation operated by a quantum circuit on a quantum register is commonly interpreted as a matrix. In this setting, the parallel combination of circuits is interpreted by the *Kronecker product* and the sequential combination by the *matrix multiplication*.
* the actual quantum computing part consists in transforming an initialized state. This is performed by applying a sequence of proper quantum operations, structured in a so-called *quantum circuit*. In Figure 2 this part is identified with a dashed box (itself sequenced with dotted boxes a. and b.),

* the extraction of useful information from a quantum computation is performed through the *measurement* operation, by which one probabilistically gets classical data from the quantum memory register. Measurement is represented, on each qubit it is applied to, as $\otimes$.

* In generalized circuits, not all wires in a register need to be initialized and measured. Hence in Figure 2 the transformations are performed over the two first wires of a wider register, and the additional wires are left untouched.

<figure><img src="image_3.png" /><figcaption>Figure 2: Generalized circuit to create and measure Bell states</figcaption></figure>

*Note that we reserve the term circuit for the pure quantum part (the dashed box in Figure 2). We call generalized circuit a process made of a circuit together with, possibly, initialization and measurements.*

Quantum circuits are built by *combining*, either in *sequence* or in *parallel*, a given set of elementary operations called *quantum gates*. In addition to sequence and parallelism, derived circuit combinators (controls, reversion, ancillas, etc) are often used in quantum circuit design (See Figure 9 in Section 6.1.1 for details). The circuit part of Figure 2 uses two different quantum gates, drawn in dotted boxes:

* the Hadamard gate $H$ (a.), which induces a state superposition on a given qubit,

* the *control not* gate, often written $CNOT$ (b.) and represented as $\oplus$. It is a binary gate, flipping the *target qubit* (in wire 2 in our case) when the *control qubit* (wire 1) has value 1.

### 2.1.5 Quantum Matrix Semantics and density operators

The transformation operated by a quantum circuit on a quantum register is commonly interpreted as a matrix. In this setting, the parallel combination of circuits is interpreted by the *Kronecker product* and the sequential combination by the *matrix multiplication*.
**Quantum circuits.** Quantum circuits happen to operate as *unitary* operators (preserving the inner product between vectors). A set of elementary gates is (pseudo-) *universal* if, by a combination of parallel and sequential composition, one can synthesize (or approximate) all *unitary* operations. Examples for elementary gates are given in Table 1, with their matrix semantics interpretation. Apart from the already encountered gates *H* and *CNOT*, it features two additional families of gates, *Ph(θ)* and *R<sub>Z</sub>(θ)*, where *θ* is an angle inducing a so-called *phase factor* *e*<sup>*iθ*</sup>. *Ph(θ)* operates a simple scalar multiplication by a phase factor, while *R<sub>Z</sub>(θ)* operates as a rotation. Table 1 is given with indexes ranging over any angle *θ*, making the set of gates universal. Usually, we restrict it to angles of measure *π* / (2n), with *n* ranging over integers. This restriction makes the resulting set of gates pseudo-universal.

<table><caption>Table 1: Elementary gates and their matrix semantics</caption><thead><tr><th>H</th><th>CNOT</th><th>Ph(θ)</th><th>R<sub>Z</sub>(θ)</th></tr></thead><tbody><tr><td><sup>1</sup>&frasl;<sub>√2</sub> (<span style="font-size: 2em; vertical-align: middle;">(</span><table style="display: inline-table; vertical-align: middle; text-align: center; line-height: 1em; border: none; padding: 0.2em 0.5em;"><tbody><tr><td style="border: none; padding: 0.1em 0.2em;">1</td><td style="border: none; padding: 0.1em 0.2em;">1</td></tr><tr><td style="border: none; padding: 0.1em 0.2em;">1</td><td style="border: none; padding: 0.1em 0.2em;">-1</td></tr></tbody></table><span style="font-size: 2em; vertical-align: middle;">)</span>)</td><td><span style="font-size: 2em; vertical-align: middle;">(</span><table style="display: inline-table; vertical-align: middle; text-align: center; line-height: 1em; border: none; padding: 0.2em 0.5em;"><tbody><tr><td style="border: none; padding: 0.1em 0.2em;">1</td><td style="border: none; padding: 0.1em 0.2em;">0</td><td style="border: none; padding: 0.1em 0.2em;">0</td><td style="border: none; padding: 0.1em 0.2em;">0</td></tr><tr><td style="border: none; padding: 0.1em 0.2em;">0</td><td style="border: none; padding: 0.1em 0.2em;">1</td><td style="border: none; padding: 0.1em 0.2em;">0</td><td style="border: none; padding: 0.1em 0.2em;">0</td></tr><tr><td style="border: none; padding: 0.1em 0.2em;">0</td><td style="border: none; padding: 0.1em 0.2em;">0</td><td style="border: none; padding: 0.1em 0.2em;">0</td><td style="border: none; padding: 0.1em 0.2em;">1</td></tr><tr><td style="border: none; padding: 0.1em 0.2em;">0</td><td style="border: none; padding: 0.1em 0.2em;">0</td><td style="border: none; padding: 0.1em 0.2em;">1</td><td style="border: none; padding: 0.1em 0.2em;">0</td></tr></tbody></table><span style="font-size: 2em; vertical-align: middle;">)</span></td><td><span style="font-size: 2em; vertical-align: middle;">(</span><table style="display: inline-table; vertical-align: middle; text-align: center; line-height: 1em; border: none; padding: 0.2em 0.5em;"><tbody><tr><td style="border: none; padding: 0.1em 0.2em;">e<sup>*iθ*</sup></td><td style="border: none; padding: 0.1em 0.2em;">0</td></tr><tr><td style="border: none; padding: 0.1em 0.2em;">0</td><td style="border: none; padding: 0.1em 0.2em;">e<sup>*iθ*</sup></td></tr></tbody></table><span style="font-size: 2em; vertical-align: middle;">)</span></td><td><span style="font-size: 2em; vertical-align: middle;">(</span><table style="display: inline-table; vertical-align: middle; text-align: center; line-height: 1em; border: none; padding: 0.2em 0.5em;"><tbody><tr><td style="border: none; padding: 0.1em 0.2em;">e<sup>-*iθ*</sup></td><td style="border: none; padding: 0.1em 0.2em;">0</td></tr><tr><td style="border: none; padding: 0.1em 0.2em;">0</td><td style="border: none; padding: 0.1em 0.2em;">e<sup>*iθ*</sup></td></tr></tbody></table><span style="font-size: 2em; vertical-align: middle;">)</span></td></tr></tbody></table>

**Example 2.2** (Semantics for the Bell generating circuit). Let us look at Figure 2 again. First, an Hadamard gate is applied to the first wire and nothing happens to the second wire (it stays untouched, which is represented by the identity matrix). The matrix for the first column—the dotted box indexed with a.—of Figure 2 is

$$ \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix} \otimes \begin{pmatrix} 1 & 0 \\ 0 & 1 \end{pmatrix} = \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 0 & 1 & 0 \\ 0 & 1 & 0 & 1 \\ 1 & 0 & -1 & 0 \\ 0 & 1 & 0 & -1 \end{pmatrix} $$

Then gate CNOT is applied, with matrix $\begin{pmatrix} 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 \end{pmatrix}$ and the sequential combination of the two sub-circuits translates, in the matrix semantics, as their usual product (mind the reverse ordering, wrt the figure):

$$ \mathbf{Mat}(\text{Bell-circuit}) = \begin{pmatrix} 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 1 & 0 \\ 0 & 0 & 0 & 1 \end{pmatrix} \cdot \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 0 & 1 & 0 \\ 0 & 1 & 0 & 1 \\ 1 & 0 & -1 & 0 \\ 0 & 1 & 0 & -1 \end{pmatrix} = \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 0 & 1 & 0 \\ 0 & 1 & 0 & 1 \\ 0 & 1 & 0 & -1 \\ 1 & 0 & -1 & 0 \end{pmatrix} $$

**Application to input initialized kets.** In the matrix formalism, we interpret $|0\rangle$ as the column vector $(\begin{pmatrix} 1 \\ 0 \end{pmatrix})$, $|1\rangle$ as $(\begin{pmatrix} 0 \\ 1 \end{pmatrix})$ and the concatenation $|ij\rangle$, where *i* and *j* both are sequences of 0 or 1, as the Kronecker product $|i\rangle \otimes |j\rangle$. For example, the two qubits basis kets $|00\rangle$, $|01\rangle$, $|10\rangle$, $|11\rangle$ are represented, respectively, as

$$ (\begin{pmatrix} 1 \\ 0 \\ 0 \\ 0 \end{pmatrix}, \begin{pmatrix} 0 \\ 1 \\ 0 \\ 0 \end{pmatrix}, \begin{pmatrix} 0 \\ 0 \\ 1 \\ 0 \end{pmatrix}) \text{ and } (\begin{pmatrix} 0 \\ 0 \\ 0 \\ 1 \end{pmatrix}). $$

The transformation performed by a quantum circuit *C* upon a quantum state $|\psi\rangle$ is interpreted as the matrix product $\mathbf{Mat}(C) \cdot |\psi\rangle$ of the matrix for this circuit by the column vector for this quantum state. By notation abuse, we also simply write it $C|\psi\rangle$.

**Example 2.3.** One can now directly verify that the Bell generating circuit from Figure 2 generates the Bell states from Example 2.1: for any $a, b \in \{0, 1\}$,

$$ \text{Bell-circuit} \cdot |ab\rangle = |\beta_{ab}\rangle $$
**Quantum circuits.** Quantum circuits happen to operate as *unitary* operators (preserving the inner product between vectors). A set of elementary gates is (pseudo-) *universal* if, by a combination of parallel and sequential composition, one can synthesize (or approximate) all *unitary* operations. Examples for elementary gates are given in Table 1, with their matrix semantics interpretation. Apart from the already encountered gates *H* and *CNOT*, it features two additional families of gates, *Ph(θ)* and *Rz(θ)*, where *θ* is an angle inducing a so-called *phase factor* *e*<sup>*iθ*</sup>. *Ph(θ)* operates a simple scalar multiplication by a phase factor, while *Rz(θ)* operates as a rotation. Table 1 is given with indexes ranging over any angle *θ*, making the set of gates universal. Usually, we restrict it to angles of measure *π* / (2*n*), with *n* ranging over integers. This restriction makes the resulting set of gates pseudo-universal.

<table><caption>Table 1: Elementary gates and their matrix semantics</caption><thead><tr><th>H</th><th>CNOT</th><th>Ph(θ)</th><th>R<sub>Z</sub>(θ)</th></tr></thead><tbody><tr><td><sup>1</sup>&frasl;<sub>√2</sub> (<span style="text-decoration: overline;">1</span> 1)</td><td>(<span style="text-decoration: overline;">1</span> 0 0 0)</td><td>(<span style="text-decoration: overline;">e<sup>iθ</sup></span> 0)</td><td>(<span style="text-decoration: overline;">e<sup>-iθ</sup></span> 0)</td></tr><tr><td>1 &minus; 1</td><td>(0 1 0 0)</td><td>(0 <span style="text-decoration: overline;">e<sup>iθ</sup></span>)</td><td>(0 <span style="text-decoration: overline;">e<sup>iθ</sup></span>)</td></tr><tr><td></td><td>(0 0 0 1)</td><td></td><td></td></tr><tr><td></td><td>(0 0 1 0)</td><td></td><td></td></tr></tbody></table>

**Example 2.2** (Semantics for the Bell generating circuit). Let us look at Figure 2 again. First, an Hadamard gate is applied to the first wire and nothing happens to the second wire (it stays untouched, which is represented by the identity matrix). The matrix for the first column—the dotted box indexed with *a*—of Figure 2 is

$$ \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix} \otimes \begin{pmatrix} 1 & 0 \\ 0 & 1 \end{pmatrix} = \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 0 & 1 & 0 \\ 0 & 1 & 0 & 1 \\ 1 & 0 & -1 & 0 \\ 0 & 1 & 0 & -1 \end{pmatrix} $$

Then gate CNOT is applied, with matrix $\begin{pmatrix} 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 \end{pmatrix}$ and the sequential combination of the two sub-circuits translates, in the matrix semantics, as their usual product (mind the reverse ordering, wrt the figure):

$$ \mathbf{Mat}(\text{Bell-circuit}) = \begin{pmatrix} 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 1 & 0 \\ 0 & 0 & 0 & 1 \end{pmatrix} \cdot \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 0 & 1 & 0 \\ 0 & 1 & 0 & 1 \\ 1 & 0 & -1 & 0 \\ 0 & 1 & 0 & -1 \end{pmatrix} = \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 0 & 1 & 0 \\ 0 & 1 & 0 & 1 \\ 0 & 1 & 0 & -1 \\ 1 & 0 & -1 & 0 \end{pmatrix} $$

**Application to input initialized kets.** In the matrix formalism, we interpret $|0\rangle$ as the column vector $(\begin{pmatrix} 1 \\ 0 \end{pmatrix})$, $|1\rangle$ as $(\begin{pmatrix} 0 \\ 1 \end{pmatrix})$ and the concatenation $|ij\rangle$, where *i* and *j* both are sequences of 0 or 1, as the Kronecker product $|i\rangle \otimes |j\rangle$. For example, the two qubits basis kets $|00\rangle$, $|01\rangle$, $|10\rangle$, $|11\rangle$ are represented, respectively, as

$$(\begin{pmatrix} 1 \\ 0 \\ 0 \\ 0 \end{pmatrix}), (\begin{pmatrix} 0 \\ 1 \\ 0 \\ 0 \end{pmatrix}), (\begin{pmatrix} 0 \\ 0 \\ 1 \\ 0 \end{pmatrix}) \text{ and } (\begin{pmatrix} 0 \\ 0 \\ 0 \\ 1 \end{pmatrix}).$$

The transformation performed by a quantum circuit *C* upon a quantum state $|\psi\rangle$ is interpreted as the matrix product $\mathbf{Mat}(C) \cdot |\psi\rangle$ of the matrix for this circuit by the column vector for this quantum state. By notation abuse, we also simply write it $C|\psi\rangle$.

**Example 2.3.** One can now directly verify that the Bell generating circuit from Figure 2 generates the Bell states from Example 2.1: for any $a, b \in \{0, 1\}$,

$$ \text{Bell-circuit} \cdot |ab\rangle = |\beta_{ab}\rangle $$
**Measurement.** Last, measurement is performed over an orthonormal basis of the Hilbert space. For sake of simplicity, we only consider the case of measurements in the computational basis. Hence, measuring a quantum register results in a basis state, with probabilities following the Born rule introduced in Section 2.1.2: measuring any state $|u\rangle_n$ results in basis state $|k\rangle_n$ with probability (written $\text{proba\_measure}(|u\rangle_n, |k\rangle_n)$) $|\alpha_k|^2$, where $\alpha_k$ is the amplitude of $|k\rangle_n$ in $|u\rangle_n$. Applying this rule to the Bell state, one easily state that for any $a, b, i, j \in \{0, 1\}$,

$$ \text{proba\_measure}(|\beta_{ab}\rangle, |ij\rangle) = \frac{1}{2}(\text{if } b=0 \text{ then } i \oplus j \text{ else } 1-(i \oplus j)) $$

where $\oplus$ denotes addition modulo 2. Note, from Example 2.1, that index $a$ in notation $|\beta_{ab}\rangle$ only accounts for a $-1$ factor in the second term of the state superposition. Hence, since measurement is ruled by the Born rule and since this rule ignores negation (see Section 2.1.2), then index $a$ does not appear in the expression of $\text{proba\_measure}(|\beta_{ab}\rangle, |ij\rangle)$.

**Discussion over the matrix semantics.** Matrix semantics is the usual standard formalism for quantum computing (see [140] for example). Still, the size of matrices grows exponentially with the width (number of qubits) of circuits, so it is often cumbersome when addressing circuits from non-trivial algorithm instances. Furthermore, algorithms usually manipulate parametrized families of circuits. The resulting parametrized families of matrices may not be conveniently writable.

Hence, a more compact interpretation for quantum circuits may be helpful. In particular, path-sum semantics [5, 4] directly interprets quantum circuits by the input/output function they induce over kets-corresponding, in matrix terms, for any circuit $C$ of width $n$, to the function $|u\rangle_n \mapsto \text{Mat}(C) \cdot |u\rangle_n$. To do so, it exhibits a generic form for quantum registers description, which is generated by a restricted number of parameters and composes nicely with sequence and parallel compositions. Path-sum semantics plays a growing role in formal specification and verification. It is introduced with further details in Section 5.2.

**Density operators.** In the preceding paragraph, we introduced measurement as a non-deterministic operation over quantum states. Another strategy consists in dealing with a notion of states featuring this non-determinism. A mixed state (as opposed to a pure state) is a probability distribution over several states. Alternatively, it can be seen as an incomplete description of a state, featuring the incomplete knowledge one may have about it. Then, measurement can be characterized as a simple transition between mixed states.

In quantum processes, this view is formalized by density operators, that extends matrices formalism with the characterization of probabilistic states. For sake of brevity, in this paragraph we give only a short introduction to the density operator formalism. Our aim here is only to provide the required definitions and notations for this review. For further detail about density operators and for the related soundness proofs, we refer the interested reader either to [168] or [139] (Section 2.4).

Basically, the density operator for a pure state $|x\rangle$ is the reflexive outer product $|x\rangle\langle x|$. Given a set $S$ of indices and a distribution of states $\{|x_k\rangle\}_{k \in S}$, each occurring with probability $p_k$, we represent the overall mixed state as the density operator

$$ \rho := \sum_{k \in S} p_k |x_k\rangle\langle x_k| $$

By linearity, the result of applying a unitary $U$ to $|x\rangle\langle x|$ is given by the product $U|x\rangle\langle x|U^\dagger$. A measurement of a quantum register $q$ of size $n$ may be described by the collection of possible projectors it realizes, that is the set $M = \{M_k := |k\rangle_n \langle k|_n\}_{k \in [0, 2^{n-1}]}$.
**Measurement.** Last, measurement is performed over an orthonormal basis of the Hilbert space. For sake of simplicity, we only consider the case of measurements in the computational basis. Hence, measuring a quantum register results in a basis state, with probabilities following the Born rule introduced in Section 2.1.2: measuring any state $|u\rangle_n$ results in basis state $|k\rangle_n$ with probability (written $\text{proba\_measure}(|u\rangle_n, |k\rangle_n)$) $|\alpha_k|^2$, where $\alpha_k$ is the amplitude of $|k\rangle_n$ in $|u\rangle_n$. Applying this rule to the Bell state, one easily state that for any $a, b, i, j \in \{0, 1\}$,

$$ \text{proba\_measure}(|\beta_{ab}\rangle, |ij\rangle) = \frac{1}{2}(\text{if } b=0 \text{ then } i \oplus j \text{ else } 1-(i \oplus j)) $$

where $\oplus$ denotes addition modulo 2. Note, from Example 2.1, that index $a$ in notation $|\beta_{ab}\rangle$ only accounts for a $-1$ factor in the second term of the state superposition. Hence, since measurement is ruled by the Born rule and since this rule ignores negation (see Section 2.1.2), then index $a$ does not appear in the expression of $\text{proba\_measure}(|\beta_{ab}\rangle, |ij\rangle)$.

**Discussion over the matrix semantics.** Matrix semantics is the usual standard formalism for quantum computing (see [140] for example). Still, the size of matrices grows exponentially with the width (number of qubits) of circuits, so it is often cumbersome when addressing circuits from non-trivial algorithm instances. Furthermore, algorithms usually manipulate parametrized families of circuits. The resulting parametrized families of matrices may not be conveniently writable.

Hence, a more compact interpretation for quantum circuits may be helpful. In particular, path-sum semantics [5, 4] directly interprets quantum circuits by the input/output function they induce over kets-corresponding, in matrix terms, for any circuit $C$ of width $n$, to the function $|u\rangle_n \mapsto \text{Mat}(C) \cdot |u\rangle_n$. To do so, it exhibits a generic form for quantum registers description, which is generated by a restricted number of parameters and composes nicely with sequence and parallel compositions. Path-sum semantics plays a growing role in formal specification and verification. It is introduced with further details in Section 5.2.

**Density operators.** In the preceding paragraph, we introduced measurement as a non-deterministic operation over quantum states. Another strategy consists in dealing with a notion of states featuring this non-determinism. A mixed state (as opposed to a pure state) is a probability distribution over several states. Alternatively, it can be seen as an incomplete description of a state, featuring the incomplete knowledge one may have about it. Then, measurement can be characterized as a simple transition between mixed states.

In quantum processes, this view is formalized by density operators, that extends matrices formalism with the characterization of probabilistic states. For sake of brevity, in this paragraph we give only a short introduction to the density operator formalism. Our aim here is only to provide the required definitions and notations for this review. For further detail about density operators and for the related soundness proofs, we refer the interested reader either to [168] or [139] (Section 2.4).

Basically, the density operator for a pure state $|x\rangle$ is the reflexive outer product $|x\rangle\langle x|$. Given a set $S$ of indices and a distribution of states $\{|x_k\rangle\}_{k \in S}$, each occurring with probability $p_k$, we represent the overall mixed state as the density operator

$$ \rho := \sum_{k \in S} p_k |x_k\rangle\langle x_k| $$

By linearity, the result of applying a unitary $U$ to $|x\rangle\langle x|$ is given by the product $U|x\rangle\langle x|U^\dagger$. A measurement of a quantum register $q$ of size $n$ may be described by the collection of possible projectors it realizes, that is the set $M = \{M_k := |k\rangle_n \langle k|_n\}_{k \in [0, 2^{n-1}]}$.
the action of $\mathcal{M}$ over a state $\rho$ may result in any state $M_k \rho M_k^\dagger$, with probability $\text{tr}(M_k M_k^\dagger \rho)$, where the trace $\text{tr}(\mathcal{M})$ of a square matrix $\mathcal{M}$ with $n$ rows and columns is defined as the sum $\sum_{j \in [0, n]} M(j, j)$ of its diagonal cell values. Then, the overall action of a measurement $\mathcal{M}$ over a density operator $\rho$ results in $\rho' = \sum_{k \in [0, 2^{n-1}]} M_k \rho M_k^\dagger$.

Now, measurement description generalizes to the case of *partial measurements*, where only a sub-register is measured. Let us consider the case of a quantum register $q$ of size $n = n_1 + n_2$. We write $q_1$ and $q_2$ for the concatenated sub-registers and $H, H_1, H_2$ for the respectively induced Hilbert spaces. To simplify the notations we consider the case of measuring the first $n$ qubits. For any density operator $\rho$, if it is separable as $\rho = |x_1\rangle_n \langle y_1|_{n_1} \otimes |x_2\rangle_n \langle y_2|_{n_2}$, then the partial trace of $\rho$ over $H_2$ is defined as $\text{tr}_2(\rho) = \langle y_1|x_1\rangle \langle x_2|\langle y_2|$ and the definition generalizes by linearity to any density operator $\rho$. Then, $\text{tr}_2(\rho)$ equivalently represents the result of:

* (1) measuring register $q_2$ from the mixed state $\rho$ and (2) forgetting the measured qubits while conserving memory of the unmeasured subregister $q_1$ state;

* or just forgetting about (*discarding*) register $q_2$ in the description of $\rho$. Then, $\text{tr}_2(\rho)$ is the description of the sub-system held by $q_1$. We call $\text{tr}_2(\rho)$ a *partial density operator* on $H_1$.

### 2.1.6 Other Models for Quantum Computations

Many alternatives are currently explored for physical implementations of quantum computing machines and worth mentioning. Some of them (such as Measurement Based Quantum Computing [157, 32], topological quantum computations [76], linear optical networks [1], adiabatic quantum computing [65], etc.) differing on rather fundamental aspects (like, e.g., the elementary operations constituting computations). Nevertheless, currently, formal methods developments mainly address the standard circuit model introduced above.

The ZX-Calculus [47] also provides an alternative graphical formalism to reason about quantum processes. Basically, in this setting, quantum operations are represented by diagrams and their composition through sequence or parallelism corresponds to graphical compositions in the calculus. This language comes with a series of enabled transformations over graphs, preserving computational equivalence. ZX-Calculus is presented in Section 5.1.

## 2.2 Algorithms

As previously introduced, quantum computers are meant to perform calculations that classical computers are a priori not able to perform in a *reasonable* time. We give the formal complexity theory characterization for this point in Section 2.2.1, then Section 2.2.2 discusses the usual conventions for quantum algorithms descriptions.

### 2.2.1 Quantum Algorithms and Complexity

It is commonly assumed that formal problems are *tractable* by a computer if there exists an algorithm to solve this problem in time (measured by the number of elementary operations it requires) that is bounded by a polynomial over the size of the input parameters. Formal problems satisfying this criterion for classical computers form a *complexity class* usually referred to as *P*. It is schematically represented in Figure 3.

As introduced in Section 2.1.2, extracting useful information from a quantum register requires a measurement, ruled by the Born law. Therefore, a quantum computation is an alternation of non-deterministic (measurement) and deterministic (circuit unitary application, classical post-treatment,
the action of $\mathcal{M}$ over a state $\rho$ may result in any state $M_k \rho M_k^\dagger$, with probability $\text{tr}(M_k M_k^\dagger \rho)$, where the trace $\text{tr}(\mathcal{M})$ of a square matrix $\mathcal{M}$ with $n$ rows and columns is defined as the sum $\sum_{j \in [0, n]} M(j, j)$ of its diagonal cell values. Then, the overall action of a measurement $\mathcal{M}$ over a density operator $\rho$ results in $\rho' = \sum_{k \in [0, 2^{n}-1]} M_k \rho M_k^\dagger$.

Now, measurement description generalizes to the case of *partial measurements*, where only a sub-register is measured. Let us consider the case of a quantum register $q$ of size $n = n_1 + n_2$. We write $q_1$ and $q_2$ for the concatenated sub-registers and $H, H_1, H_2$ for the respectively induced Hilbert spaces. To simplify the notations we consider the case of measuring the first $n$ qubits. For any density operator $\rho$, if it is separable as $\rho = |x_1\rangle_n \langle y_1|_{n_1} \otimes |x_2\rangle_n \langle y_2|_{n_2}$, then the partial trace of $\rho$ over $H_2$ is defined as $\text{tr}_2(\rho) = \langle y_1|x_1\rangle \langle x_2|\langle y_2|$ and the definition generalizes by linearity to any density operator $\rho$. Then, $\text{tr}_2(\rho)$ equivalently represents the result of:

* (1) measuring register $q_2$ from the mixed state $\rho$ and (2) forgetting the measured qubits while conserving memory of the unmeasured subregister $q_1$ state;

* or just forgetting about (*discarding*) register $q_2$ in the description of $\rho$. Then, $\text{tr}_2(\rho)$ is the description of the sub-system held by $q_1$. We call $\text{tr}_2(\rho)$ a *partial density operator* on $H_1$.

### 2.1.6 Other Models for Quantum Computations

Many alternatives are currently explored for physical implementations of quantum computing machines and worth mentioning. Some of them (such as Measurement Based Quantum Computing [157, 32], topological quantum computations [76], linear optical networks [1], adiabatic quantum computing [65], etc.) differing on rather fundamental aspects (like, e.g., the elementary operations constituting computations). Nevertheless, currently, formal methods developments mainly address the standard circuit model introduced above.

The ZX-Calculus [47] also provides an alternative graphical formalism to reason about quantum processes. Basically, in this setting, quantum operations are represented by diagrams and their composition through sequence or parallelism corresponds to graphical compositions in the calculus. This language comes with a series of enabled transformations over graphs, preserving computational equivalence. ZX-Calculus is presented in Section 5.1.

## 2.2 Algorithms

As previously introduced, quantum computers are meant to perform calculations that classical computers are a priori not able to perform in a reasonable time. We give the formal complexity theory characterization for this point in Section 2.2.1, then Section 2.2.2 discusses the usual conventions for quantum algorithms descriptions.

### 2.2.1 Quantum Algorithms and Complexity

It is commonly assumed that formal problems are *tractable* by a computer if there exists an algorithm to solve this problem in time (measured by the number of elementary operations it requires) that is bounded by a polynomial over the size of the input parameters. Formal problems satisfying this criterion for classical computers form a *complexity class* usually referred to as *P*. It is schematically represented in Figure 3.

As introduced in Section 2.1.2, extracting useful information from a quantum register requires a measurement, ruled by the Born law. Therefore, a quantum computation is an alternation of non-deterministic (measurement) and deterministic (circuit unitary application, classical post-treatment,
etc) operations. Since such computations are probabilistic, the tractability criterion from above needs to be slightly adapted. Instead of considering problems for which a polynomial algorithm brings a solution with certainty, we consider those for which a polynomial algorithm brings a solution with an error probability of at most $\frac{1}{3}$. The corresponding class of problems for quantum computers is called *bounded error quantum polynomial time (BQP)*.

In addition to **P** and **BQP**, Figure 3 represents the *non-deterministic polynomial time* class **NP**. It gathers formal problems $\mathcal{P}$ for which there is an algorithm that, given a candidate solution, checks whether this candidate is an actual solution for $\mathcal{P}$ in polynomial time. It is trivial that **P** is included in **NP** and it is also proved that $\mathbf{P} \subseteq \mathbf{BQP}$. There are good reasons to believe that these inclusions are strict. Nevertheless, strictness is not formally proved and there are a variety of problems that belong to **NP** without a known tractable resolution algorithm.

<figure><img src="image_4.png" /><figcaption>Figure 3: Complexity classes P, NP, BQP</figcaption></figure>

Hence, quantum algorithm performance is not to be evaluated against the best *possible* performance of any classical computation (which depends on whether $\mathbf{BQP} = \mathbf{P}$) but, more pragmatically, against the best classical *known* equivalent.

Then, quantum computing is relevant for problems that are polynomially solvable by a quantum computer (with a given probability of success) but *intractable* by a classical one. They appear in the gray zone in Figure 3. The question whether the dark gray part ($\mathbf{BQP} \setminus \mathbf{NP}$) is empty or not depends on whether $\mathbf{BQP} \subseteq \mathbf{NP}$, which is unknown, but several $\mathbf{BQP}$-complete problems have been described through the literature [200]. These are neither easily computable nor verifiable with known classical means, but may be computed with quantum means: since quantum computers output a right solution for them with probability $> \frac{2}{3}$, after several runs one can select the best represented output as the sought solution.

Let us stress that the correspondence between polynomial solvability and tractability is not strict. For a problem, not belonging to a polynomial class bounds the size of input parameters concretely tractable by a computer, but does not absolutely forbid computation for any instance of it. Hence, for some problems, the quantum advantage does not consist in providing a polynomial resolution, but in reducing computation time to extend the set of tractable inputs. A typical example is the Grover search algorithm [84], searching for a distinguished element in an unstructured data set, providing a quadratic acceleration against classical procedures.

### 2.2.2 Quantum Algorithm Design

Before introducing the challenges at stake with implementations of quantum algorithms and their formal solutions, we make a few observations on the usual format used to describe quantum algorithms, based on an example: Figure 4 reproduces the core quantum part for Shor's algorithm [140, p. 232]— certainly the most emblematic of all quantum algorithms.
etc) operations. Since such computations are probabilistic, the tractability criterion from above needs to be slightly adapted. Instead of considering problems for which a polynomial algorithm brings a solution with certainty, we consider those for which a polynomial algorithm brings a solution with an error probability of at most $\frac{1}{3}$. The corresponding class of problems for quantum computers is called *bounded error quantum polynomial time (BQP)*.

In addition to **P** and **BQP**, Figure 3 represents the *non-deterministic polynomial time* class **NP**. It gathers formal problems $\mathcal{P}$ for which there is an algorithm that, given a candidate solution, checks whether this candidate is an actual solution for $\mathcal{P}$ in polynomial time. It is trivial that **P** is included in **NP** and it is also proved that $\mathbf{P} \subseteq \mathbf{BQP}$. There are good reasons to believe that these inclusions are strict. Nevertheless, strictness is not formally proved and there are a variety of problems that belong to **NP** without a known tractable resolution algorithm.

<figure><img src="image_4.png" /><figcaption>Figure 3: Complexity classes P, NP, BQP</figcaption></figure>

Hence, quantum algorithm performance is not to be evaluated against the best *possible* performance of any classical computation (which depends on whether $\mathbf{BQP} = \mathbf{P}$) but, more pragmatically, against the best classical *known* equivalent.

Then, quantum computing is relevant for problems that are polynomially solvable by a quantum computer (with a given probability of success) but *intractable* by a classical one. They appear in the gray zone in Figure 3. The question whether the dark gray part ($\mathbf{BQP} \setminus \mathbf{NP}$) is empty or not depends on whether $\mathbf{BQP} \subseteq \mathbf{NP}$, which is unknown, but several $\mathbf{BQP}$-complete problems have been described through the literature [200]. These are neither easily computable nor verifiable with known classical means, but may be computed with quantum means: since quantum computers output a right solution for them with probability $> \frac{2}{3}$, after several runs one can select the best represented output as the sought solution.

Let us stress that the correspondence between polynomial solvability and tractability is not strict. For a problem, not belonging to a polynomial class bounds the size of input parameters concretely tractable by a computer, but does not absolutely forbid computation for any instance of it. Hence, for some problems, the quantum advantage does not consist in providing a polynomial resolution, but in reducing computation time to extend the set of tractable inputs. A typical example is the Grover search algorithm [84], searching for a distinguished element in an unstructured data set, providing a quadratic acceleration against classical procedures.

### 2.2.2 Quantum Algorithm Design

Before introducing the challenges at stake with implementations of quantum algorithms and their formal solutions, we make a few observations on the usual format used to describe quantum algorithms, based on an example: Figure 4 reproduces the core quantum part for Shor's algorithm [140, p. 232]— certainly the most emblematic of all quantum algorithms.
The following observations generally hold for other quantum algorithms in the literature. We give them together with illustrations (within parenthesis) from the example of Figure 4.

1. The algorithm is structured in two main parts: a specification preamble and a **Procedure** description. The preamble indicates the minimal specification an implementation should satisfy. Note that it figures as an actual part of the algorithm itself. It contains three types of entries:

* a description of the **Inputs**, giving a signature for the parameters (a black-box circuit $U$, integers $x, N, L$ and two quantum registers of sizes $t$ and $L$) and some preconditions for these elements (e.g. $x$ co-prime to $L$, $L$ being $N$ bits long, etc);

* a description of the **Outputs** of the algorithm. It contains, again, a signature (an integer) and a success condition for these **Outputs** (to be equal to the sought modular order);

* a **Runtime** specification, containing: (1) a probability of success for each run of the **Procedure** ($O(1)$), (2) resources specifications. In the example, the latter consists in bounding the number of required elementary operations. Further metrics are also often used (the maximal *width* of required quantum circuits—the number of qubits a circuit requires, the maximal depth of a circuit—the maximal number of operations performed on a given qubit, etc).

2. The **Procedure** itself consists of a sequence of declared operations, interspersed with formal descriptions of the state of the system along with the performance of these operations. (in Figure 4 these elements are given in parallel, declarations of operations constitute the right-hand side and intermediate formal assertions are on the left-hand side). These assertions serve as specifications for the declared operations. For instance, operation “create superposition” has precondition the formal expression of Line 1, left (framed in blue) and postcondition the one of Line 2, left (framed in red). They serve as arguments to convince the reader that the algorithm **Outputs** conditions are met at the end of the **Procedure** (notice that the ultimate such postcondition—the measured state being $r$— corresponds to the success condition for the overall algorithm). But we can also interpret them as *contracts* for the programmer, committing her to implement each function in any way provided that whenever its inputs satisfy the preconditions, then its outputs satisfy the postconditions.

3. The algorithm description is parametric, and so should be any program implementing it. Hence, the quantum programming paradigm is higher-order: a quantum program is a function from (classical data) input parameters to quantum circuits. Then, each instance of a quantum circuit behaves as a function from its (quantum data) inputs to its (quantum data) outputs.

Most of the current quantum programs [153, 83, 193, 181, 180, 27, 41] proceed as implementations for functions such as those declared in Figure 4 (right part of the **Procedure** part), providing no guarantee over the algorithm specifications, be it about their functional behavior or their resource specifications.

Based on the preceding comments, the purpose of formal verification can be summarized as completing algorithm implementations with their proved specifications. In other words:

*Formal verification in quantum programming aims at providing solutions to furnish, in addition to quantum programs, evidence that these programs meet their specifications, in terms of both success probability and resource usage.*
The following observations generally hold for other quantum algorithms in the literature. We give them together with illustrations (within parenthesis) from the example of Figure 4.

1. The algorithm is structured in two main parts: a specification preamble and a **Procedure** description. The preamble indicates the minimal specification an implementation should satisfy. Note that it figures as an actual part of the algorithm itself. It contains three types of entries:

* a description of the **Inputs**, giving a signature for the parameters (a black-box circuit $U$, integers $x, N, L$ and two quantum registers of sizes $t$ and $L$) and some preconditions for these elements (e.g. $x$ co-prime to $L$, $L$ being $N$ bits long, etc);

* a description of the **Outputs** of the algorithm. It contains, again, a signature (an integer) and a success condition for these **Outputs** (to be equal to the sought modular order);

* a **Runtime** specification, containing: (1) a probability of success for each run of the **Procedure** ($O(1)$), (2) resources specifications. In the example, the latter consists in bounding the number of required elementary operations. Further metrics are also often used (the maximal *width* of required quantum circuits—the number of qubits a circuit requires, the maximal depth of a circuit—the maximal number of operations performed on a given qubit, etc).

2. The **Procedure** itself consists of a sequence of declared operations, interspersed with formal descriptions of the state of the system along with the performance of these operations. (in Figure 4 these elements are given in parallel, declarations of operations constitute the right-hand side and intermediate formal assertions are on the left-hand side). These assertions serve as specifications for the declared operations. For instance, operation “create superposition” has precondition the formal expression of Line 1, left (framed in blue) and postcondition the one of Line 2, left (framed in red). They serve as arguments to convince the reader that the algorithm **Outputs** conditions are met at the end of the **Procedure** (notice that the ultimate such postcondition—the measured state being $r$— corresponds to the success condition for the overall algorithm). But we can also interpret them as *contracts* for the programmer, committing her to implement each function in any way provided that whenever its inputs satisfy the preconditions, then its outputs satisfy the postconditions.

3. The algorithm description is parametric, and so should be any program implementing it. Hence, the quantum programming paradigm is higher-order: a quantum program is a function from (classical data) input parameters to quantum circuits. Then, each instance of a quantum circuit behaves as a function from its (quantum data) inputs to its (quantum data) outputs.

Most of the current quantum programs [153, 83, 193, 181, 180, 27, 41] proceed as implementations for functions such as those declared in Figure 4 (right part of the **Procedure** part), providing no guarantee over the algorithm specifications, be it about their functional behavior or their resource specifications.

Based on the preceding comments, the purpose of formal verification can be summarized as completing algorithm implementations with their proved specifications. In other words:

*Formal verification in quantum programming aims at providing solutions to furnish, in addition to quantum programs, evidence that these programs meet their specifications, in terms of both success probability and resource usage.*
**Inputs:** (1) A black-box $U_{x,N}$ which performs the transformation $|j\rangle|k\rangle \rightarrow |j\rangle|x^j k \text{ mod } N\rangle$, for $x$ co-prime to the $L$-bit number $N$, (2) $t = 2L+1 + \lfloor \log(2 + \frac{1}{2^E}) \rfloor$ qubits initialized to $|0\rangle$, and (3) $L$ qubits initialized to the state $|1\rangle$.

**Outputs:** The least integer $r > 0$ such that $x^r = 1 \pmod N$.

**Runtime:** $O(L^3)$ operations. Succeeds with probability $O(1)$.

**Procedure:**

1. $|0\rangle|u\rangle$ initial state

2. $\rightarrow \frac{1}{\sqrt{2^t}} \sum_{j=0}^{2^t-1} |j\rangle|1\rangle$ create superposition

3. $\rightarrow \frac{1}{\sqrt{2^t}} \sum_{j=0}^{2^t-1} |j\rangle|x^j \text{ mod } N\rangle$ apply $U_{x,N}$

$$ \approx \frac{1}{\sqrt{r2^t}} \sum_{s=0}^{r-1} \sum_{j=0}^{2^t-1} e^{2\pi i s j / r} |j\rangle|u_s\rangle $$

4. $\rightarrow \frac{1}{\sqrt{r}} \sum_{s=0}^{r-1} |\widetilde{s/r}\rangle|u_s\rangle$ apply inverse Fourier transform to the first register

5. $\rightarrow |\widetilde{s/r}\rangle$ measure first register

6. $\rightarrow r$ apply continued fraction algorithm

Figure 4: Bird-eye view of the circuit for Shor's factoring algorithm [174] (as presented in [140, p. 232])

## 2.3 Challenges for Quantum Computation

Let us now introduce some particularities of quantum programming with regards to classical computing. They raise design challenges that are particular to this programming paradigm.

### 2.3.1 Destructive Measurement and Non-Determinism

One of the main particularities of quantum programming is that the output produced by the quantum memory device follows the probabilistic Born rule (see Section 2.1.2). So, in the general case, the result of quantum computation is non-deterministic.

Furthermore, a computation in the model from Figure 1 contains both probabilistic quantum computations and classical control structures, performed by the classical controller. Hence, control itself may depend on the probabilistic data received from the quantum device and the execution flow itself is probabilistic.

### 2.3.2 Quantum Noise

Another particularity comes from the difficulty to maintain big quantum systems in a given state and to control the evolution of this state through time. Along with a quantum computation, uncontrolled modifications (bit or phase flip, amplitude damping, etc.) of the quantum state may occur.
**Inputs:** (1) A black-box $U_{x,N}$ which performs the transformation $|j\rangle|k\rangle \rightarrow |j\rangle|x^j k \text{ mod } N\rangle$, for $x$ co-prime to the $L$-bit number $N$, (2) $t = 2L+1 + \lfloor \log(2 + \frac{1}{2^E}) \rfloor$ qubits initialized to $|0\rangle$, and (3) $L$ qubits initialized to the state $|1\rangle$.

**Outputs:** The least integer $r > 0$ such that $x^r = 1 \pmod N$.

**Runtime:** $O(L^3)$ operations. Succeeds with probability $O(1)$.

**Procedure:**

1. $|0\rangle|u\rangle$ initial state

2. $\rightarrow \frac{1}{\sqrt{2^t}} \sum_{j=0}^{2^t-1} |j\rangle|1\rangle$ create superposition

3. $\rightarrow \frac{1}{\sqrt{2^t}} \sum_{j=0}^{2^t-1} |j\rangle|x^j \text{ mod } N\rangle$ apply $U_{x,N}$

$$ \approx \frac{1}{\sqrt{r2^t}} \sum_{s=0}^{r-1} \sum_{j=0}^{2^t-1} e^{2\pi i s j / r} |j\rangle|u_s\rangle $$

4. $\rightarrow \frac{1}{\sqrt{r}} \sum_{s=0}^{r-1} |\widetilde{s/r}\rangle|u_s\rangle$ apply inverse Fourier transform to the first register

5. $\rightarrow |\widetilde{s/r}\rangle$ measure first register

6. $\rightarrow r$ apply continued fraction algorithm

Figure 4: Bird-eye view of the circuit for Shor's factoring algorithm [174] (as presented in [140, p. 232])

## 2.3 Challenges for Quantum Computation

Let us now introduce some particularities of quantum programming with regards to classical computing. They raise design challenges that are particular to this programming paradigm.

### 2.3.1 Destructive Measurement and Non-Determinism

One of the main particularities of quantum programming is that the output produced by the quantum memory device follows the probabilistic Born rule (see Section 2.1.2). So, in the general case, the result of quantum computation is non-deterministic.

Furthermore, a computation in the model from Figure 1 contains both probabilistic quantum computations and classical control structures, performed by the classical controller. Hence, control itself may depend on the probabilistic data received from the quantum device and the execution flow itself is probabilistic.

### 2.3.2 Quantum Noise

Another particularity comes from the difficulty to maintain big quantum systems in a given state and to control the evolution of this state through time. Along with a quantum computation, uncontrolled modifications (bit or phase flip, amplitude damping, etc.) of the quantum state may occur.
To overcome this phenomenon, one solution consists in integrating error correction mechanisms into the compilation. Error correction design is an active research fields [40, 129, 81, 75]. Many propositions have been developed. They mainly consist in designing redundant quantum circuits (one logical qubit is implemented by many different physical qubits). Then the main challenge is to design a solution for testing the reliability along with a computation without losing the state of the register due to destructive measurement.

Since error correction requires bigger quantum registers (due to redundancy), its possible implementation is conditioned by the design, elaboration and availability of large quantum processors.

An alternative strategy is to not correct quantum errors, but design computations to limit their effect. John Preskill introduced the notion of *Noisy-Intermediate Scale Quantum (NISQ)* technologies [152]. The formal analysis of error propagation requires the identification of possible errors together with rules specifying how their probability of occurrences propagates along with quantum circuits [97, 155].

### 2.3.3 Efficient Compilation on Constrained Hardware

Languages such as *Liqui|*\rangle, Q#, Quipper, etc. enable the description and building of quantum circuits for so-called *logical qubits*. In practice, realizing a quantum circuit on an actual quantum machine (*physical qubits*) requires several compilation passes, in addition to the error correction mentioned in the preceding paragraph. Among others:

* the physical realization should respect the physical constraints of its target architecture, which concerns, e.g. connectivity of qubits or register size limits. Considering this point requires qubit reordering intermediary operations and an adequate mapping between theoretical and physical qubits;

* the set of possible quantum operations over physical qubits may not correspond to the set of elementary gates from the logical circuit description, which would require an adequate gate synthesis and circuit rewriting;

* last but not least, physical realization of an algorithm should be as resource frugal as possible, requiring the development of circuit optimization techniques.

Each of these steps consists of low-level operations over circuits. They must all preserve functional equivalence while reaching their proper purpose. For these low-level developing layers, one requires tools and languages formalizing functionally equivalent circuit transformation operations. ZX-Calculus [47] (Section 5.1) is particularly well-fitted for such design, other propositions include the proof of path-sum semantics equivalence [5, 4] (Section 5.2) and formally verified circuit optimization [91] (Section 5.4).

# 3 General Background on Formal Methods

We now present a brief overview of formal methods. While the domain is old and has led to rich literature, we try to highlight the underlying main principles and to quickly describe the most popular classes of techniques so far.

## 3.1 Introduction

Formal methods and formal verification [44] denote a wide range of techniques aiming at *proving* the correctness of a system with a *mathematical guarantee*—reasoning over *all* possible inputs and
To overcome this phenomenon, one solution consists in integrating error correction mechanisms into the compilation. Error correction design is an active research fields [40, 129, 81, 75]. Many propositions have been developed. They mainly consist in designing redundant quantum circuits (one logical qubit is implemented by many different physical qubits). Then the main challenge is to design a solution for testing the reliability along with a computation without losing the state of the register due to destructive measurement.

Since error correction requires bigger quantum registers (due to redundancy), its possible implementation is conditioned by the design, elaboration and availability of large quantum processors.

An alternative strategy is to not correct quantum errors, but design computations to limit their effect. John Preskill introduced the notion of *Noisy-Intermediate Scale Quantum (NISQ)* technologies [152]. The formal analysis of error propagation requires the identification of possible errors together with rules specifying how their probability of occurrences propagates along with quantum circuits [97, 155].

### 2.3.3 Efficient Compilation on Constrained Hardware

Languages such as *Liqui|*\rangle, Q#, Quipper, etc. enable the description and building of quantum circuits for so-called *logical qubits*. In practice, realizing a quantum circuit on an actual quantum machine (*physical qubits*) requires several compilation passes, in addition to the error correction mentioned in the preceding paragraph. Among others:

* the physical realization should respect the physical constraints of its target architecture, which concerns, e.g. connectivity of qubits or register size limits. Considering this point requires qubit reordering intermediary operations and an adequate mapping between theoretical and physical qubits;

* the set of possible quantum operations over physical qubits may not correspond to the set of elementary gates from the logical circuit description, which would require an adequate gate synthesis and circuit rewriting;

* last but not least, physical realization of an algorithm should be as resource frugal as possible, requiring the development of circuit optimization techniques.

Each of these steps consists of low-level operations over circuits. They must all preserve functional equivalence while reaching their proper purpose. For these low-level developing layers, one requires tools and languages formalizing functionally equivalent circuit transformation operations. ZX-Calculus [47] (Section 5.1) is particularly well-fitted for such design, other propositions include the proof of path-sum semantics equivalence [5, 4] (Section 5.2) and formally verified circuit optimization [91] (Section 5.4).

# 3 General Background on Formal Methods

We now present a brief overview of formal methods. While the domain is old and has led to rich literature, we try to highlight the underlying main principles and to quickly describe the most popular classes of techniques so far.

## 3.1 Introduction

Formal methods and formal verification [44] denote a wide range of techniques aiming at *proving* the correctness of a system with a *mathematical guarantee*—reasoning over *all* possible inputs and
paths of the system, with methods drawn from logic, automated reasoning and program analysis. The last two decades have seen an extraordinary blooming of the field, with significant case studies ranging from pure mathematics [80] to complete software architectures [112, 124] and industrial systems [20, 107]. In addition to offering an alternative to testing, formal verification has in principle the decisive additional advantages to both enable parametric proof certificates and offer once-for-all absolute guarantees for the correctness of programs.

## 3.2 Principles

Formal methods' main principles were laid mostly in the 1970s. Pioneers include Floyd [74], Hoare [94], Dijkstra [59], Cousot [49] and Clark [42]. While there is a wide diversity of approaches in the field, any formal method builds upon the following three key ingredients:

* a formal semantics $M$ representing the possible behaviors of a system or program-$M$ is typically equipped with an operational semantics and behaviors are often represented as a set of traces $L(M)$;

* a formal specification $\varphi$ of the acceptable or correct behaviors-$\varphi$ is typically a logical formula or an automaton representing a set of traces $L_\varphi$;

* a (semi-)decision procedure verifying that possible behaviors are indeed correct, denoted $M \models \varphi$-typically a semi-algorithm to check whether $L(M) \subseteq L_\varphi$ holds or not.

Regarding the complexity of realistic systems and programs, the verification problem is usually undecidable, hence the impossibility to have a fully automated and perfectly precise decision procedure for it. The different formal method communities bring different responses to get around this fundamental limitation, yielding different trade-offs in the design space, favoring either restriction of the classes of systems under analysis, restrictions of the classes of properties, human guidance or one-sided answer (over-approximations or under-approximations).

Overall, after two decades of maturation, formal methods have made enough progress to be successfully applied to (mostly safety-critical) software [89, 191, 12, 31, 50, 116, 107].

## 3.3 The Formal Method Zoo

We present now in more detail the main classes of formal methods. While recent techniques tend to blur the lines and combine aspects from several main approaches, this classification is still useful to understand the trade-off at stake in the field.

* Type checking and unification: at the crossroad of programming language design and formal methods, type systems [150] allow forbidding by design certain classes of errors or bad code patterns (such as trying to add together a number and a boolean in Java or, in a quantum setting, trying to apply a unitary operation over a classical data register). Traditionally, type systems focus on simple “well-formedness” properties (good typing), but they scale very well (modular reasoning) and require only a little manual annotation effort (type inference). While first type systems were based on basic unification [93, 136], advanced type systems with dependent types or flow-sensitivity come closer and closer to full-fledged verification techniques;

* Model checking and its many variants: while initially focused on finite-state systems [42] (typically, idealized protocols or hardware models) and complex temporal properties-with
paths of the system, with methods drawn from logic, automated reasoning and program analysis. The last two decades have seen an extraordinary blooming of the field, with significant case studies ranging from pure mathematics [80] to complete software architectures [112, 124] and industrial systems [20, 107]. In addition to offering an alternative to testing, formal verification has in principle the decisive additional advantages to both enable parametric proof certificates and offer once-for-all absolute guarantees for the correctness of programs.

## 3.2 Principles

Formal methods' main principles were laid mostly in the 1970s. Pioneers include Floyd [74], Hoare [94], Dijkstra [59], Cousot [49] and Clark [42]. While there is a wide diversity of approaches in the field, any formal method builds upon the following three key ingredients:

* a formal semantics $M$ representing the possible behaviors of a system or program-$M$ is typically equipped with an operational semantics and behaviors are often represented as a set of traces $L(M)$;

* a formal specification $\varphi$ of the acceptable or correct behaviors-$\varphi$ is typically a logical formula or an automaton representing a set of traces $L_\varphi$;

* a (semi-)decision procedure verifying that possible behaviors are indeed correct, denoted $M \models \varphi$-typically a semi-algorithm to check whether $L(M) \subseteq L_\varphi$ holds or not.

Regarding the complexity of realistic systems and programs, the verification problem is usually undecidable, hence the impossibility to have a fully automated and perfectly precise decision procedure for it. The different formal method communities bring different responses to get around this fundamental limitation, yielding different trade-offs in the design space, favoring either restriction of the classes of systems under analysis, restrictions of the classes of properties, human guidance or one-sided answer (over-approximations or under-approximations).

Overall, after two decades of maturation, formal methods have made enough progress to be successfully applied to (mostly safety-critical) software [89, 191, 12, 31, 50, 116, 107].

## 3.3 The Formal Method Zoo

We present now in more detail the main classes of formal methods. While recent techniques tend to blur the lines and combine aspects from several main approaches, this classification is still useful to understand the trade-off at stake in the field.

* Type checking and unification: at the crossroad of programming language design and formal methods, type systems [150] allow forbidding by design certain classes of errors or bad code patterns (such as trying to add together a number and a boolean in Java or, in a quantum setting, trying to apply a unitary operation over a classical data register). Traditionally, type systems focus on simple “well-formedness” properties (good typing), but they scale very well (modular reasoning) and require only a little manual annotation effort (type inference). While first type systems were based on basic unification [93, 136], advanced type systems with dependent types or flow-sensitivity come closer and closer to full-fledged verification techniques;

* Model checking and its many variants: while initially focused on finite-state systems [42] (typically, idealized protocols or hardware models) and complex temporal properties-with
essentially graph-based and automata-based decision procedures, model checking [43] has
notably evolved along the year to cope with infinite-state systems, either through specific
decidable classes (e.g., Petri Nets or Timed Automata) or through abstractions. The cur-
rent approaches to software model checking include notably symbolic bounded verification
[116, 35] for bug finding and counter-example guided abstraction refinement [89] for bug
finding and proof of invariants (but it may loop forever). Usually, model checking relies on
specifications expressed in a variant of modal logic such as temporal logic [42, 151], dynamic
logic [86, 122, 72] or mu-calculus [114, 167];

*   **Abstract Interpretation:** Generally speaking, Abstract Interpretation [49] is a general theory of abstraction for fixpoint computations. Abstract Interpretation-based static analysis [161] builds over Abstract Interpretation to effectively compute sound (i.e. overapproximated) abstractions of all reachable states of a program. Hence, these techniques are well suited for proving invariants. More precisely, Abstract Interpretation provides a systematic recipe to design sound abstract computation over sets of program states, by connecting the concrete domain (e.g., sets of states) to a given abstract domain (e.g., interval constraints) through a Galois Connexion between an abstraction and a concretization functions. In practice, Abstract Interpretation comes down to computing the fixpoint over the abstract domain, ensuring termination but losing precision. Different abstract domains provide different trade-offs between cost and precision. Historically speaking, the approach targets full automation and implicit properties (e.g., runtime error);

*   **Deductive verification and first-order reasoning:** Deductive program verification [17, 71, 94, 182] is probably the oldest formal method technique, dating back to 1969 [94] and the development of Hoare logic. In this approach, programs are annotated with logical assertions, such as pre- and postconditions for operations or loop invariants, then so-called proof obligations are automatically generated (e.g., by the weakest precondition algorithm) in such a way that proving (a.k.a. discharging) them ensures that the logical assertions hold along any execution of the program. These proof obligations are commonly expressed in first-order or separation logic [158] and proven by the help of proof assistants [145, 141] or automatic solvers lying on Satisfiability Modulo Theory [18] or Automated Theorem Proving [73];

*   Interactive proof and second-order reasoning: some techniques completely drop the hope for automation in favor of expressivity, relying on 2nd order or even higher-order specification and proofs languages—typically in Coq [145] or ISABELLE/HOL [141]. Once programmed and proved in the language, a certified functional program can then often be extracted. This family of approaches is very versatile and almost any problem or specification can be encoded, yet it requires lots of manual effort, both for the specification and the proofs—higher-order proofs can be automatically checked but not found. Still, the technique has been for example used for certified compilers or operating systems [124, 112].

# 4 Overview of Formal Methods in Quantum Computing

As presented in Section 3, formal methods for proving properties of classical algorithms, programs and systems are well-developed and versatile. In this section, we present the needs for formal methods in the realm of quantum computation, while the later sections are devoted to answering them.
essentially graph-based and automata-based decision procedures, model checking [43] has
notably evolved along the year to cope with infinite-state systems, either through specific
decidable classes (e.g., Petri Nets or Timed Automata) or through abstractions. The cur-
rent approaches to software model checking include notably symbolic bounded verification
[116, 35] for bug finding and counter-example guided abstraction refinement [89] for bug
finding and proof of invariants (but it may loop forever). Usually, model checking relies on
specifications expressed in a variant of modal logic such as temporal logic [42, 151], dynamic
logic [86, 122, 72] or mu-calculus [114, 167];

*   **Abstract Interpretation:** Generally speaking, Abstract Interpretation [49] is a general theory of abstraction for fixpoint computations. Abstract Interpretation-based static analysis [161] builds over Abstract Interpretation to effectively compute sound (i.e. overapproximated) abstractions of all reachable states of a program. Hence, these techniques are well suited for proving invariants. More precisely, Abstract Interpretation provides a systematic recipe to design sound abstract computation over sets of program states, by connecting the concrete domain (e.g., sets of states) to a given abstract domain (e.g., interval constraints) through a Galois Connexion between an abstraction and a concretization functions. In practice, Abstract Interpretation comes down to computing the fixpoint over the abstract domain, ensuring termination but losing precision. Different abstract domains provide different trade-offs between cost and precision. Historically speaking, the approach targets full automation and implicit properties (e.g., runtime error);

*   **Deductive verification and first-order reasoning:** Deductive program verification [17, 71, 94, 182] is probably the oldest formal method technique, dating back to 1969 [94] and the development of Hoare logic. In this approach, programs are annotated with logical assertions, such as pre- and postconditions for operations or loop invariants, then so-called proof obligations are automatically generated (e.g., by the weakest precondition algorithm) in such a way that proving (a.k.a. discharging) them ensures that the logical assertions hold along any execution of the program. These proof obligations are commonly expressed in first-order or separation logic [158] and proven by the help of proof assistants [145, 141] or automatic solvers lying on Satisfiability Modulo Theory [18] or Automated Theorem Proving [73];

*   Interactive proof and second-order reasoning: some techniques completely drop the hope for automation in favor of expressivity, relying on 2nd order or even higher-order specification and proofs languages—typically in Coq [145] or ISABELLE/HOL [141]. Once programmed and proved in the language, a certified functional program can then often be extracted. This family of approaches is very versatile and almost any problem or specification can be encoded, yet it requires lots of manual effort, both for the specification and the proofs—higher-order proofs can be automatically checked but not found. Still, the technique has been for example used for certified compilers or operating systems [124, 112].

# 4 Overview of Formal Methods in Quantum Computing

As presented in Section 3, formal methods for proving properties of classical algorithms, programs and systems are well-developed and versatile. In this section, we present the needs for formal methods in the realm of quantum computation, while the later sections are devoted to answering them.
## 4.1 The Need for Formal Methods in Quantum Computing

As introduced in Section 2, the data structures at stake in quantum computing make the computations hard to represent for developers. Intermediary formal languages are of great help for understanding what quantum programs do and describing their functional behavior.

Furthermore, as introduced in Section 1, directly importing the testing and debugging practices at use in classical programming is extremely difficult in the quantum case<fnref n="4" />, due to the destructive aspect of quantum measurement. Moreover, the probabilistic nature of quantum algorithms seriously impedes system-level quantum testing. As a consequence, test-based programming strategies do not seem adequate in the quantum case and quantum computing needs alternative debugging strategies and methodologies.

So far, existing quantum processors were small enough that their behavior could be entirely simulated on a classical device. Hence, a short-term solution for overcoming the debugging challenge relied on classical simulations of quantum programs. Since quantum computer prototypes are now reaching the size limit over which this simulation will not be possible anymore (among others, [9] is often referred to as the milestone for this context change, referred to as *quantum supremacy*), more robust solutions must be developed.

On the other hand, nothing prevents *a priori* the formal verification of quantum programs. In addition to constituting alternative debugging strategies, formal methods have several additional decisive advantages. In particular:

* They enable parametrized reasoning and certification in the higher-order quantum programming context introduced in Section 2.2.2: formal certification of a parametrized program holds for any circuit generated by this program, whatever the value of its parameters. In contrast, testing certification holds for the particular values of these parameters that are used in a test. Formal certification is not limited by the size of the parameters;

* It provides once for all an absolute, mathematically proven, certification of a program's specifications, whereas testing furnishes at best only statistical arguments based on bounded-size input samples.

## 4.2 Typology of Properties to Verify

In this section we detail the different properties one has to mind for developing correct quantum programs. The goal of formal certification is to provide solutions for their verification.

### 4.2.1 Functional Specifications

A major challenge is to give assurance on the input/output relationship computed by a given program, that is verifying whether a given program implements an intended function $f$. Functional specifications are two-layered:

**High-level specifications.** We give a circuit an overall specification independent from the concrete implementation. It is made of a success condition and a minimum probability, for any run of this circuit, to result in an output satisfying the success condition.

In the hybrid model, circuits are run on a quantum co-processor but controlled by a classical computer, performing control operations (such as **if** and **while** instructions, simple sequence, etc). As a simple example, an algorithm such as the one from Figure 4 outputs a success with probability

<footnote n="4">⁴It requires major adaptations and redefinitions, see Section 8.4 for details.</footnote>
## 4.1 The Need for Formal Methods in Quantum Computing

As introduced in Section 2, the data structures at stake in quantum computing make the computations hard to represent for developers. Intermediary formal languages are of great help for understanding what quantum programs do and describing their functional behavior.

Furthermore, as introduced in Section 1, directly importing the testing and debugging practices at use in classical programming is extremely difficult in the quantum case<fnref n="4" />, due to the destructive aspect of quantum measurement. Moreover, the probabilistic nature of quantum algorithms seriously impedes system-level quantum testing. As a consequence, test-based programming strategies do not seem adequate in the quantum case and quantum computing needs alternative debugging strategies and methodologies.

So far, existing quantum processors were small enough that their behavior could be entirely simulated on a classical device. Hence, a short-term solution for overcoming the debugging challenge relied on classical simulations of quantum programs. Since quantum computer prototypes are now reaching the size limit over which this simulation will not be possible anymore (among others, [9] is often referred to as the milestone for this context change, referred to as *quantum supremacy*), more robust solutions must be developed.

On the other hand, nothing prevents *a priori* the formal verification of quantum programs. In addition to constituting alternative debugging strategies, formal methods have several additional decisive advantages. In particular:

* They enable parametrized reasoning and certification in the higher-order quantum programming context introduced in Section 2.2.2: formal certification of a parametrized program holds for any circuit generated by this program, whatever the value of its parameters. In contrast, testing certification holds for the particular values of these parameters that are used in a test. Formal certification is not limited by the size of the parameters;

* It provides once for all an absolute, mathematically proven, certification of a program's specifications, whereas testing furnishes at best only statistical arguments based on bounded-size input samples.

## 4.2 Typology of Properties to Verify

In this section we detail the different properties one has to mind for developing correct quantum programs. The goal of formal certification is to provide solutions for their verification.

### 4.2.1 Functional Specifications

A major challenge is to give assurance on the input/output relationship computed by a given program, that is verifying whether a given program implements an intended function $f$. Functional specifications are two-layered:

**High-level specifications.** We give a circuit an overall specification independent from the concrete implementation. It is made of a success condition and a minimum probability, for any run of this circuit, to result in an output satisfying the success condition.

In the hybrid model, circuits are run on a quantum co-processor but controlled by a classical computer, performing control operations (such as **if** and **while** instructions, simple sequence, etc). As a simple example, an algorithm such as the one from Figure 4 outputs a success with probability

<footnote n="4">⁴It requires major adaptations and redefinitions, see Section 8.4 for details.</footnote>
p. It can be included in a control structure including k iterations of it. This higher-level procedure has probability [1 - (1 - p)^k] to output a success at least once, which can be made arbitrarily close to 1.

More generally, a high-level quantum verification framework [131, 194] considers an algorithm as a controlled sequence of quantum functions. There, one considers quantum operations as primitives and composes them together via controlled sequence operations. These operations are interpreted as functions in the semantical formalism. For example, [168, 131, 194] formalize quantum programs in the *density operators formalism*. This view is introduced in detail in Section 7.1 together with the Quantum Hoare Logic (QHL) [131, 194].

**Intermediate specifications.** In the **Procedure** section from Figure 4, each mid-level step of the algorithm is given a formal specification, that is a description of the state of the system. These intermediate specifications are deterministic and concern quantum data.

In a lower-level verification approach view, instead of inputting quantum operations as primitive functions, one builds quantum circuit implementations of these operations, by adequately combining quantum gates. Such a framework [91, 156, 38] relies on a circuit description language such as Quipper or QWIRE. Then, an adequate semantics characterization for the built circuits enables to reason about the quantum data received as inputs and delivered as outputs. A certification solution for quantum circuits enables us to reason compositionally about their semantics. This programming view is explored in Sections 7.2 and7.3.

### 4.2.2 Complexity specifications

The major reason for developing quantum computers and quantum algorithms is to lower computing complexity specifications, w.r.t. classical computing solutions (see Section 2.2.1 for precisions). Therefore, the relevance of a quantum implementation relies on the fact it satisfies low complexity specifications. As introduced in Section 2.2.2, they may be formulated through different metrics, such as the width and/or depth of quantum circuits, their number of elementary gates or more complex metrics such as *quantum volume* [125].

The complexity specification is also crucial for another reason: remind from Section 2.3.2 that quantum computation is subject to noise: the bigger a quantum circuit is, the most prone to error it is. Functional specifications introduced so far reason about the theoretical output of quantum computations, in the absence of errors. The risk of error in a circuit is closely related to the structural characteristics of this circuit, among which are the different measures of complexity. Therefore, the information provided by these measures is also crucial to appreciate the functional trustfulness of an implementation.

### 4.2.3 Structural Constraints

Quantum circuit design must also consider various *structural constraints* that discriminate through several criteria:

1. They can be either relative to a target architecture or absolute (induced by quantum physics laws). The first category comprises, for example, the number of available qubits in a processor, the connectivity between physical qubits, the set of available elementary gates, etc. The second category mainly deals with aspects induced by quantum Calculus unitarity (no cloning theorem, ancilla management, quantum control, etc.);
p. It can be included in a control structure including k iterations of it. This higher-level procedure has probability [1 - (1 - p)^k] to output a success at least once, which can be made arbitrarily close to 1.

More generally, a high-level quantum verification framework [131, 194] considers an algorithm as a controlled sequence of quantum functions. There, one considers quantum operations as primitives and composes them together via controlled sequence operations. These operations are interpreted as functions in the semantical formalism. For example, [168, 131, 194] formalize quantum programs in the *density operators formalism*. This view is introduced in detail in Section 7.1 together with the Quantum Hoare Logic (QHL) [131, 194].

**Intermediate specifications.** In the **Procedure** section from Figure 4, each mid-level step of the algorithm is given a formal specification, that is a description of the state of the system. These intermediate specifications are deterministic and concern quantum data.

In a lower-level verification approach view, instead of inputting quantum operations as primitive functions, one builds quantum circuit implementations of these operations, by adequately combining quantum gates. Such a framework [91, 156, 38] relies on a circuit description language such as Quipper or QWIRE. Then, an adequate semantics characterization for the built circuits enables to reason about the quantum data received as inputs and delivered as outputs. A certification solution for quantum circuits enables us to reason compositionally about their semantics. This programming view is explored in Sections 7.2 and7.3.

### 4.2.2 Complexity specifications

The major reason for developing quantum computers and quantum algorithms is to lower computing complexity specifications, w.r.t. classical computing solutions (see Section 2.2.1 for precisions). Therefore, the relevance of a quantum implementation relies on the fact it satisfies low complexity specifications. As introduced in Section 2.2.2, they may be formulated through different metrics, such as the width and/or depth of quantum circuits, their number of elementary gates or more complex metrics such as *quantum volume* [125].

The complexity specification is also crucial for another reason: remind from Section 2.3.2 that quantum computation is subject to noise: the bigger a quantum circuit is, the most prone to error it is. Functional specifications introduced so far reason about the theoretical output of quantum computations, in the absence of errors. The risk of error in a circuit is closely related to the structural characteristics of this circuit, among which are the different measures of complexity. Therefore, the information provided by these measures is also crucial to appreciate the functional trustfulness of an implementation.

### 4.2.3 Structural Constraints

Quantum circuit design must also consider various *structural constraints* that discriminate through several criteria:

1. They can be either relative to a target architecture or absolute (induced by quantum physics laws). The first category comprises, for example, the number of available qubits in a processor, the connectivity between physical qubits, the set of available elementary gates, etc. The second category mainly deals with aspects induced by quantum Calculus unitarity (no cloning theorem, ancilla management, quantum control, etc.);
2. Now, depending on the programming language at stake, absolute structural constraints may either be taken into charge by the language design or left to the user's responsibility. For example, the *no-cloning rule* is derived from the unitarity of quantum processes. It forbids using the same quantum data register twice:

* in languages where quantum data registers are full right objects (eg: Quipper, QWIRE, *etc*), caring for the respect of no-cloning is left to the user. In this case, formal verification may help her to do so. Solutions like ProtoQuipper [162] or QWIRE [148, 156] tackle this problem through linear type systems (see Section 6.3);

* another possibility is to reduce the expressivity of the language (eg: QFC/QPL [168], SQIR [91], QBRICKS [38]), to prevent any possible violation of no-cloning. In SQIR or QBRICKS, quantum data registers are addressed via integer indexes, but the quantum data they hold are not directly accessible from the programming language itself. These data concern the semantics of the language and they are formalized only in the specification language. Hence, the respecting conditions for the no-cloning theorem are reduced to simple indexing rules for quantum circuits.

3. Last, structural program constraints can be either syntactic or semantic. The first category contains, for example, all constraints that are linked with qubit identification (eg. *do not control an operation by the value of a qubit it is acting on*). The most representative example for semantic constraints concerns a particular aspect of quantum computing that we do not detail in this survey: the management of ancilla qubits. Ancilla qubits provide additional memory for some sections of quantum circuits, the content of which is then discharged at some stage of the computation. Discharging a part of a register is possible (without affecting the rest of the memory) only if there is no interaction between the memory to discharge and the rest of the memory (See [140] for further details). Hence, ancilla management is possible modulo some non-entanglement specifications, regarding the semantics of quantum circuits.

### 4.2.4 Circuit Equivalence

Compilation of quantum programs contains many circuit rewriting operations (see Section 2.3.3). They concern the implementation of logical qubits in a physical framework and require certification for functional behavior preservation. Concretely, given a logical circuit *C*, compiling *C* traces as a chain of circuits, starting from *C* and each obtained from the precedent by applying a circuit rewriting operation. Each such rewriting must preserve the input/output relation, to ensure that, provided *C* fits its functional specifications, then so does the final physical qubits circuit. In Section 5 we present two tools enabling the verification of circuit equivalence: the ZX-Calculus (Section 5.1) and the path-sum equivalence verification (Section 5.2).

**Further formal comparisons between quantum processes.** Different notions of equivalence between quantum processes are also at stake with further uses of quantum information, such as communication protocols. Recent developments [185, 19] generalize the equivalence specification to further comparison predicates between quantum processes. Since they are not designed for the formalization of algorithms, which is the scope of the present survey, we do not detail these propositions in the present survey.
2. Now, depending on the programming language at stake, absolute structural constraints may either be taken into charge by the language design or left to the user's responsibility. For example, the *no-cloning rule* is derived from the unitarity of quantum processes. It forbids using the same quantum data register twice:

* in languages where quantum data registers are full right objects (eg: Quipper, QWIRE, *etc*), caring for the respect of no-cloning is left to the user. In this case, formal verification may help her to do so. Solutions like ProtoQuipper [162] or QWIRE [148, 156] tackle this problem through linear type systems (see Section 6.3);

* another possibility is to reduce the expressivity of the language (eg: QFC/QPL [168], SQIR [91], QBRICKS [38]), to prevent any possible violation of no-cloning. In SQIR or QBRICKS, quantum data registers are addressed via integer indexes, but the quantum data they hold are not directly accessible from the programming language itself. These data concern the semantics of the language and they are formalized only in the specification language. Hence, the respecting conditions for the no-cloning theorem are reduced to simple indexing rules for quantum circuits.

3. Last, structural program constraints can be either syntactic or semantic. The first category contains, for example, all constraints that are linked with qubit identification (eg. *do not control an operation by the value of a qubit it is acting on*). The most representative example for semantic constraints concerns a particular aspect of quantum computing that we do not detail in this survey: the management of ancilla qubits. Ancilla qubits provide additional memory for some sections of quantum circuits, the content of which is then discharged at some stage of the computation. Discharging a part of a register is possible (without affecting the rest of the memory) only if there is no interaction between the memory to discharge and the rest of the memory (See [140] for further details). Hence, ancilla management is possible modulo some non-entanglement specifications, regarding the semantics of quantum circuits.

### 4.2.4 Circuit Equivalence

Compilation of quantum programs contains many circuit rewriting operations (see Section 2.3.3). They concern the implementation of logical qubits in a physical framework and require certification for functional behavior preservation. Concretely, given a logical circuit *C*, compiling *C* traces as a chain of circuits, starting from *C* and each obtained from the precedent by applying a circuit rewriting operation. Each such rewriting must preserve the input/output relation, to ensure that, provided *C* fits its functional specifications, then so does the final physical qubits circuit. In Section 5 we present two tools enabling the verification of circuit equivalence: the ZX-Calculus (Section 5.1) and the path-sum equivalence verification (Section 5.2).

**Further formal comparisons between quantum processes.** Different notions of equivalence between quantum processes are also at stake with further uses of quantum information, such as communication protocols. Recent developments [185, 19] generalize the equivalence specification to further comparison predicates between quantum processes. Since they are not designed for the formalization of algorithms, which is the scope of the present survey, we do not detail these propositions in the present survey.
# 5 Low-Level Verification: Compilation and Equivalence

Realizing logical circuits into physical devices (circuit compilation) requires to deal with severe constraints: the number of available qubits, their connectivity, the set of elementary operations, the instability of quantum information–requiring the insertion of error correction mechanisms, etc. As mentioned in Section 4.2.4, the underlying circuit transformations must preserve functional equivalence with the initial circuit representation, all along the compilation process. In the present section we introduce formal tools for checking such equivalences and certifying compilation correctness.

## 5.1 ZX-Calculus and Quantomatic/PyZX

ZX-Calculus [46] is a powerful graphical language for representing and manipulating quantum information. This language historically stems from category theory applied to quantum mechanics, through the program Categorical Quantum Mechanics initiated by Samson Abramsky and Bob Coecke [2].

For our purposes, it is interesting to see ZX-diagrams as a lax version of quantum circuits. This laxness on the one hand implies that not all ZX-diagrams are implementable with physical qubits, but on the other hand, it allows formalism to get powerful results on the underlying equational theory (rewriting rules, pseudo-normal forms).

The level of abstraction provided by the language allows the user to reason about quantum programs or protocols while significantly alleviating the "bureaucracy checks" typically coming with circuit-level reasoning, in particular, checking sub-circuit equivalence in the presence of ancillas. It also allows unifying different models of quantum computation (circuits, measurement-based quantum computing, lattice surgery, etc.), as well as to provide optimization strategies for these models. Last but not least, it can be used to formally (yet, graphically) verify properties on protocols or programs—all that based on simple graph-based manipulations.

### 5.1.1 Semantical Model

The ZX-diagrams are generated from a set of primitives:

$$ \left\{ \left| \begin{array}{c} \text{X} \\ \text{Y} \\ \text{Z} \end{array} \right\rangle, \begin{array}{c} \text{U} \\ \text{U} \\ \text{U} \end{array}, \begin{array}{c} \text{C} \\ \text{C} \\ \text{C} \end{array}, \begin{array}{c} \text{n} \\ \text{n} \\ \text{n} \end{array}, \begin{array}{c} \text{α} \\ \text{α} \\ \text{α} \end{array}, \begin{array}{c} \vdash \\ \vdash \\ \vdash \end{array} \right\}_{n,m \in \mathbb{N} \\ \alpha \in \mathbb{R}} $$

which can be composed either:

<figure><img src="image_5.png" /></figure>

* sequentially:

<figure><img src="image_6.png" /></figure>

* or in parallel:

where $D_1$ and $D_2$ are both ZX-diagrams (themselves composed of the above primitives). We denote by **ZX** the set of ZX-diagrams. In these, information flows from top to bottom, which is in contrast with quantum circuits where it flows from left to right. This is only a matter of convention, as string diagrams, on which the ZX-Calculus formalism relies upon, are oriented vertically.
These diagrams are used to represent linear maps, thanks to the so-called standard interpretation of ZX-diagrams as complex number matrices [1]: $\mathbf{ZX} \to \mathcal{M}(\mathbb{C})^5$. It is inductively defined as:

$$ 
\begin{align*}
\left[ \begin{array}{@{}c@{}} \mathbf{D}_1 \\ \mathbf{D}_2 \end{array} \right]
&= \left[ \begin{array}{@{}c@{}} \cdots \\ \cdots \end{array} \right] \circ \left[ \begin{array}{@{}c@{}} \mathbf{D}_1 \\ \mathbf{D}_2 \end{array} \right] \\
&= \left[ \begin{array}{@{}c@{}} \mathbf{D}_1 \\ \mathbf{D}_2 \end{array} \right] \circ \left[ \begin{array}{@{}c@{}} \cdots \\ \cdots \end{array} \right] \\
&= \left[ \begin{array}{@{}c@{}} \cdots \\ \cdots \end{array} \right] \circ \left[ \begin{array}{@{}c@{}} \mathbf{D}_1 \\ \mathbf{D}_2 \end{array} \right] \circ \left[ \begin{array}{@{}c@{}} \cdots \\ \cdots \end{array} \right] \\
&= \mathrm{id}_{\mathbb{C}^2} = |0\rangle\langle 0| + |1\rangle\langle 1| \\
&= \left[ \begin{array}{@{}c@{}} \circled{2} \\ \circled{2} \end{array} \right]^\dagger = |00\rangle + |11\rangle \\
&= |0^m\rangle\langle 0^n| + e^{i\alpha}|1^m\rangle\langle 1^n| \\
&= \left[ \begin{array}{@{}c@{}} \circled{2} \\ \circled{2} \end{array} \right]
\end{align*}
$$

where $|+\rangle := \frac{|0\rangle+|1\rangle}{\sqrt{2}}$ and $|-\rangle := \frac{|0\rangle-|1\rangle}{\sqrt{2}}$ and $|u\rangle\langle v|$ is the ket bra outer product from Section 2.1.2.

For example, $\mathrm{id}_{\mathbb{C}^2} = |0\rangle\langle 0| + |1\rangle\langle 1| = (1 \ 0) \otimes (\begin{smallmatrix} 1 \\ 0 \end{smallmatrix}) + (0 \ 1) \otimes (\begin{smallmatrix} 0 \\ 1 \end{smallmatrix}) = (\begin{smallmatrix} 1 & 0 \\ 0 & 0 \end{smallmatrix}) + (\begin{smallmatrix} 0 & 0 \\ 0 & 0 \end{smallmatrix}) = (\begin{smallmatrix} 1 & 0 \\ 0 & 1 \end{smallmatrix})$.

Notice that the green (light) and red (dark) nodes only differ from the basis in which they are defined (as $|+\rangle, |-\rangle$) defines an orthonormal basis of $\mathbb{C}^2$ and that they can have an arbitrary number of inputs and outputs. It often happens that a green or red node has a parameter of value 0. In this case, by convention, this angle 0 is omitted. Finally, notice that ⊢ represents exactly the Hadamard gate of quantum circuits. This is not a coincidence, as ZX-diagrams can be seen as a generalization of quantum circuits. In particular, we can map any quantum circuit to a ZX-diagram that represents exactly the same quantum operator:

<figure><img src="image_5.png" /></figure>

and that preserves sequential and parallel compositions. The elementary gates given above are the ones detailed in Table 1.

We can actually map any generalized quantum circuit (i.e. circuit including measure) into a ZX-diagram. Indeed, initializations of qubits are easy to represent: $|0\rangle \mapsto \bullet$ and there exists an extension of the ZX-Calculus [48, 36] that allows the language to represent measurements. In this extension, we represent the environment as $\perp$, which becomes an additional generator of the diagrams (we denote by $\mathbf{ZX}^{\perp}$ this updated set of ZX-diagrams). This generator can also be understood as discarding a qubit. However, contrary to classical data, this action affects the rest of the system. Introducing $\perp$ forces us to change the codomain of the standard interpretation, but we will not give the details here. Simply keep in mind that the measurement in the computational basis ($|0\rangle, |1\rangle$) is represented by $\perp$.

In this way, we can (fairly) easily represent any generalized quantum circuit as a ZX-diagram. But we can actually represent more, and this is an active field of research to try and characterize diagrams that can be put in circuit form (we talk about “extracting a circuit”). First was introduced the notion of causal flow [52] which was then extended to that of “gflow” (for generalized flow) [33]. Some other variations exist [11].

<footnote n="5">⁵To be more precise, the standard interpretation associates to any ZX-diagram in $\mathbf{ZX}[n,m]$ (i.e. with $n$ inputs and $m$ outputs) a complex matrix of dimension $2^m \times 2^n$ i.e. in $\mathcal{M}_{2^m \times 2^n}(\mathbb{C})$.</footnote>
These diagrams are used to represent linear maps, thanks to the so-called standard interpretation of ZX-diagrams as complex number matrices [1]: $\mathbf{ZX} \to \mathcal{M}(\mathbb{C})^5$. It is inductively defined as:

$$ 
\begin{align*}
\left[ \begin{array}{c|c} \multicolumn{2}{c}{\boxed{\begin{array}{c} \vdots \\ D_1 \\ \vdots \\ D_2 \\ \vdots \end{array}}} \\ \hline \boxed{\begin{array}{c} \vdots \\ D_1 \\ \vdots \\ D_2 \\ \vdots \end{array}} \end{array} \right] &= \left[ \begin{array}{c|c} \boxed{\begin{array}{c} \vdots \\ D_2 \\ \vdots \\ D_1 \\ \vdots \end{array}} & \boxed{\begin{array}{c} \vdots \\ D_1 \\ \vdots \\ D_2 \\ \vdots \end{array}} \end{array} \right] \circ \left[ \begin{array}{c|c} \boxed{\begin{array}{c} \vdots \\ D_1 \\ \vdots \\ D_2 \\ \vdots \end{array}} & \boxed{\begin{array}{c} \vdots \\ D_1 \\ \vdots \\ D_2 \\ \vdots \end{array}} \end{array} \right] \\
&= \left[ \begin{array}{c} \boxed{\begin{array}{c} \vdots \\ D_1 \\ \vdots \\ D_2 \\ \vdots \end{array}} \\ \hline \boxed{\begin{array}{c} \vdots \\ D_1 \\ \vdots \\ D_2 \\ \vdots \end{array}} \end{array} \right] \circ \left[ \begin{array}{c} \boxed{\begin{array}{c} \vdots \\ D_1 \\ \vdots \\ D_2 \\ \vdots \end{array}} \\ \hline \boxed{\begin{array}{c} \vdots \\ D_1 \\ \vdots \\ D_2 \\ \vdots \end{array}} \end{array} \right] \\
&= \mathrm{id}_{\mathbb{C}^2} = |0\rangle\langle 0| + |1\rangle\langle 1| \\
&= \left[ \begin{array}{c} \boxed{\begin{array}{c} \vdots \\ D_1 \\ \vdots \\ D_2 \\ \vdots \end{array}} \\ \hline \boxed{\begin{array}{c} \vdots \\ D_1 \\ \vdots \\ D_2 \\ \vdots \end{array}} \end{array} \right]^\dagger = |00\rangle + |11\rangle \\
&= \boxed{\begin{array}{c} \begin{array}{c} \vdots \\ D_1 \\ \vdots \\ D_2 \\ \vdots \end{array} \\ \hline \begin{array}{c} \vdots \\ D_1 \\ \vdots \\ D_2 \\ \vdots \end{array} \end{array}} = |0^m\rangle\langle 0^n| + e^{i\alpha}|1^m\rangle\langle 1^n| \\
&= \left[ \begin{array}{c} \boxed{\begin{array}{c} \vdots \\ D_1 \\ \vdots \\ D_2 \\ \vdots \end{array}} \\ \hline \boxed{\begin{array}{c} \vdots \\ D_1 \\ \vdots \\ D_2 \\ \vdots \end{array}} \end{array} \right] = |+^m\rangle\langle +^n| + e^{i\alpha} |-^m\rangle\langle -^n|
\end{align*}
$$

where $|+\rangle := \frac{|0\rangle+|1\rangle}{\sqrt{2}}$ and $|-\rangle := \frac{|0\rangle-|1\rangle}{\sqrt{2}}$ and $|u\rangle\langle v|$ is the ket bra outer product from Section 2.1.2.

For example, $\mathrm{id}_{\mathbb{C}^2} = |0\rangle\langle 0| + |1\rangle\langle 1| = (1 \ 0) \otimes (\begin{smallmatrix} 1 \\ 0 \end{smallmatrix}) + (0 \ 1) \otimes (\begin{smallmatrix} 0 \\ 1 \end{smallmatrix}) = (\begin{smallmatrix} 1 & 0 \\ 0 & 0 \end{smallmatrix}) + (\begin{smallmatrix} 0 & 0 \\ 0 & 0 \end{smallmatrix}) = (\begin{smallmatrix} 1 & 0 \\ 0 & 1 \end{smallmatrix})$.

Notice that the green (light) and red (dark) nodes only differ from the basis in which they are defined (as $|+\rangle, |-\rangle$) defines an orthonormal basis of $\mathbb{C}^2$ and that they can have an arbitrary number of inputs and outputs. It often happens that a green or red node has a parameter of value 0. In this case, by convention, this angle 0 is omitted. Finally, notice that $\otimes$ represents exactly the Hadamard gate of quantum circuits. This is not a coincidence, as ZX-diagrams can be seen as a generalization of quantum circuits. In particular, we can map any quantum circuit to a ZX-diagram that represents exactly the same quantum operator:

<figure><img src="image_7.png" /></figure>

and that preserves sequential and parallel compositions. The elementary gates given above are the ones detailed in Table 1.

We can actually map any generalized quantum circuit (i.e. circuit including measure) into a ZX-diagram. Indeed, initializations of qubits are easy to represent: $|0\rangle \mapsto \bullet$, and there exists an extension of the ZX-Calculus [48, 36] that allows the language to represent measurements. In this extension, we represent the environment as $\perp$, which becomes an additional generator of the diagrams (we denote by $\mathbf{ZX}^{\perp}$ this updated set of ZX-diagrams). This generator can also be understood as discarding a qubit. However, contrary to classical data, this action affects the rest of the system. Introducing $\perp$ forces us to change the codomain of the standard interpretation, but we will not give the details here. Simply keep in mind that the measurement in the computational basis ($|0\rangle, |1\rangle$) is represented by $\perp$.

In this way, we can (fairly) easily represent any generalized quantum circuit as a ZX-diagram. But we can actually represent more, and this is an active field of research to try and characterize diagrams that can be put in circuit form (we talk about “extracting a circuit”). First was introduced the notion of causal flow [52] which was then extended to that of “gflow” (for generalized flow) [33]. Some other variations exist [11].

<footnote n="5">⁵To be more precise, the standard interpretation associates to any ZX-diagram in $\mathbf{ZX}[n,m]$ (i.e. with $n$ inputs and $m$ outputs) a complex matrix of dimension $2^m \times 2^n$ i.e. in $\mathcal{M}_{2^m \times 2^n}(\mathbb{C})$.</footnote>
Quantum circuits, however, are not the only computational model one might want ZX-diagrams to compile to. Indeed, it so happens that the primitives of the ZX-Calculus quite naturally match those of *lattice surgery* [55], a scheme for error correction [75, 95]. In particular, ZX-diagrams implementing a (physical) lattice surgery procedure features a special notion of flow, the *PF flow* (for Pauli fusion flow) [54].

### 5.1.2 Verified Properties

The strength of ZX-Calculus comes from its powerful equational theory. This equational theory allows to define equivalence classes of ZX-diagrams and to conveniently decide whether two different diagrams represent the same quantum operator.

This question can be asked for quantum circuits as well, as two different circuits may represent the same operator (e.g. $H^2 = Id$). Some such equational theories exist for quantum circuits [169, 6], but none, as of today, for a universal fragment of quantum mechanics (notice that in [179] a completeness theorem is given for the interaction between measurements and pure parts of the circuit, but crucially one for the pure part itself is not provided but only assumed).

The main difference between the two formalisms is that the equational theory of the ZX-Calculus allows for a powerful result in this language, aggregated under the paradigm “only connectivity matters”. This result states that we can treat any ZX-diagram as an undirected open graph, where the Hadamard box and the green and red nodes are considered as vertices. In particular, any (open) graph isomorphism is an allowed transformation.

**Example 5.1.** $\simeq$ because the two diagrams can be obtained from one another by simply “moving their nodes around” (while keeping inputs and outputs fixed).

<figure><img src="image_6.png" /></figure>

This result also allows us to unambiguously represent a horizontal wire. For instance:

<figure><img src="image_7.png" /></figure>

This “meta”-rule, that all isomorphisms of open graphs are allowed, constitutes the backbone of the ZX-Calculus. In what follows, different sets of axioms, that satisfy different needs, will be presented, but this meta-rule will always be there implicitly.

When two diagrams $D_1$ and $D_2$ are proven to be equal using the equational theory $\mathcal{T}$, we write $\mathcal{T} \vdash D_1 = D_2$. The axiomatization zx for the ZX-Calculus can be found in Figure 5, and it was recently proven to be complete for the standard interpretation [189]:

**Theorem 1.** $\mathbf{ZX/zx}$ is complete with respect to $[\cdot]$:

$$ \forall D_1, D_2 \in \mathbf{ZX}, \quad [[D_1]] = [[D_2]] \iff zx \vdash D_1 = D_2 $$

Here $\mathbf{ZX/zx}$ represents the quotient of $\mathbf{ZX}$ by the equational theory $zx$. The completeness property is fundamental. It allows us to reason on quantum processes through diagrammatic transformations rather than by matrix computations. In particular, it tells us that whenever two diagrams represent the same quantum operator, they can be turned into one another using only the rules of $zx$.

It is customary in quantum computing to work with particular (restricted) sets of gates. For a lot of such restrictions, there exist complete axiomatizations [85, 101, 102, 100, 103, 104]. The ZX-
Quantum circuits, however, are not the only computational model one might want ZX-diagrams to compile to. Indeed, it so happens that the primitives of the ZX-Calculus quite naturally match those of lattice surgery [55], a scheme for error correction [75, 95]. In particular, ZX-diagrams implementing a (physical) lattice surgery procedure features a special notion of flow, the PF flow (for Pauli fusion flow) [54].

### 5.1.2 Verified Properties

The strength of ZX-Calculus comes from its powerful equational theory. This equational theory allows to define equivalence classes of ZX-diagrams and to conveniently decide whether two different diagrams represent the same quantum operator.

This question can be asked for quantum circuits as well, as two different circuits may represent the same operator (e.g. $H^2 = Id$). Some such equational theories exist for quantum circuits [169, 6], but none, as of today, for a universal fragment of quantum mechanics (notice that in [179] a completeness theorem is given for the interaction between measurements and pure parts of the circuit, but crucially one for the pure part itself is not provided but only assumed).

The main difference between the two formalisms is that the equational theory of the ZX-Calculus allows for a powerful result in this language, aggregated under the paradigm “only connectivity matters”. This result states that we can treat any ZX-diagram as an undirected open graph, where the Hadamard box and the green and red nodes are considered as vertices. In particular, any (open) graph isomorphism is an allowed transformation.

**Example 5.1.** $\simeq$ because the two diagrams can be obtained from one another by simply “moving their nodes around” (while keeping inputs and outputs fixed).

<figure><img src="image_8.png" /></figure>

This result also allows us to unambiguously represent a horizontal wire. For instance:

<figure><img src="image_9.png" /></figure>

This “meta”-rule, that all isomorphisms of open graphs are allowed, constitutes the backbone of the ZX-Calculus. In what follows, different sets of axioms, that satisfy different needs, will be presented, but this meta-rule will always be there implicitly.

When two diagrams $D_1$ and $D_2$ are proven to be equal using the equational theory $\mathcal{T}$, we write $\mathcal{T} \vdash D_1 = D_2$. The axiomatization zx for the ZX-Calculus can be found in Figure 5, and it was recently proven to be complete for the standard interpretation [189]:

**Theorem 1.** $\mathcal{ZX}/zx$ is complete with respect to $[\cdot]$:

$$ \forall D_1, D_2 \in \mathcal{ZX}, \quad [[D_1]] = [[D_2]] \iff zx \vdash D_1 = D_2 $$

Here $\mathcal{ZX}/zx$ represents the quotient of $\mathcal{ZX}$ by the equational theory $zx$. The completeness property is fundamental. It allows us to reason on quantum processes through diagrammatic transformations rather than by matrix computations. In particular, it tells us that whenever two diagrams represent the same quantum operator, they can be turned into one another using only the rules of $zx$.

It is customary in quantum computing to work with particular (restricted) sets of gates. For a lot of such restrictions, there exist complete axiomatizations [85, 101, 102, 100, 103, 104]. The ZX-
<figure><img src="image_8.png" /><figcaption>Figure 5: The equational theory $zx^6$. All rules – provably – hold in their upside-down and color-swapped (between green and red) versions.</figcaption></figure>

Calculus with measurements has a similar completeness result for $ZX^{\pm}/zx^{\pm}$ [36] with an updated set of rules $zx^{\pm}$ which we will not give here for conciseness purposes.

Some properties of quantum protocols or algorithms can then be verified by diagram transformations. To give the reader the flavor of such verifications, we detail the example of superdense coding.

**Example 5.2 (Superdense Coding).** The idea of the superdense coding protocol is to transmit two classical bits using a single qubit. This is not possible in general, but it is when the two parties initially share an entangled pair of qubits. The protocol goes as follows:

* Alice and Bob initially share the (previously defined) EPR pair $\beta_{00} = \frac{|00\rangle + |11\rangle}{\sqrt{2}}$, and Alice moreover has two bits she wants to send to Bob

* Alice applies $\sigma_X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}$ to her qubit if her first bit is 1, then $\sigma_Z = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix}$ if her second bit is 1

* Alice sends her qubit to Bob

* Bob applies a CNOT between his qubit and the one he received from Alice, then a H gate on his qubit, and finally measures his two qubits

<footnote n="6">⁶The way we denote the equations relates to their names in broader literature if such exists, and more informal names if not. (S) is the spider rule, ($I_g$) and ($I_r$) are the green and red identity rules, (E) is the empty diagram rule, (CP) the copy rule, (B) the bialgebra rule, (EU) the Euler angles rule, (HD) the Hadamard decomposition and (H) the Hadamard colour change rule.</footnote>
<figure><img src="image_10.png" /><figcaption>Figure 5: The equational theory $zx^6$. All rules – provably – hold in their upside-down and color-swapped (between green and red) versions.</figcaption></figure>

Calculus with measurements has a similar completeness result for $ZX^{\pm}/zx^{\pm}$ [36] with an updated set of rules $zx^{\pm}$ which we will not give here for conciseness purposes.

Some properties of quantum protocols or algorithms can then be verified by diagram transformations. To give the reader the flavor of such verifications, we detail the example of superdense coding.

**Example 5.2 (Superdense Coding).** The idea of the superdense coding protocol is to transmit two classical bits using a single qubit. This is not possible in general, but it is when the two parties initially share an entangled pair of qubits. The protocol goes as follows:

* Alice and Bob initially share the (previously defined) EPR pair $\beta_{00} = \frac{|00\rangle + |11\rangle}{\sqrt{2}}$, and Alice moreover has two bits she wants to send to Bob

* Alice applies $\sigma_X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}$ to her qubit if her first bit is 1, then $\sigma_Z = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix}$ if her second bit is 1

* Alice sends her qubit to Bob

* Bob applies a CNOT between his qubit and the one he received from Alice, then a H gate on his qubit, and finally measures his two qubits

<footnote n="6">⁶The way we denote the equations relates to their names in broader literature if such exists, and more informal names if not. (S) is the spider rule, ($I_g$) and ($I_r$) are the green and red identity rules, (E) is the empty diagram rule, (CP) the copy rule, (B) the bialgebra rule, (EU) the Euler angles rule, (HD) the Hadamard decomposition and (H) the Hadamard colour change rule.</footnote>
This protocol can be represented with a ZX-diagram as follows.

<figure><img src="image_9.png" /></figure>

It is then possible to verify that Bob eventually does get (copies of) Alice's bits, using the equational
theory (although the whole derivation is not given here):

<figure><img src="image_10.png" /></figure>

We can hence see that data is transmitted from Alice to Bob, without any loss. Interestingly, this pro-
tocol can be extended for secure communication between the two parties [192]. The larger protocol
uses instances of the smaller one to also check whether an eavesdropper has tried intercepting or
copying data.

If Bob is aware that the data he received was compromised, he can abort everything by simply discarding his qubits, so that the eavesdropper (Eve) gets absolutely no information:

<figure><img src="image_11.png" /></figure>

where *U* denotes an unknown operator applied by *Eve* to the qubit she intercepted. Notice here how
no information can pass from Alice to Eve. No information is retrieved by the latter.

A plethora of quantum protocols have been verified with ZX-Calculus in a similar manner [92].
Note however that the theory is ever evolving, and in particular, $\oplus$ was not introduced in the lan-
guage at that time, so the author had to use a trick to make up for the absence of measurement
(namely case-based reasoning).
This protocol can be represented with a ZX-diagram as follows.

<figure><img src="image_11.png" /></figure>

It is then possible to verify that Bob eventually does get (copies of) Alice's bits, using the equational theory (although the whole derivation is not given here):

<figure><img src="image_12.png" /></figure>

We can hence see that data is transmitted from Alice to Bob, without any loss. Interestingly, this protocol can be extended for secure communication between the two parties [192]. The larger protocol uses instances of the smaller one to also check whether an eavesdropper has tried intercepting or copying data.

If Bob is aware that the data he received was compromised, he can abort everything by simply discarding his qubits, so that the eavesdropper (Eve) gets absolutely no information:

<figure><img src="image_13.png" /></figure>

where $U$ denotes an unknown operator applied by Eve to the qubit she intercepted. Notice here how no information can pass from Alice to Eve. No information is retrieved by the latter.

A plethora of quantum protocols have been verified with ZX-Calculus in a similar manner [92]. Note however that the theory is ever evolving, and in particular, $\hat{=}^-$ was not introduced in the language at that time, so the author had to use a trick to make up for the absence of measurement (namely case-based reasoning).
### 5.1.3 Algorithms and Tools

It is possible to manipulate ZX-diagrams in a computer-verified way. For instance, Quantomatic [110] allows the users to define at the same time diagrams in graphical form and equational theories. It is also possible to work with user-defined nodes in the diagram so that even though $\perp$ is not part of the “vanilla” ZX-Calculus, it can be defined as a new node. It is then possible in the tool to manipulate diagrams in a way that satisfies the equational theory, and even to define rewriting strategies that can be then applied in an automated way.

The verification of protocols and programs using the ZX-Calculus relies on diagrammatic equivalence. This problem, in general, is at least QMA-complete, [29, 98] (the quantum counterpart of NP-completeness). This problem is linked to the one of simplification/optimization, which asks how a quantum operator can be simplified, given a particular metric (e.g. the number of non-Clifford gates). Indeed, for instance if $D_1$ and $D_2$ are two diagrams representing the same unitary (i.e. $[D_1] = [D_2]$), then simplifying $D_2^\dagger \circ D_1$ should ideally get us to the identity.

In the case of the Clifford fragment (obtained when the angles in $\bigcirc_{\substack{n \\ m}}^\alpha$ and $\bigcirc_{\substack{n \\ m}}^\alpha$ are restricted to multiples of $\pi/2$), there exists a strategy that reduces the diagram in (pseudo-)normal form [10]. When this algorithm terminates, the resulting diagram is of size $O(n^2)$ where $n$ is the number of inputs and outputs in the diagram. The algorithm is polynomial in the overall size of the diagram it is applied on.

Turning an arbitrary diagram into a normal form can be done in principle [103], however, the complexity of this algorithm is EXPSPACE for universal fragments. So this approach is obviously not preferred in general. However, one can use the ideas of the algorithm for the Clifford fragment as a starting point to get a rewriting strategy for the general case. Applications to quantum circuits and improvements on this strategy can be found in the literature [109, 53, 60, 11], and implementations in the PyZX tool [108]. This tool can in particular be used to tackle circuit equivalence verification, using a different but related approach to that of Section 5.2 below. The formalism used later is that of *path-sums*, where morphisms were showed in [123, 190] to be essentially equivalent to ZX-diagrams, allowing us to apply strategies for path-sums to the ZX-Calculus and vice-versa. Next Section is devoted to we introducing the path-sum formalism and its use for circuits verification.

## 5.2 Path-Sum circuit Equivalence Verification

Path-sums are a recent alternative direction for verifying the equivalence between quantum circuits [4, 5]. In this section we briefly present it, together with the main verification related achievements.

Note that a generalization of path-sum semantics is introduced in Section 7.2, for parametrized families of circuits. For sake of readability, conciseness and coherence with this further content, in the coming paragraphs we slightly simplify path-sums related notations. We refer the reader to the original definitions [4, 5] for the full formalism and underlying mathematical structures.

### 5.2.1 Semantical Model

The standard semantics for quantum circuits is the matrix formalism, introduced in Section 2.1.5. It associates to each quantum circuit C a matrix $\mathbf{Mat}(C)$ and it interprets the behavior of this circuit as a function $|x\rangle \rightarrow \mathbf{Mat}(C) \cdot |x\rangle$ from kets to kets, where $\cdot$ stands for the usual matrix product.

Notice that this standard semantics builds on an intermediary object– the matrix–to derive and interprets the functional behavior of circuits. And it does so by use of a higher-order function– the matrix product. Contrarily, path-sums are a straight construction of the *input/output* function
### 5.1.3 Algorithms and Tools

It is possible to manipulate ZX-diagrams in a computer-verified way. For instance, Quantomatic [110] allows the users to define at the same time diagrams in graphical form and equational theories. It is also possible to work with user-defined nodes in the diagram so that even though $\perp$ is not part of the “vanilla” ZX-Calculus, it can be defined as a new node. It is then possible in the tool to manipulate diagrams in a way that satisfies the equational theory, and even to define rewriting strategies that can be then applied in an automated way.

The verification of protocols and programs using the ZX-Calculus relies on diagrammatic equivalence. This problem, in general, is at least QMA-complete, [29, 98] (the quantum counterpart of NP-completeness). This problem is linked to the one of simplification/optimization, which asks how a quantum operator can be simplified, given a particular metric (e.g. the number of non-Clifford gates). Indeed, for instance if $D_1$ and $D_2$ are two diagrams representing the same unitary (i.e. $[D_1] = [D_2]$), then simplifying $D_2^\dagger \circ D_1$ should ideally get us to the identity.

In the case of the Clifford fragment (obtained when the angles in $\bigcirc_{\substack{n \\ m}}^\alpha$ and $\bigcirc_{\substack{n \\ m}}^\alpha$ are restricted to multiples of $\pi/2$), there exists a strategy that reduces the diagram in (pseudo-)normal form [10]. When this algorithm terminates, the resulting diagram is of size $O(n^2)$ where $n$ is the number of inputs and outputs in the diagram. The algorithm is polynomial in the overall size of the diagram it is applied on.

Turning an arbitrary diagram into a normal form can be done in principle [103], however, the complexity of this algorithm is EXPSPACE for universal fragments. So this approach is obviously not preferred in general. However, one can use the ideas of the algorithm for the Clifford fragment as a starting point to get a rewriting strategy for the general case. Applications to quantum circuits and improvements on this strategy can be found in the literature [109, 53, 60, 11], and implementations in the PyZX tool [108]. This tool can in particular be used to tackle circuit equivalence verification, using a different but related approach to that of Section 5.2 below. The formalism used later is that of *path-sums*, where morphisms were showed in [123, 190] to be essentially equivalent to ZX-diagrams, allowing us to apply strategies for path-sums to the ZX-Calculus and vice-versa. Next Section is devoted to we introducing the path-sum formalism and its use for circuits verification.

## 5.2 Path-Sum circuit Equivalence Verification

Path-sums are a recent alternative direction for verifying the equivalence between quantum circuits [4, 5]. In this section we briefly present it, together with the main verification related achievements.

Note that a generalization of path-sum semantics is introduced in Section 7.2, for parametrized families of circuits. For sake of readability, conciseness and coherence with this further content, in the coming paragraphs we slightly simplify path-sums related notations. We refer the reader to the original definitions [4, 5] for the full formalism and underlying mathematical structures.

### 5.2.1 Semantical Model

The standard semantics for quantum circuits is the matrix formalism, introduced in Section 2.1.5. It associates to each quantum circuit $C$ a matrix $\mathbf{Mat}(C)$ and it interprets the behavior of this circuit as a function $|x\rangle \rightarrow \mathbf{Mat}(C) \cdot |x\rangle$ from kets to kets, where $\cdot$ stands for the usual matrix product.

Notice that this standard semantics builds on an intermediary object– the matrix–to derive and interprets the functional behavior of circuits. And it does so by use of a higher-order function– the matrix product. Contrarily, path-sums are a straight construction of the *input/output* function
performed by circuits, enabling compositional reasoning.

Concretely, a path-sum $PS(x)$ is a quantum register state (a ket), parametrized by an input basis ket $|x\rangle$ and defined as the sum of kets

$$PS(x) ::= \frac{1}{\sqrt{2}^n} \sum_{k=0}^{2^n-1} e^{\frac{2 \cdot \pi \cdot i \cdot P_k(x)}{2^m}} |\phi_k(x)\rangle \quad (2)$$

where the $P_k(x)$ are called phase polynomials while the $|\phi_k(x)\rangle$ are basis-kets. This representation is closed under functional composition and Kronecker product. For instance, if

$$C : |x\rangle \mapsto PS(x) = \frac{1}{\sqrt{2}^n} \sum_{k=0}^{2^n-1} e^{\frac{2 \cdot \pi \cdot i \cdot P_k(x)}{2^m}} |\phi_k(x)\rangle,$$

$$C' : |y\rangle \mapsto PS'(y) = \frac{1}{\sqrt{2}^n} \sum_{k=0}^{2^n-1} e^{\frac{2 \cdot \pi \cdot i \cdot P_k'(y)}{2^m}} |\phi_k'(y)\rangle,$$

then their parallel combination $parallel(C, C')$ sends $|x\rangle \otimes |y\rangle$ to:

$$\frac{1}{\sqrt{2}^{n+n'}} \sum_{j=0}^{2^{n+n'}-1} e^{\frac{2 \cdot \pi \cdot i \cdot \left(2^{m'} \cdot P_{j/2^n}(x)+2^{m'} \cdot P'_{j/2^n}(y)\right)}{2^{m+m'}}} |\phi_{j/2^n}(x)\rangle \otimes |\phi'_{j/2^n}(y)\rangle$$

The sequential combination of quantum circuits C and C' receives a similar compositional definition, parametrized by path-sums components for circuits C and C'.

### 5.2.2 Path-Sums Reduction

While path-sums compose nicely, a given linear map (eg. the input/output function for a quantum circuit) does not have a unique representative path-sum. Hence, given two different path-sum, how to decide whether they both encode the behavior of a given circuit? To tackle this problem, an equivalence relation is defined with a few, simple rules that can be oriented. As an example, the *HH* rule enables to simplify a path-sum expression over the reduction from a sequence of two consecutive Hadamard gates to the identity–see Figure 6. All these rules transform a path-sum into an equivalent one, with a lower number of *path variables* (parameter *n* in the notation of Equation 2).

$$\frac{PS(x) = \frac{1}{\sqrt{2}^{n+1}} \sum_{j=0}^{2^n} \sum_{k=0}^{2^n} e^{\frac{1}{2} \cdot \pi \cdot i \cdot \left( \frac{1}{2} j(k_i + Q_k(x)) + P_k(x) \right)} |\phi_k(x)\rangle}{PS(x) = \frac{1}{\sqrt{2}^{n+1}} \sum_{k=0}^{2^n} e^{\frac{1}{2} \cdot \pi \cdot i \cdot P[i:=Q_k(x)]_k(x)} |\phi[i:=Q_k(x)]_k(x)\rangle} \quad HH$$

<caption>Figure 6: The *HH* path-sum transformation rule</caption>

We refer the desirous reader to [5, 4] for an exhaustive exposition of the corresponding proof system. It was proved strongly normalizing, meaning that every sequence of reduction rules application terminates with an irreducible path-sum. Furthermore, finding and applying such a normalizing sequence is feasible in time polynomial in the width of the circuit at stake, which makes the overall reduction procedure tractable.
performed by circuits, enabling compositional reasoning.

Concretely, a path-sum $PS(x)$ is a quantum register state (a ket), parametrized by an input basis ket $|x\rangle$ and defined as the sum of kets

$$PS(x) ::= \frac{1}{\sqrt{2}^n} \sum_{k=0}^{2^n-1} e^{\frac{2\pi i \cdot P_k(x)}{2^m}} |\phi_k(x)\rangle \quad (2)$$

where the $P_k(x)$ are called phase polynomials while the $|\phi_k(x)\rangle$ are basis-kets. This representation is closed under functional composition and Kronecker product. For instance, if

$$C : |x\rangle \mapsto PS(x) = \frac{1}{\sqrt{2}^n} \sum_{k=0}^{2^n-1} e^{\frac{2\pi i \cdot P_k(x)}{2^m}} |\phi_k(x)\rangle,$$

$$C' : |y\rangle \mapsto PS'(y) = \frac{1}{\sqrt{2}^{n'}} \sum_{k=0}^{2^{n'}-1} e^{\frac{2\pi i \cdot P_k'(y)}{2^{m'}}} |\phi_k'(y)\rangle,$$

then their parallel combination parallel(C, C') sends $|x\rangle \otimes |y\rangle$ to:

$$\frac{1}{\sqrt{2}^{n+n'}} \sum_{j=0}^{2^{n+n'}-1} e^{\frac{2\pi i \cdot \left(2^{m'} \cdot P_{j/2^n}(x)+2^m \cdot P'_{j/2^n}(y)\right)}{2^{m+m'}}} |\phi_{j/2^n}(x)\rangle \otimes |\phi'_{j/2^n}(y)\rangle$$

The sequential combination of quantum circuits C and C' receives a similar compositional definition, parametrized by path-sums components for circuits C and C'.

### 5.2.2 Path-Sums Reduction

While path-sums compose nicely, a given linear map (eg. the input/output function for a quantum circuit) does not have a unique representative path-sum. Hence, given two different path-sum, how to decide whether they both encode the behavior of a given circuit? To tackle this problem, an equivalence relation is defined with a few, simple rules that can be oriented. As an example, the HH rule enables to simplify a path-sum expression over the reduction from a sequence of two consecutive Hadamard gates to the identity–see Figure 6. All these rules transform a path-sum into an equivalent one, with a lower number of path variables (parameter n in the notation of Equation 2).

$$\frac{PS(x) = \frac{1}{\sqrt{2}^{n+1}} \sum_{j=0}^{2^n} \sum_{k=0}^{2^n} e^{\frac{1}{2} \cdot \pi \cdot i \left( \frac{1}{2} j(k_i + Q_k(x)) + P_k(x) \right)} |\phi_k(x)\rangle}{PS(x) = \frac{1}{\sqrt{2}^{n+1}} \sum_{k=0}^{2^n} e^{\frac{1}{2} \cdot \pi \cdot i \left( P[i:=Q_k(x)]_k(x) \right)} |\phi[i:=Q_k(x)]_k(x)\rangle} \quad HH$$

<caption>Figure 6: The HH path-sum transformation rule</caption>

We refer the desirous reader to [5, 4] for an exhaustive exposition of the corresponding proof system. It was proved strongly normalizing, meaning that every sequence of reduction rules application terminates with an irreducible path-sum. Furthermore, finding and applying such a normalizing sequence is feasible in time polynomial in the width of the circuit at stake, which makes the overall reduction procedure tractable.
### 5.2.3 Verified Properties

Hence, path-sums provide a human-readable formalism for the interpretation of quantum circuits as ket data functions. Furthermore, it is given a polynomial normalization procedure, based on a restricted set of rewriting rules. The method was probed against both circuit equivalence and functional specifications verification. More precisely:

**Translation validation** consists, for a given quantum algorithm, in (1) computing the path-sums for both a non-optimized and an optimized circuit realization and (2) using the normalization procedure for the automatic checking of their equivalence. It was performed on various quantum routine instances (Grover, modular adder, Galois field multiplication, etc) of various size (up to several dozens of qubits). Interestingly, the methods proved as efficient for identifying non-equivalence (over erroneous instances) as for checking equivalence.

**Quantum algorithms verification** consists in verifying whether a given circuit instance respects its functional description. It was performed for instances of similar case studies as for the translation validation (QFT, Hidden Shift [187]), with up to a hundred qubits.

As conclusion, the path-sum formalism provides a fully automatized procedure for verifying the equivalence between two circuits. Hence, given two quantum circuits, the latter being a supposed optimized version of the former, path-sums treatment enables us to verify that they implement the same quantum function. Since path-sums perform internal complexity reduction, an open direction is a search for efficient heuristics extracting an optimized quantum circuit from reduced path-sums. As mentioned in Section 5.1, this problem is closely linked to the reduction of ZX-Calculus diagrams. So, in its general form, it faces the same complexity limitations. The search for efficient reduction procedure applying to identified useful fragments could then both benefit from and feed advances in the ZX setting.

In its present state of development, using path-sums for quantum algorithm verification is restricted to compilation time, when program parameters are instantiated. Furthermore, a new run of the path-sum reduction is required at each new call of a given quantum function. In Section 7.2 we introduce the QBRICKS language, whose semantics is based on a parametrized extension of path-sums. It enables the verification, once for all, of parametrized programs, holding for any possible future parameter instances–yet at the price of full automation as the manipulation of parametrized path-sums requires first-order logic reasoning.

## 5.3 Quantum abstract interpretation

The techniques presented so far target an exhaustive functional description of a quantum circuit. Because of the intrinsic complexity of quantum computing, their use is limited, in particular by the size of circuits. As illustrated in the benchmarks summed up in Section 5.2.3, path-sums reduction enabled, for instance, the verification of quantum circuits up to a hundred of qubits.

To push the boundary, a possible strategy comes from Abstract Interpretation (see Section 3.3). There, one does not target an exhaustive description of the functional behavior of a circuit, but an over-approximation of it. Such a framework relies on:

* the identification of a conveniently structured set of properties of interest (the abstract domain);

* sound abstraction and concretization to/from this abstract domain;

* reasoning tools for the abstract domain.
### 5.2.3 Verified Properties

Hence, path-sums provide a human-readable formalism for the interpretation of quantum circuits as ket data functions. Furthermore, it is given a polynomial normalization procedure, based on a restricted set of rewriting rules. The method was probed against both circuit equivalence and functional specifications verification. More precisely:

**Translation validation** consists, for a given quantum algorithm, in (1) computing the path-sums for both a non-optimized and an optimized circuit realization and (2) using the normalization procedure for the automatic checking of their equivalence. It was performed on various quantum routine instances (Grover, modular adder, Galois field multiplication, etc) of various size (up to several dozens of qubits). Interestingly, the methods proved as efficient for identifying non-equivalence (over erroneous instances) as for checking equivalence.

**Quantum algorithms verification** consists in verifying whether a given circuit instance respects its functional description. It was performed for instances of similar case studies as for the translation validation (QFT, Hidden Shift [187]), with up to a hundred qubits.

As conclusion, the path-sum formalism provides a fully automatized procedure for verifying the equivalence between two circuits. Hence, given two quantum circuits, the latter being a supposed optimized version of the former, path-sums treatment enables us to verify that they implement the same quantum function. Since path-sums perform internal complexity reduction, an open direction is a search for efficient heuristics extracting an optimized quantum circuit from reduced path-sums. As mentioned in Section 5.1, this problem is closely linked to the reduction of ZX-Calculus diagrams. So, in its general form, it faces the same complexity limitations. The search for efficient reduction procedure applying to identified useful fragments could then both benefit from and feed advances in the ZX setting.

In its present state of development, using path-sums for quantum algorithm verification is restricted to compilation time, when program parameters are instantiated. Furthermore, a new run of the path-sum reduction is required at each new call of a given quantum function. In Section 7.2 we introduce the QBRICKS language, whose semantics is based on a parametrized extension of path-sums. It enables the verification, once for all, of parametrized programs, holding for any possible future parameter instances–yet at the price of full automation as the manipulation of parametrized path-sums requires first-order logic reasoning.

## 5.3 Quantum abstract interpretation

The techniques presented so far target an exhaustive functional description of a quantum circuit. Because of the intrinsic complexity of quantum computing, their use is limited, in particular by the size of circuits. As illustrated in the benchmarks summed up in Section 5.2.3, path-sums reduction enabled, for instance, the verification of quantum circuits up to a hundred of qubits.

To push the boundary, a possible strategy comes from Abstract Interpretation (see Section 3.3). There, one does not target an exhaustive description of the functional behavior of a circuit, but an over-approximation of it. Such a framework relies on:

* the identification of a conveniently structured set of properties of interest (the abstract domain);

* sound abstraction and concretization to/from this abstract domain;

* reasoning tools for the abstract domain.
In [149], the author introduces such an abstract interpretation of quantum states based on their entanglement structure. The technique enables to identify mutually separable sub-registers. It is useful, for example, for uncomputation, qubit discarding or identifying a convenient decomposition for further analysis of a state.

A more recent development on abstract interpretation applied to quantum process is [199], in which the authors define abstract domains made of tuples of partial projections over quantum sub-registers. Intuitively, the idea is to overcome the exponential complexity of quantum states by decomposing them into sub-spaces. Interestingly, the method was implemented and evaluation results are provided. In particular, thus abstraction enabled to characterize the invariant in the main loop structuring the Grover search algorithm and to prove it for instances of width up to 300 qubits.

## 5.4 Toward Integrated Verified Optimization: VOQC

A noticeable effort for an integrated verified quantum optimization was recently led through the development of a *Verified Optimizer for Quantum Circuits* (VOQC–pronounced ‘vox’) [91]. As main aspects, in comparison to ZX- and path-sum calculus, VOQC:

* is integrated into a core programming environment and applies on circuits issued from parametrized programs;

* not only validates the equivalence between an input quantum circuit and a candidate optimized version of it, but also provides the formally verified optimization procedure, directly generating this optimized version.

<figure><img src="image_12.png" /><figcaption>Figure 7: A simplified view of VOQC architecture</figcaption></figure>

### 5.4.1 Architecture

In Figure 7 we give a simplified view of VOQC architecture: it relies on an Intermediate Representation Language named SQIR. Since it may also be used as a verified programming environment, SQIR is introduced and developed *per se* in a dedicated section below (Section 7.3). In the present context, we can think of it as a core language generating parametrized quantum circuits. Then, for any instance of the parameters, VOQC extracts the corresponding sequence of operations, applies an optimization procedure upon this sequence of operations and extracts back an optimized proved equivalent SQIR quantum circuit. Furthermore,
In [149], the author introduces such an abstract interpretation of quantum states based on their entanglement structure. The technique enables to identify mutually separable sub-registers. It is useful, for example, for uncomputation, qubit discarding or identifying a convenient decomposition for further analysis of a state.

A more recent development on abstract interpretation applied to quantum process is [199], in which the authors define abstract domains made of tuples of partial projections over quantum sub-registers. Intuitively, the idea is to overcome the exponential complexity of quantum states by decomposing them into sub-spaces. Interestingly, the method was implemented and evaluation results are provided. In particular, thus abstraction enabled to characterize the invariant in the main loop structuring the Grover search algorithm and to prove it for instances of width up to 300 qubits.

## 5.4 Toward Integrated Verified Optimization: VOQC

A noticeable effort for an integrated verified quantum optimization was recently led through the development of a *Verified Optimizer for Quantum Circuits* (VOQC–pronounced ‘vox’) [91]. As main aspects, in comparison to ZX- and path-sum calculus, VOQC:

* is integrated into a core programming environment and applies on circuits issued from parametrized programs;

* not only validates the equivalence between an input quantum circuit and a candidate optimized version of it, but also provides the formally verified optimization procedure, directly generating this optimized version.

<figure><img src="image_14.png" /><figcaption>Figure 7: A simplified view of VOQC architecture</figcaption></figure>

### 5.4.1 Architecture

In Figure 7 we give a simplified view of VOQC architecture: it relies on an Intermediate Representation Language named SQIR. Since it may also be used as a verified programming environment, SQIR is introduced and developed *per se* in a dedicated section below (Section 7.3). In the present context, we can think of it as a core language generating parametrized quantum circuits. Then, for any instance of the parameters, VOQC extracts the corresponding sequence of operations, applies an optimization procedure upon this sequence of operations and extracts back an optimized proved equivalent SQIR quantum circuit. Furthermore,
* in addition to optimization, VOQC also contains some circuit mapping functionalities. They perform further circuit transformation so that the output circuits fit to specific quantum architecture qubit connectivity constraints. This functionality is a preliminary address to the problem raised as first bullet in Section 2.3.3,

* VOQC environment also provides both ways compilations between SQIR and the standard assembly language OPENQASM [51]. Hence, it opens the way for a modular easy integration in any standard programming environment, in particular QISKIT [153], which uses OPENQASM as assembly language.

### 5.4.2 Optimization Procedure

VOQC optimization process provides two functionalities, one is deterministic (optimization by propagation and cancellation) and the other one requires a replacing circuit input.

**Optimization by propagation and cancellation** is based on local circuit rewriting schemes and self composition properties of elementary gates, borrowed from [138] (eg., sequences of an even number of either *H*, *CNOT* or *X* gate annihilate as the identity, successive occurrences of $R_z$ gates melt by summing their angle parameters, *etc*). Hence, the procedure consists of two successive steps:

* propagate: for any elementary gate, it

- considers several identified patterns enabling gate commutations,

- finds all occurrences of these patterns,

- and performs the related commutation, pushing any occurrence of this elementary gate to the end of the computation,

* cancellation then consists in deleting the resulting repetitive occurrences of the elementary gate at stake.

**Optimization by circuit replacement** consists in substituting a part of a quantum circuit (a sub-circuit) by another one that is proven to be functionally equivalent. In this case, the equivalence proof is led by help of the path-sums semantics (see Section 5.2). Hence, in its most general form, the process requires an external equivalence proof oracle. Nevertheless, VOQC provides some instances of such proved equivalence patterns (eg, rotation merging), whose application is automatic.

**Performance and Achievements.** VOQC performance has been evaluated against several standard quantum computation routines, and compared with several existing optimizers [7, 153, 138, 178, 108]. Note that in VOQC, since optimization is performed as a succession of rewriting operations, the formal verification consists in assessing the equivalence between the input and the output of the optimization, it does not address the optimization performance. Still, on reported experiments, VOQC performance competes with other existing non-verified optimizers, both regarding computation time and circuit complexity reduction-precise performance comparison tables appear in [91]. Thus, in the current state of the art, the benefits of formally verified circuit optimization comes for free.
* in addition to optimization, VOQC also contains some circuit mapping functionalities. They perform further circuit transformation so that the output circuits fit to specific quantum architecture qubit connectivity constraints. This functionality is a preliminary address to the problem raised as first bullet in Section 2.3.3,

* VOQC environment also provides both ways compilations between SQIR and the standard assembly language OPENQASM [51]. Hence, it opens the way for a modular easy integration in any standard programming environment, in particular QISKIT [153], which uses OPENQASM as assembly language.

### 5.4.2 Optimization Procedure

VOQC optimization process provides two functionalities, one is deterministic (optimization by propagation and cancellation) and the other one requires a replacing circuit input.

**Optimization by propagation and cancellation** is based on local circuit rewriting schemes and self composition properties of elementary gates, borrowed from [138] (eg., sequences of an even number of either *H*, *CNOT* or *X* gate annihilate as the identity, successive occurrences of $R_z$ gates melt by summing their angle parameters, *etc*). Hence, the procedure consists of two successive steps:

* propagate: for any elementary gate, it

- considers several identified patterns enabling gate commutations,

- finds all occurrences of these patterns,

- and performs the related commutation, pushing any occurrence of this elementary gate to the end of the computation,

* cancellation then consists in deleting the resulting repetitive occurrences of the elementary gate at stake.

**Optimization by circuit replacement** consists in substituting a part of a quantum circuit (a sub-circuit) by another one that is proven to be functionally equivalent. In this case, the equivalence proof is led by help of the path-sums semantics (see Section 5.2). Hence, in its most general form, the process requires an external equivalence proof oracle. Nevertheless, VOQC provides some instances of such proved equivalence patterns (eg, rotation merging), whose application is automatic.

**Performance and Achievements.** VOQC performance has been evaluated against several standard quantum computation routines, and compared with several existing optimizers [7, 153, 138, 178, 108]. Note that in VOQC, since optimization is performed as a succession of rewriting operations, the formal verification consists in assessing the equivalence between the input and the output of the optimization, it does not address the optimization performance. Still, on reported experiments, VOQC performance competes with other existing non-verified optimizers, both regarding computation time and circuit complexity reduction—precise performance comparison tables appear in [91]. Thus, in the current state of the art, the benefits of formally verified circuit optimization comes for free.
## 5.5 Formally verified quantum compilation in an imperative setting: CertiQ

CertiQ [173] is another noticeable effort for verified compilation. Interestingly, it applies to QISKIT language, which is certainly the most widely used quantum compiler. CertiQ proceeds similarly as VOQC, by applying successive optimization passes, each consisting in applying local circuit equivalence transformations over quantum circuits. CertiQ has been evaluated against the very compilation environment provided by IBM QISKIT framework. And verified optimization went through 26 out of the 30 compilation passes the framework offered at writing time. Hence, the current limitations of formally verified compilation is mainly inherited from the state of the art in (non verified) quantum compilation.

The application to QISKIT also inevitably brings an additional drawback: while CertiQ can bring insurance that compilation respects the functional equivalence between an input and an output quantum circuits, the initial circuit building brick still lacks formal verification. Indeed, the environment is not provided formal means to assess that the input circuit meets a given functional specification. An open work direction then is to develop formal circuit building verification methods similar as SQIR or QBRICKS but applying to (mostly imperative) widely used development environments such as QISKIT, so as to complete the verified development chain.

# 6 Formal Quantum Programming Languages

For reasoning on a concrete *runs* of quantum algorithms solving a specific problem *instances*, the notion of quantum circuit is natural. Yet, a quantum circuit is only a by-product of a specific run of a quantum algorithm, holding only for a specific instantiation of the algorithm parameters.

Hence, a quantum algorithm is not reducible to a quantum circuit. To run quantum algorithms and reason about them, one needs *quantum programming languages (QPL)*: this is the topic of the current section.

## 6.1 Quantum Programming Languages Design

In Section 5, circuits were merely seen as sequences of elementary gates. However, in most quantum algorithms circuits follow a more complex structure: they are built compositionally from smaller sub-circuits and circuits combiners. Circuits are usually *static* objects, buffered until completion before being flushed to the quantum co-processor. Still, in some algorithms, they are *dynamically* generated: the tail of the circuit depends on the result of former measurements.

In this section, we discuss the high-level structure of quantum algorithms, the requirements for a quantum programming language, and review some of the existing proposals.

### 6.1.1 Structure of Quantum Algorithms

The usual model for quantum computation was depicted in Figure 1: a classical computer controls a quantum co-processor, whose role is to hold a quantum memory. A programmatic interface for interacting with the co-processor is provided to the programmer sitting in front of the classical computer. The interface gives methods to send instructions to the quantum memory to allocate and initialize new quantum registers, apply unitary gates on qubits, and eventually perform measurements. Even though the set of instructions is commonly represented as a circuit, it is merely the result of a *trace of classical execution* of a classical program on the classical computer.

Figure 8 presents two standard workflows with a quantum co-processor. In Figure 8a, the classical execution inputs some (classical) parameters, performs some pre-processing, generates a circuit,