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

IEEE Dallas Circuits and Systems Conference (DCAS)

Formally Verifying Quantum Phase Estimation Circuits With 1,000+ Qubits

Arun Govindankutty, Sudarshan K. Srinivasan

Published Apr 10, 2026• 2 citations
Publisher

Abstract

We present a scalable formal verification methodology for Quantum Phase Estimation (QPE) circuits. Our approach uses a symbolic qubit abstraction based on quantifier-free bitvector logic, capturing key quantum phenomena, including superposition, rotation, and measurement. The proposed methodology maps quantum circuit functional behaviour from Hilbert space to a bit-vector domain. We develop formal properties aligned with this abstraction to ensure functional correctness of QPE circuits. The method scales efficiently, verifying QPE circuits with up to 6 precision qubits and 1,024 phase qubits using under 7.5 GB of memory.

DOI
10.1109/dcas69364.2026.11544241

Related papers

Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits

Arun Govindankutty, Sudarshan K. Srinivasan

We present a scalable formal verification methodology for Quantum Phase Estimation (QPE) circuits. Our approach uses a symbolic qubit abstraction based on quantifier-free bit-vector logic, capturing key quantum phenomena, including superposition, rotation, and measurement. The proposed methodology maps quantum circuit functional behaviour from Hilbert space to a bit-vector domain. We develop formal properties aligned with this abstraction to ensure functional correctness of QPE circuits. The method scales efficiently, verifying QPE circuits with up to 6 precision qubits and 1,024 phase qubits using under 7.5~GB of memory.

quant-pharXiv:2603.08762•Mar 10, 2026•1 citation

Bit-Vector Abstractions to Formally Verify Quantum Error Detection & Entanglement

Arun Govindankutty

As the number of qubits increases, quantum circuits become more complex and their state space grows rapidly. This makes functional verification challenging for conventional techniques. Ensuring correctness is especially critical for quantum error correction and entanglement generation. This paper presents a novel application of bit-vector based abstraction methodology for formal verification of quantum circuits where superposition and functional behaviour can be decoupled. The approach is applied to error detection circuits for 2-qubit, 3-qubit, and Shor 9-qubit quantum codes, as well as Bell-state and GHZ-state generation circuits. The error detection circuits and the Bell-state generation circuit are verified in less than a second and 25MB memory. GHZ circuits with up to 8,192 qubits are verified in under three minutes using a maximum of 23.2 GB of memory. The results demonstrate the versatility, scalability, and effectiveness of the proposed approach.

quant-pharXiv:2603.13554•IEEE Dallas Circuits and Systems Conference (DCAS)•Mar 17, 2026•1 citation

Superposition‐Based Abstractions for Quantum Data Encoding Verification

Arun Govindankutty, Sudarshan K. Srinivasan

ABSTRACT Many quantum algorithms operate on classical data, by first encoding classical data into the quantum domain using quantum data encoding circuits. To be effective for large data sets, encoding circuits that operate on large data sets are required. However, as the size of the data sets increases, the encoding circuits quickly become large, complex and error prone. Errors in the encoding circuit will provide incorrect inputs to quantum algorithms, making them ineffective. To address this problem, a formal method is proposed for verification of encoding circuits. The key idea to address scalability is the use of abstractions that reduce the verification problem to bit‐vector space. The major outcome of this work is that using this approach, the authors have been able to verify encoding circuits with up to 8191 qubits with very low memory (85 MB) and time (0.29s), demonstrating that the proposed approach can easily be employed to verify even much larger encoding circuits. The results are very significant because, traditional verification approaches that rely on modelling quantum circuits in Hilbert space have only demonstrated verification scalability up to 250 qubits. Also, this is the first approach to tackle the verification of quantum encoding circuits.

IET Quantum Communication•Jan 1, 2025•14 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

Formal Verification For Cyclic Quantum Walk Circuits

Benedicto James Sitou Campbell, Sudarshan K. Srinivasan

To fully utilize the advances in quantum computing, it is critical to develop verification techniques that can scale and ensure the design of reliable and error-free quantum circuits. In this work, we propose a formal verification approach for a popular subset of quantum walk circuits, which are those that traverse cycles. Quantum walks are the quantum mechanical analog of random walks and as such have many safety- critical and security-critical applications. The proposed approach incorporates abstractions for quantum gates used in quantum walk circuits and correctness properties. Experimental results demonstrated that the verification approach is very efficient and is able to scale up to quantum walk circuits with as many as 5,000 qubits.

IEEE International Symposium on Circuits and Systems proceedings•May 19, 2024•3 citations

A Review of Formal Methods in Quantum Circuit Verification

Arun Govindankutty

