{"id":"arxiv/2603.08762","url":"https://arxiv.org/abs/2603.08762","tags":["quant-ph","cs.FL","cs.LO"],"score":0,"title":"Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits","domain":"quant-ph","source":"arxiv","authors":["Arun Govindankutty","Sudarshan K. Srinivasan"],"reviews":0,"subject":"quant-ph","summary":"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…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"discussed":0,"published":"2026-03-09","reactions":{}}