Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Formal Methods in Quantum Circuit Design

Matthew Amy

Published Feb 26, 2019• 13 citations
OpenAlex

Abstract

The design and compilation of correct, efficient quantum circuits is integral to the future operation of quantum computers. This thesis makes contributions to the problems of optimizing and verifying quantum circuits, with an emphasis on the development of formal models for such purposes. We also present software implementations of these methods, which together form a full stack of tools for the design of optimized, formally verified quantum oracles. \n \nOn the optimization side, we study methods for the optimization of Rz and CNOT gates in Clifford+Rz circuits. We develop a general, efficient optimization algorithm called phase folding, which reduces the number of Rz gates without increasing any metrics by computing its phase polynomial. This algorithm can further be combined with synthesis techniques for CNOT-dihedral operators to optimize circuits with respect to particular costs. We then study the optimal synthesis problem for CNOT-dihedral operators from the perspectives of Rz and CNOT gate optimization. In the case of Rz gate optimization, we show that the optimal synthesis problem is polynomial-time equivalent to minimum-distance decoding in certain Reed-Muller codes. For the CNOT optimization problem, we show that the optimal synthesis problem is at least as hard as a combinatorial problem related to Gray codes. In both cases, we develop heuristics for the optimal synthesis problem, which together with phase folding reduces T counts by 42% and CNOT counts by 22% across a suite of real-world benchmarks. \n \nFrom the perspective of formal verification, we make two contributions. The first is the development of a formal model of quantum circuits with ancillary bits based on the Feynman path integral, along with a concrete verification algorithm. The path integral model, with some syntactic sugar, further doubles as a natural specification language for quantum computations. Our experiments show some practical circuits with up to hundreds of qubits can be efficiently verified. Our second contribution is a formally verified, optimizing compiler for reversible circuits. The compiler compiles a classical, irreversible language to reversible circuits, with a formal, machine-checked proof of correctness written in the proof assistant F*. The compiler is structured as a partial evaluator, allowing verification to be carried out significantly faster than previous results.

Related papers

Program compilation for large-scale quantum computers

Giulia Meuli

Practical realizations of quantum computers are poised to deliver outstanding computational capabilities far beyond the reach of any classical supercomputer. While classical systems are reliably implemented using CMOS technology, the fabrication of quantum hardware has not yet reached a commercially viable level of maturity. Nowadays, many different technologies are being developed as competing candidates to build the first error-corrected quantum computer. Among the software resources required to operate such a system, quantum compilers translate a high-level description of a quantum algorithm into low-level, technology-dependent quantum instructions. Many quantum algorithms, including Shor's and Grover's algorithms, require to compute some classical logic functions on the quantum computer. The first part of this thesis deals with the problem of compiling quantum circuits that perform such classical Boolean functions, called oracles, into a fault-tolerant set of instructions. Oracle circuits often demand many resources in terms of the number of qubits and gates. The focus is on compiling quantum circuits starting from multi-level logic networks representing large Boolean functions while minimizing the resource footprint of the obtained quantum circuits. At the same time, the trade-off between memory resources and the number of operations typical of such a compilation process is explored. As part of the effort in reducing the resources required to perform a given quantum program, I also present some quantum circuit optimization techniques. The researched algorithms leverage data structures and techniques borrowed and adapted from classical logic synthesis, e.g., SAT solvers, LUT mapping, and multi-level logic networks. I implemented all the compilation algorithms presented in this thesis as part of open-source projects. In particular, I develop and maintain caterpillar---a C++ header-only library dedicated to the quantum compilation of oracles and quantum memory management. The second part of this thesis describes how to equip quantum programming language compilers with automatic accuracy management. Despite the availability of many of such languages, resource estimation of quantum algorithms does not yet support taking approximation errors into account. This general methodology is applicable to any programming language and I demonstrate its integration into the Q# compiler. The technique consists of providing language support to ease the accuracy-aware programming task. The user can define accuracy parameters that will be automatically optimized according to a constraint and a cost function directly generated from the source code. In the presented practical evaluations, the constraint function is the overall allowed accuracy, while the cost function is application-dependent and related to the number of gates. During the optimization process, such functions are evaluated hundreds of times. For this reason, we extract them as (near-)symbolic expressions, whose evaluation time does not depend on the quantum algorithm size. The algorithms and the methodologies presented in this thesis are part of a widespread effort of the research community to build a complete and efficient software stack to program and control the first practical universal quantum computer.