Quantum computing exploits the principles of quantum mechanics to perform computation. Information is stored in qubits and processed with a sequence of quantum gates arranged as circuits. Verifying the correctness of quantum circuits is becoming essential as hardware scales in qubit count and architectural complexity. Traditional testing and naive simulation do not scale and quickly become computationally infeasible because the state space grows exponentially. This creates a strong need for more powerful and scalable verification techniques. Formal methods offer a viable solution by providing mathematically rigorous and scalable verification techniques that address these scalability challenges through abstraction, symbolic reasoning, and probabilistic guarantees. This study examines how formal methods are applied to quantum circuit verification. Specifically, four families of formal techniques: barrier certificates, abstract interpretation, model checking, and theorem proving are examined, along with the theoretical foundations and practical applications of these techniques. Finally, the study highlights open challenges and identifies promising directions for future research. An extensive set of references is included to support further study and exploration.

Qeios•Feb 11, 2026•0 citations
We present a scalable formal verification methodology for Quantum Phase Estimation (QPE) circuits. Our approach uses a symbolic qubit abstraction based on quantifier-free bitvector logic, capturing key quantum phenomena, including superposition, rotation, and measurement. The proposed methodology maps quantum circuit functional behaviour from Hilbert space to a bit-vector domain. We develop formal properties aligned with this abstraction to ensure functional correctness of QPE circuits. The method scales efficiently, verifying QPE circuits with up to 6 precision qubits and 1,024 phase qubits using under 7.5 GB of memory.
We present a scalable formal verification methodology for Quantum Phase Estimation (QPE) circuits. Our approach uses a symbolic qubit abstraction based on quantifier-free bit-vector logic, capturing key quantum phenomena, including superposition, rotation, and measurement. The proposed methodology maps quantum circuit functional behaviour from Hilbert space to a bit-vector domain. We develop formal properties aligned with this abstraction to ensure functional correctness of QPE circuits. The method scales efficiently, verifying QPE circuits with up to 6 precision qubits and 1,024 phase qubits using under 7.5~GB of memory.
As the number of qubits increases, quantum circuits become more complex and their state space grows rapidly. This makes functional verification challenging for conventional techniques. Ensuring correctness is especially critical for quantum error correction and entanglement generation. This paper presents a novel application of bit-vector based abstraction methodology for formal verification of quantum circuits where superposition and functional behaviour can be decoupled. The approach is applied to error detection circuits for 2-qubit, 3-qubit, and Shor 9-qubit quantum codes, as well as Bell-state and GHZ-state generation circuits. The error detection circuits and the Bell-state generation circuit are verified in less than a second and 25MB memory. GHZ circuits with up to 8,192 qubits are verified in under three minutes using a maximum of 23.2 GB of memory. The results demonstrate the versatility, scalability, and effectiveness of the proposed approach.
ABSTRACT Many quantum algorithms operate on classical data, by first encoding classical data into the quantum domain using quantum data encoding circuits. To be effective for large data sets, encoding circuits that operate on large data sets are required. However, as the size of the data sets increases, the encoding circuits quickly become large, complex and error prone. Errors in the encoding circuit will provide incorrect inputs to quantum algorithms, making them ineffective. To address this problem, a formal method is proposed for verification of encoding circuits. The key idea to address scalability is the use of abstractions that reduce the verification problem to bit‐vector space. The major outcome of this work is that using this approach, the authors have been able to verify encoding circuits with up to 8191 qubits with very low memory (85 MB) and time (0.29s), demonstrating that the proposed approach can easily be employed to verify even much larger encoding circuits. The results are very significant because, traditional verification approaches that rely on modelling quantum circuits in Hilbert space have only demonstrated verification scalability up to 250 qubits. Also, this is the first approach to tackle the verification of quantum encoding circuits.
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.
To fully utilize the advances in quantum computing, it is critical to develop verification techniques that can scale and ensure the design of reliable and error-free quantum circuits. In this work, we propose a formal verification approach for a popular subset of quantum walk circuits, which are those that traverse cycles. Quantum walks are the quantum mechanical analog of random walks and as such have many safety- critical and security-critical applications. The proposed approach incorporates abstractions for quantum gates used in quantum walk circuits and correctness properties. Experimental results demonstrated that the verification approach is very efficient and is able to scale up to quantum walk circuits with as many as 5,000 qubits.
Quantum computing exploits the principles of quantum mechanics to perform computation. Information is stored in qubits and processed with a sequence of quantum gates arranged as circuits. Verifying the correctness of quantum circuits is becoming essential as hardware scales in qubit count and architectural complexity. Traditional testing and naive simulation do not scale and quickly become computationally infeasible because the state space grows exponentially. This creates a strong need for more powerful and scalable verification techniques. Formal methods offer a viable solution by providing mathematically rigorous and scalable verification techniques that address these scalability challenges through abstraction, symbolic reasoning, and probabilistic guarantees. This study examines how formal methods are applied to quantum circuit verification. Specifically, four families of formal techniques: barrier certificates, abstract interpretation, model checking, and theorem proving are examined, along with the theoretical foundations and practical applications of these techniques. Finally, the study highlights open challenges and identifies promising directions for future research. An extensive set of references is included to support further study and exploration.