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 3.5 GB of memory.
Journal reference
2026 IEEE 19th Dallas Circuits and Systems Conference (DCAS)
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 3.5 GB of memory.
Formal verification of quantum circuits becomes difficult as circuit size grows because exhaustive reasoning over the Hilbert space is computationally expensive. In previous work [1], we introduced a bit-vector abstraction that separates superposition tracking from basis-state behavior, enabling SMT-based verification of fixed-size error-detection and entanglement circuits built from H, X, and C-NOT gates. This paper extends the framework in five directions. First, we generalise correctness properties to parametrised repetition and concatenated phase-flip codes with up to 101 logical elements. Second, we verify syndrome extraction for CSS codes specified by arbitrary parity-check matrices, including the Steane, [[15,7,3]] Hamming, [[15,1,3]] Reed-Muller, and rotated surface codes with distances up to 101. We consider arbitrary error patterns, detection up to a specified weight, and recovery using a classical decoder, with counterexamples beyond each code's correction or detection capability. Third, we characterize the {H,X,C-NOT} fragment for which the abstraction faithfully represents Hilbert-space semantics. We prove soundness, demonstrate necessity with counterexamples, validate the characterisation against state-vector simulation, and prove the six lemmas from the original work. Fourth, a mutation study using 13 operators identifies equivalent mutants and detects all 622 non-equivalent mutants within the evaluated fault model. Fifth, a direct Z3 implementation verifies GHZ circuits with up to 262,144 qubits across three topologies on a 16GB laptop. Random H+C-NOT networks show verification cost rises sharply with depth when outputs depend on many inputs. The approach does not target general stabilizer circuits, Y-type stabilizers, fault-tolerant protocols, or physical noise; we identify extensions needed to address these cases.
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.
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.
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.
This research paper provides an in-depth examination of verification and testing approaches for quantum circuits, focusing on methodologies essential for ensuring the correctness, reliability and operational efficiency of quantum computing systems. Since quantum circuits function on the fundamental principles of superposition and entanglement, they present verification challenges that cannot be effectively addressed using conventional classical testing techniques. As a result, the development of specialized quantum-specific verification strategies has become critically important. The study highlights simulation-based verification as a foundational technique, wherein the outcomes of quantum circuit simulations are systematically compared with results obtained from physical quantum hardware. This process enables the identification of functional inconsistencies and supports iterative refinement of circuit designs. In addition, randomized benchmarking is examined as a key evaluation method for estimating circuit fidelity and quantifying error rates through the application of random gate sequences and performance comparisons against established benchmarks. To further improve system robustness, the research investigates fault-tolerant mechanisms, particularly quantum error correction codes, which play a vital role in minimizing the effects of noise, decoherence and hardware imperfections. The integration of advanced quantum metrology and characterization techniques is also explored, enabling precise measurement and detailed analysis of quantum system behavior. These techniques provide deeper insights into circuit performance and contribute significantly to validation processes. By combining simulation-based verification, randomized benchmarking, fault-tolerant protocols and quantum metrology, this study proposes a comprehensive and reliable framework for quantum circuit verification and testing. The findings contribute to the advancement of dependable quantum technologies and support their growing applications in areas such as cryptography, materials science and other emerging domains.
Quantum computing uses the laws of quantum mechanics to perform computation. Information is stored in qubits and processed using quantum gates arranged as quantum circuits. As quantum hardware grows in size and complexity, verifying these systems becomes increasingly difficult. Traditional verification methods do not scale well and quickly become computationally infeasible. This creates a strong need for more powerful and scalable verification techniques. Formal methods provide a potential solution to this problem. Techniques such as theorem proving, model checking, and symbolic reasoning offer mathematically rigorous ways to verify correctness, equivalence, and implementation. They also help detect design errors early in the development process. This review examines how formal methods are applied to quantum circuit verification. It focuses on barrier certificates, abstract interpretation, model checking, theorem proving approaches. The review discusses both the theoretical foundations and practical applications of these techniques. Their strengths and limitations are analysed through representative case studies. Finally, the review highlights open challenges and identifies promising directions for future research. An extensive set of references is included to support further study and exploration.