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.
@article{arxiv.2603.08762,
title = {Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits},
author = {Arun Govindankutty and Sudarshan K. Srinivasan},
journal= {arXiv preprint arXiv:2603.08762},
year = {2026}
}
Comments
The work is accepted for presentation as a full research paper in IEEE-DCAS 2026 and the final version will be available via IEEE Xplore after the conference