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

arXiv:2404.05934 · Proceedings of the ACM on Programming Languages

Verification of Recursively Defined Quantum Circuits

Mingsheng Ying, Zhicheng Zhang

Published Jun 8, 2026• 0 citations
arXivHTMLPDF

Abstract

Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and compactly programmed. In this paper, we present a proof system for formal verification of the correctness of recursively defined quantum circuits. The soundness and (relative) completeness of the proof system are established. To demonstrate its effectiveness, we present a series of application examples, including formal verification of multi-qubit controlled gates, a quantum circuit for generating multi-qubit GHZ (Greenberger-Horne-Zeilinger) states, and more sophisticated quantum algorithms with recursive structures such as the quantum Fourier transform, quantum state preparation, and quantum random access memories (QRAMs).

DOI
10.1145/3808273

Related papers

Self-Referential Formal Verification of Quantum Circuits

Jincheng Zhang

Formal verification of quantum circuits is a crucial step towards building reliable quantum computers. However, the exponential scaling of quantum states makes traditional formal verification methods impractical for anything beyond small circuits. This paper proposes a novel approach leveraging self-referential quantum circuits for verification. The core idea is to create a verification circuit that recursively simulates and verifies the behavior of the original circuit. This self-referential process allows for a more efficient exploration of the state space, mitigating the exponential growth problem. We define the key components of this system, including the self-referential circuit architecture and the underlying mathematical framework. The paper outlines the potential for this approach to overcome limitations of existing techniques and represents a significant advancement in the field of quantum verification. The primary mathematical challenge addressed is the efficient simulation of quantum circuits within a self-referential structure.

•Sep 2, 2026•0 citations

Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs

Zhicheng Zhang, Mingsheng Ying

Quantum recursive programming has been recently introduced for describing sophisticated and complicated quantum algorithms in a compact and elegant way. However, implementation of quantum recursion involves intricate interplay between quantum control flow and recursive procedure calls. In this paper, we aim at resolving this fundamental challenge and develop a series of techniques to efficiently implement quantum recursive programs. Our main contributions include:

arXiv:2408.10054•Proceedings of the ACM on Programming Languages•Jun 10, 2025•4 citations

Formal Verification of Quantum Circuits Performance Analysis Across Algorithmic and Protocol-Based Implementations

Hasnain Muhammad

ABSTRACT- This paper presents an integrated framework for the automated verification and visualization of quantum circuits, addressing the critical need for reliable quantum software development tools. We implement and analyze eight fundamental quantum circuits Bell states, GHZ states, Quantum Fourier Transform (QFT), Grover's search algorithm, the Variational Quantum Eigensolver (VQE) for H₂ molecules, Quantum Teleportation, Superdense Coding, and the Bernstein-Vazirani algorithm through a comprehensive verification pipeline. The system generates publication-ready circuit diagrams and performs formal verification via automated theorem proving, achieving an overall verification success rate of 93.7% across all circuits. Notably, basic circuits such as Bell and GHZ states achieve perfect verification (100% success), whereas the Quantum Teleportation circuit presents the greatest challenge, attaining only 88.9% success. Results demonstrate a strong linear correlation (R² = 0.89) between circuit complexity (gate count) and verification time, with the framework processing 348 verification conditions per second. This work establishes quantitative benchmarks for quantum software verification, highlights specific gaps in protocol-level verification, and provides an integrated toolset that bridges the gap between circuit visualization and formal correctness assurance, thereby advancing the state of quantum software engineering.

•Jan 7, 2026•0 citations

Structural Verification of Quantum Circuits: A Haskell Implementation via Hoare Logic

Alex Bastianini

