Hon Hai Research Institute and Academia Sinica Unveil AutoQ 2.0: A Breakthrough Tool for Quantum Program Verification at TACAS 2025
Hon Hai Research Institute and Academia Sinica Unveil AutoQ 2.0: A Breakthrough Tool for Quantum Program Verification at TACAS 2025

Dr. Min-Hsiu Hsieh, Director of the Quantum Computing Research Center at Hon Hai Research Institute, and Research Scientist Wei-Chia Huang, in collaboration with researchers from Academia Sinica (Taiwan) and institutions in the Czech Republic, have presented their latest work entitled “AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs” at TACAS 2025 (31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems). The paper has been published by Springer in the Lecture Notes in Computer Science (LNCS), Volume 15698, and is available open access.
AutoQ 2.0 is a new automatic verification tool designed specifically for quantum programs. Building on the original AutoQ 1.0 — which was limited to quantum circuit verification — the new version supports quantum programs with classical control structures, such as conditional branches and loops. This major extension addresses both theoretical and engineering challenges, including quantum measurement and state normalization, as well as the adaptation of loop invariant techniques from classical to quantum program verification.
The team successfully applied AutoQ 2.0 to verify two classes of advanced quantum algorithms that cannot be represented purely as quantum circuits: the Repeat-Until-Success (RUS) algorithm and a weak-measurement-based version of Grover’s search algorithm. Experimental results show that AutoQ 2.0 efficiently verifies all tested cases. In particular, all RUS algorithms were verified instantaneously, and the Grover variant with 100 qubits was verified in approximately 20 minutes.
This research represents a major technological advancement in quantum computing and formal verification from Taiwan, offering a powerful new tool for the global quantum software community. With the release of AutoQ 2.0, the team aims to accelerate the development and deployment of quantum algorithms and facilitate the practical application of quantum technologies.
The full paper is freely available via Springer’s official website:
👉 https://link.springer.com/chapter/10.1007/978-3-031-90660-2_5