•Jan 1, 2020•1 citation

Heuristic and Optimal Synthesis of CNOT and Clifford Circuits

Mark Webster, Stergios Koutsioumpas, Dan E. Browne

Efficiently implementing Clifford circuits is crucial for quantum error correction and quantum algorithms. Linear reversible circuits, equivalent to circuits composed of CNOT\xspace gates, have important applications in classical computing. In this work we present methods for CNOT\xspace and general Clifford circuit synthesis which can be used to minimise either the entangling two-qubit gate count or the circuit depth. We present three families of algorithms - optimal synthesis which works on small circuits, A* synthesis for intermediate-size circuits and greedy synthesis for large circuits. We benchmark against existing methods, including rustiq, tket and qiskit and show that our approach results in circuits with lower two-qubit gate count. For encoding circuits, our methods outperform previous reinforcement learning results and find a lower two-qubit gate count circuit for the Golay code than previously known. The algorithms have been implemented in a GitHub repository for use by the classical and quantum computing community.

arXiv:2503.14660•Quantum•Sep 21, 2026•0 citations

Formal Verification of Quantum Circuit Optimization Algorithms

Jincheng Zhang

Quantum circuit optimization is crucial for realizing the full potential of quantum computing. However, the inherent complexity of quantum circuits and the potential for errors introduce significant challenges in ensuring the correctness and efficiency of optimization algorithms. This paper proposes a novel approach to formally verify quantum circuit optimization algorithms. We translate these algorithms into formal specification languages and leverage model checking and theorem proving techniques to rigorously demonstrate that the algorithms meet their intended objectives – primarily minimizing circuit complexity – without introducing unintended side effects. The core contribution lies in applying formal verification methodologies to this largely unexplored area, offering a path towards building trust and confidence in quantum optimization strategies. The presented framework provides a systematic method for ensuring the reliability of quantum circuits, a critical step towards practical quantum computation. The verification process relies on defining the desired behavior as a set of logical properties and then employing automated tools to check whether the optimized circuit satisfies these properties. This approach addresses the fundamental need for rigorous assurance in quantum systems, moving beyond empirical validation and towards mathematically proven correctness.

•Sep 5, 2026•0 citations

(A Variant of) Clifford Circuit Synthesis is NP-Complete

Luna Lima Keller, Richard Kueng

Optimal circuit synthesis is the problem of finding the shortest-depth circuit representation of a given functionality with respect to a pre-specified elementary gate set. This is a central problem in both quantum and classical hardware design. While the classical version is very well understood -- both in terms of heuristics and rigorous hardness assertions -- much less is known about optimal quantum circuit synthesis. We focus on optimal Clifford circuit synthesis, for which various heuristics are known, e.g. via reduction to 3-SAT. Our main result supplies a matching hardness result: a variant of optimal Clifford synthesis is NP-hard. The proof proceeds in two parts: (i) reduce 3-edge colorability on 3-regular graphs to a circuit synthesis problem that only involves CZ gates, (ii) prove that the availability of additional elementary Clifford gates -- most notably: Hadamard, phase and CNOT -- cannot lead to further improvements of the optimal circuit depth. Our work sharpens the complexity-theoretic understanding of Clifford circuits: simulation and equivalence checking are in P, whereas deciding whether a Clifford unitary admits an implementation within a prescribed depth is NP-complete.

quant-pharXiv:2610.02029•Oct 2, 2026•0 citations

Formally Verified Quantum Programming

Robert W. Rand