As quantum hardware remains limited by qubit count and noise, the efficiency and correctness of quantum programs cannot yet be efficiently checked by execution or classical simulation alone. This thesis develops a Hoare logic for reasoning about the structural properties of quantum circuits produced by Proto-Qiskit, a Qiskit inspired programming language. We define derivation rules that treat commands that modify circuits as assignments, allowing properties such as gate count, circuit width, and depth to be specified and verified. These results are implemented in a Haskell tool that parses annotated Proto-Qiskit programs and proves their validity by generating verification conditions using weakest precondition calculus, with the support of an SMT solver. The tool is demonstrated on parametric example programs, including a quantum Fourier transform circuit, highlighting both its capabilities and its current limitations. Furthermore, we informally discuss the implementation of an optimization-aware extension of the logic based on a quantum state assertion language. This allows triviality conditions to be checked during verification so that redundant gates can be identified and removed while proving the correctness of the resulting optimized circuit. We discuss the issues this extension introduces for automated verification.

•Jul 15, 2026•0 citations

Rotational abstractions for verification of quantum Fourier transform circuits

Arun Govindankutty, Sudarshan K. Srinivasan, Nimish Mathure

Abstract With the race to build large‐scale quantum computers and efforts to exploit quantum algorithms for efficient problem solving in science and engineering disciplines, the requirement to have efficient and scalable verification methods are of vital importance. A novel formal verification method that is targeted at Quantum Fourier Transform (QFT) circuits is proposed. Quantum Fourier Transform is a fundamental quantum algorithm that forms the basis of many quantum computing applications. The verification method employs abstractions of quantum gates used in QFT that leads to a reduction of the verification problem from Hilbert space to the quantifier free logic of bit‐vectors. Very efficient decision procedures are available to reason about bit‐vectors. Therefore, this method is able to scale up to the verification of QFT circuits with 10,000 qubits and 50 million quantum gates, providing a meteoric advance in the size of QFT circuits thus far verified using formal verification methods.

arXiv:2301.00737•IET Quantum Communication•Mar 13, 2023•15 citations

Reasoning about Recursive Quantum Programs

Zhaowei Xu, Mingsheng Ying, Benoît Valiron

Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursion will become one of the fundamental paradigms of quantum programming. Several program logics have been developed for verification of quantum while-programs. However, there are as yet no general methods for reasoning about (mutual) recursive procedures and ancilla quantum data structure in quantum computing (with measurement). We fill the gap in this paper by proposing a parameterized quantum assertion logic and, based on which, designing a quantum Hoare logic for verifying parameterized recursive quantum programs with ancilla data and probabilistic control. The quantum Hoare logic can be used to prove partial, total, and even probabilistic correctness (by reducing to total correctness) of those quantum programs. In particular, two counterexamples for illustrating incompleteness of non-parameterized assertions in verifying recursive procedures, and, one counterexample for showing the failure of reasoning with exact probabilities based on partial correctness, are constructed. The effectiveness of our logic is shown by three main examples -- recursive quantum Markov chain (with probabilistic control), fixed-point Grover's search, and recursive quantum Fourier sampling.