The field of quantum mechanics predates computer science by at least ten years, the time between the publication of the Schrodinger equation and the Church-Turing thesis. It took another fifty years for Feynman to recognize that harnessing quantum mechanics is necessary to efficiently simulate physics and for David Deutsch to propose the quantum Turing machine. After thirty more years, we are finally getting close to the first general-purpose quantum computers based upon prototypes by IBM, Intel, Google and others.\nWhile physicists and engineers have worked on building scalable quantum computers, theoretical computer scientists have made their own advances. Complexity theorists introduced quantum complexity classes like BQP and QMA; Shor and Grover developed their famous algorithms for factoring and unstructured search. Programming languages researchers pursued two main research directions: Small-scale languages like QPL and the quantum lambda-calculi for reasoning about quantum computation and large-scale languages like Quipper and Q# for industrial-scale quantum software development. This thesis aims to unify these two threads while adding a third one: formal verification.\nWe argue that quantum programs demand machine-checkable proofs of correctness. We justify this on the basis of the complexity of programs manipulating quantum states, the expense of running quantum programs, and the inapplicability of traditional debugging techniques to programs whose states cannot be examined. We further argue that the existing mathematical models of quantum computation make this an easier task than one could reasonably expect. In light of these observations we introduce QWIRE, a tool for writing verifiable, large scale quantum programs.\nQWIRE is not merely a language for writing and verifying quantum circuits: it is a verified circuit description language. This means that the semantics of QWIRE circuits are verified in the Coq proof assistant. We also implement verified abstractions, like ancilla management and reversible circuit compilation. Finally, we turn QWIRE and Coq's abilities outwards, towards verifying popular quantum algorithms like quantum teleportation. We argue that this tool provides a solid foundation for research into quantum programming languages and formal verification going forward.

•Jan 1, 2018•7 citations

Towards Large-scale Functional Verification of Universal Quantum Circuits

Matthew Amy

We introduce a framework for the formal specification and verification of quantum circuits based on the Feynman path integral. Our formalism, built around exponential sums of polynomial functions, provides a structured and natural way of specifying quantum operations, particularly for quantum implementations of classical functions. Verification of circuits over all levels of the Clifford hierarchy with respect to either a specification or reference circuit is enabled by a novel rewrite system for exponential sums with free variables. Our algorithm is further shown to give a polynomial-time decision procedure for checking the equivalence of Clifford group circuits. We evaluate our methods by performing automated verification of optimized Clifford+T circuits with up to 100 qubits and thousands of T gates, as well as the functional verification of quantum algorithms using hundreds of qubits. Our experiments culminate in the automated verification of the Hidden Shift algorithm for a class of Boolean functions in a fraction of the time it has taken recent algorithms to simulate.

arXiv:1805.06908•Electronic Proceedings in Theoretical Computer Science•Jan 31, 2019•119 citations
The design and compilation of correct, efficient quantum circuits is integral to the future operation of quantum computers. This thesis makes contributions to the problems of optimizing and verifying quantum circuits, with an emphasis on the development of formal models for such purposes. We also present software implementations of these methods, which together form a full stack of tools for the design of optimized, formally verified quantum oracles. \n \nOn the optimization side, we study methods for the optimization of Rz and CNOT gates in Clifford+Rz circuits. We develop a general, efficient optimization algorithm called phase folding, which reduces the number of Rz gates without increasing any metrics by computing its phase polynomial. This algorithm can further be combined with synthesis techniques for CNOT-dihedral operators to optimize circuits with respect to particular costs. We then study the optimal synthesis problem for CNOT-dihedral operators from the perspectives of Rz and CNOT gate optimization. In the case of Rz gate optimization, we show that the optimal synthesis problem is polynomial-time equivalent to minimum-distance decoding in certain Reed-Muller codes. For the CNOT optimization problem, we show that the optimal synthesis problem is at least as hard as a combinatorial problem related to Gray codes. In both cases, we develop heuristics for the optimal synthesis problem, which together with phase folding reduces T counts by 42% and CNOT counts by 22% across a suite of real-world benchmarks. \n \nFrom the perspective of formal verification, we make two contributions. The first is the development of a formal model of quantum circuits with ancillary bits based on the Feynman path integral, along with a concrete verification algorithm. The path integral model, with some syntactic sugar, further doubles as a natural specification language for quantum computations. Our experiments show some practical circuits with up to hundreds of qubits can be efficiently verified. Our second contribution is a formally verified, optimizing compiler for reversible circuits. The compiler compiles a classical, irreversible language to reversible circuits, with a formal, machine-checked proof of correctness written in the proof assistant F*. The compiler is structured as a partial evaluator, allowing verification to be carried out significantly faster than previous results.
Practical realizations of quantum computers are poised to deliver outstanding computational capabilities far beyond the reach of any classical supercomputer. While classical systems are reliably implemented using CMOS technology, the fabrication of quantum hardware has not yet reached a commercially viable level of maturity. Nowadays, many different technologies are being developed as competing candidates to build the first error-corrected quantum computer. Among the software resources required to operate such a system, quantum compilers translate a high-level description of a quantum algorithm into low-level, technology-dependent quantum instructions. Many quantum algorithms, including Shor's and Grover's algorithms, require to compute some classical logic functions on the quantum computer. The first part of this thesis deals with the problem of compiling quantum circuits that perform such classical Boolean functions, called oracles, into a fault-tolerant set of instructions. Oracle circuits often demand many resources in terms of the number of qubits and gates. The focus is on compiling quantum circuits starting from multi-level logic networks representing large Boolean functions while minimizing the resource footprint of the obtained quantum circuits. At the same time, the trade-off between memory resources and the number of operations typical of such a compilation process is explored. As part of the effort in reducing the resources required to perform a given quantum program, I also present some quantum circuit optimization techniques. The researched algorithms leverage data structures and techniques borrowed and adapted from classical logic synthesis, e.g., SAT solvers, LUT mapping, and multi-level logic networks. I implemented all the compilation algorithms presented in this thesis as part of open-source projects. In particular, I develop and maintain caterpillar---a C++ header-only library dedicated to the quantum compilation of oracles and quantum memory management. The second part of this thesis describes how to equip quantum programming language compilers with automatic accuracy management. Despite the availability of many of such languages, resource estimation of quantum algorithms does not yet support taking approximation errors into account. This general methodology is applicable to any programming language and I demonstrate its integration into the Q# compiler. The technique consists of providing language support to ease the accuracy-aware programming task. The user can define accuracy parameters that will be automatically optimized according to a constraint and a cost function directly generated from the source code. In the presented practical evaluations, the constraint function is the overall allowed accuracy, while the cost function is application-dependent and related to the number of gates. During the optimization process, such functions are evaluated hundreds of times. For this reason, we extract them as (near-)symbolic expressions, whose evaluation time does not depend on the quantum algorithm size. The algorithms and the methodologies presented in this thesis are part of a widespread effort of the research community to build a complete and efficient software stack to program and control the first practical universal quantum computer.
Efficiently implementing Clifford circuits is crucial for quantum error correction and quantum algorithms. Linear reversible circuits, equivalent to circuits composed of CNOT\xspace gates, have important applications in classical computing. In this work we present methods for CNOT\xspace and general Clifford circuit synthesis which can be used to minimise either the entangling two-qubit gate count or the circuit depth. We present three families of algorithms - optimal synthesis which works on small circuits, A* synthesis for intermediate-size circuits and greedy synthesis for large circuits. We benchmark against existing methods, including rustiq, tket and qiskit and show that our approach results in circuits with lower two-qubit gate count. For encoding circuits, our methods outperform previous reinforcement learning results and find a lower two-qubit gate count circuit for the Golay code than previously known. The algorithms have been implemented in a GitHub repository for use by the classical and quantum computing community.
Quantum circuit optimization is crucial for realizing the full potential of quantum computing. However, the inherent complexity of quantum circuits and the potential for errors introduce significant challenges in ensuring the correctness and efficiency of optimization algorithms. This paper proposes a novel approach to formally verify quantum circuit optimization algorithms. We translate these algorithms into formal specification languages and leverage model checking and theorem proving techniques to rigorously demonstrate that the algorithms meet their intended objectives – primarily minimizing circuit complexity – without introducing unintended side effects. The core contribution lies in applying formal verification methodologies to this largely unexplored area, offering a path towards building trust and confidence in quantum optimization strategies. The presented framework provides a systematic method for ensuring the reliability of quantum circuits, a critical step towards practical quantum computation. The verification process relies on defining the desired behavior as a set of logical properties and then employing automated tools to check whether the optimized circuit satisfies these properties. This approach addresses the fundamental need for rigorous assurance in quantum systems, moving beyond empirical validation and towards mathematically proven correctness.
Optimal circuit synthesis is the problem of finding the shortest-depth circuit representation of a given functionality with respect to a pre-specified elementary gate set. This is a central problem in both quantum and classical hardware design. While the classical version is very well understood -- both in terms of heuristics and rigorous hardness assertions -- much less is known about optimal quantum circuit synthesis. We focus on optimal Clifford circuit synthesis, for which various heuristics are known, e.g. via reduction to 3-SAT. Our main result supplies a matching hardness result: a variant of optimal Clifford synthesis is NP-hard. The proof proceeds in two parts: (i) reduce 3-edge colorability on 3-regular graphs to a circuit synthesis problem that only involves CZ gates, (ii) prove that the availability of additional elementary Clifford gates -- most notably: Hadamard, phase and CNOT -- cannot lead to further improvements of the optimal circuit depth. Our work sharpens the complexity-theoretic understanding of Clifford circuits: simulation and equivalence checking are in P, whereas deciding whether a Clifford unitary admits an implementation within a prescribed depth is NP-complete.
The field of quantum mechanics predates computer science by at least ten years, the time between the publication of the Schrodinger equation and the Church-Turing thesis. It took another fifty years for Feynman to recognize that harnessing quantum mechanics is necessary to efficiently simulate physics and for David Deutsch to propose the quantum Turing machine. After thirty more years, we are finally getting close to the first general-purpose quantum computers based upon prototypes by IBM, Intel, Google and others.\nWhile physicists and engineers have worked on building scalable quantum computers, theoretical computer scientists have made their own advances. Complexity theorists introduced quantum complexity classes like BQP and QMA; Shor and Grover developed their famous algorithms for factoring and unstructured search. Programming languages researchers pursued two main research directions: Small-scale languages like QPL and the quantum lambda-calculi for reasoning about quantum computation and large-scale languages like Quipper and Q# for industrial-scale quantum software development. This thesis aims to unify these two threads while adding a third one: formal verification.\nWe argue that quantum programs demand machine-checkable proofs of correctness. We justify this on the basis of the complexity of programs manipulating quantum states, the expense of running quantum programs, and the inapplicability of traditional debugging techniques to programs whose states cannot be examined. We further argue that the existing mathematical models of quantum computation make this an easier task than one could reasonably expect. In light of these observations we introduce QWIRE, a tool for writing verifiable, large scale quantum programs.\nQWIRE is not merely a language for writing and verifying quantum circuits: it is a verified circuit description language. This means that the semantics of QWIRE circuits are verified in the Coq proof assistant. We also implement verified abstractions, like ancilla management and reversible circuit compilation. Finally, we turn QWIRE and Coq's abilities outwards, towards verifying popular quantum algorithms like quantum teleportation. We argue that this tool provides a solid foundation for research into quantum programming languages and formal verification going forward.
We introduce a framework for the formal specification and verification of quantum circuits based on the Feynman path integral. Our formalism, built around exponential sums of polynomial functions, provides a structured and natural way of specifying quantum operations, particularly for quantum implementations of classical functions. Verification of circuits over all levels of the Clifford hierarchy with respect to either a specification or reference circuit is enabled by a novel rewrite system for exponential sums with free variables. Our algorithm is further shown to give a polynomial-time decision procedure for checking the equivalence of Clifford group circuits. We evaluate our methods by performing automated verification of optimized Clifford+T circuits with up to 100 qubits and thousands of T gates, as well as the functional verification of quantum algorithms using hundreds of qubits. Our experiments culminate in the automated verification of the Hidden Shift algorithm for a class of Boolean functions in a fraction of the time it has taken recent algorithms to simulate.