arXiv:2107.11679•Jul 24, 2021•1 citation
Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and compactly programmed. In this paper, we present a proof system for formal verification of the correctness of recursively defined quantum circuits. The soundness and (relative) completeness of the proof system are established. To demonstrate its effectiveness, we present a series of application examples, including formal verification of multi-qubit controlled gates, a quantum circuit for generating multi-qubit GHZ (Greenberger-Horne-Zeilinger) states, and more sophisticated quantum algorithms with recursive structures such as the quantum Fourier transform, quantum state preparation, and quantum random access memories (QRAMs).
Formal verification of quantum circuits is a crucial step towards building reliable quantum computers. However, the exponential scaling of quantum states makes traditional formal verification methods impractical for anything beyond small circuits. This paper proposes a novel approach leveraging self-referential quantum circuits for verification. The core idea is to create a verification circuit that recursively simulates and verifies the behavior of the original circuit. This self-referential process allows for a more efficient exploration of the state space, mitigating the exponential growth problem. We define the key components of this system, including the self-referential circuit architecture and the underlying mathematical framework. The paper outlines the potential for this approach to overcome limitations of existing techniques and represents a significant advancement in the field of quantum verification. The primary mathematical challenge addressed is the efficient simulation of quantum circuits within a self-referential structure.
ABSTRACT- This paper presents an integrated framework for the automated verification and visualization of quantum circuits, addressing the critical need for reliable quantum software development tools. We implement and analyze eight fundamental quantum circuits Bell states, GHZ states, Quantum Fourier Transform (QFT), Grover's search algorithm, the Variational Quantum Eigensolver (VQE) for H₂ molecules, Quantum Teleportation, Superdense Coding, and the Bernstein-Vazirani algorithm through a comprehensive verification pipeline. The system generates publication-ready circuit diagrams and performs formal verification via automated theorem proving, achieving an overall verification success rate of 93.7% across all circuits. Notably, basic circuits such as Bell and GHZ states achieve perfect verification (100% success), whereas the Quantum Teleportation circuit presents the greatest challenge, attaining only 88.9% success. Results demonstrate a strong linear correlation (R² = 0.89) between circuit complexity (gate count) and verification time, with the framework processing 348 verification conditions per second. This work establishes quantitative benchmarks for quantum software verification, highlights specific gaps in protocol-level verification, and provides an integrated toolset that bridges the gap between circuit visualization and formal correctness assurance, thereby advancing the state of quantum software engineering.
As quantum hardware remains limited by qubit count and noise, the efficiency and correctness of quantum programs cannot yet be efficiently checked by execution or classical simulation alone. This thesis develops a Hoare logic for reasoning about the structural properties of quantum circuits produced by Proto-Qiskit, a Qiskit inspired programming language. We define derivation rules that treat commands that modify circuits as assignments, allowing properties such as gate count, circuit width, and depth to be specified and verified. These results are implemented in a Haskell tool that parses annotated Proto-Qiskit programs and proves their validity by generating verification conditions using weakest precondition calculus, with the support of an SMT solver. The tool is demonstrated on parametric example programs, including a quantum Fourier transform circuit, highlighting both its capabilities and its current limitations. Furthermore, we informally discuss the implementation of an optimization-aware extension of the logic based on a quantum state assertion language. This allows triviality conditions to be checked during verification so that redundant gates can be identified and removed while proving the correctness of the resulting optimized circuit. We discuss the issues this extension introduces for automated verification.
Abstract With the race to build large‐scale quantum computers and efforts to exploit quantum algorithms for efficient problem solving in science and engineering disciplines, the requirement to have efficient and scalable verification methods are of vital importance. A novel formal verification method that is targeted at Quantum Fourier Transform (QFT) circuits is proposed. Quantum Fourier Transform is a fundamental quantum algorithm that forms the basis of many quantum computing applications. The verification method employs abstractions of quantum gates used in QFT that leads to a reduction of the verification problem from Hilbert space to the quantifier free logic of bit‐vectors. Very efficient decision procedures are available to reason about bit‐vectors. Therefore, this method is able to scale up to the verification of QFT circuits with 10,000 qubits and 50 million quantum gates, providing a meteoric advance in the size of QFT circuits thus far verified using formal verification methods.
Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursion will become one of the fundamental paradigms of quantum programming. Several program logics have been developed for verification of quantum while-programs. However, there are as yet no general methods for reasoning about (mutual) recursive procedures and ancilla quantum data structure in quantum computing (with measurement). We fill the gap in this paper by proposing a parameterized quantum assertion logic and, based on which, designing a quantum Hoare logic for verifying parameterized recursive quantum programs with ancilla data and probabilistic control. The quantum Hoare logic can be used to prove partial, total, and even probabilistic correctness (by reducing to total correctness) of those quantum programs. In particular, two counterexamples for illustrating incompleteness of non-parameterized assertions in verifying recursive procedures, and, one counterexample for showing the failure of reasoning with exact probabilities based on partial correctness, are constructed. The effectiveness of our logic is shown by three main examples -- recursive quantum Markov chain (with probabilistic control), fixed-point Grover's search, and recursive quantum Fourier sampling.