AutoQ 2.0: An automata-based C++ tool for quantum program verification.

AutoQ 2.0 is a command-line utility written in C++ for verifying partial correctness of quantum programs automatically based on non-deterministic finite tree automata (NFTA) along with the concept of Hoare-style proof systems.

Consider a triple { $P$ } $C$ { $Q$ }, where $P$ and $Q$ are the pre- and post-condition recognizing sets of pure quantum states and $C$ is a quantum program. Note that we don't consider mixed states in this work. Let $\mathcal L(x)$ denote the language (set) of all quantum states satisfying the condition $x$ and $C(L)$ denote the output set of quantum states generated by the quantum program $C$ transforming the initial set of quantum states $L$. Then essentially, AutoQ 2.0 simply checks whether each quantum state in $\mathcal L(P)$ reaches some state in $\mathcal L(Q)$ up to a nonzero complex factor after being transformed by the program $C$, i.e., whether $\forall \ket{s} \in C(\mathcal L(P)),\ \exists c\in\mathbb C\setminus\{0\}$ such that $c\ket{s}\in \mathcal L(Q)$. We may denote it by $C(\mathcal L(P)) \subseteq_{uts} \mathcal L(Q)$, where $uts$ is short for up to scaling.

The following is a simple illustration of the usage.

OPENQASM 3;
include "stdgates.inc";
qubit[2] qb; // quantum bits

//    L(P): {|00>, 0.5|00> + 0.5|01> + 0.5|10> + 0.5|11>}
x qb[0];
//          {|10>, 0.5|10> + 0.5|11> + 0.5|00> + 0.5|01>}
x qb[1];
//          {|11>, 0.5|11> + 0.5|10> + 0.5|01> + 0.5|00>}
h qb[1];
// C(L(P)): {|10>/√2 - |11>/√2, |10>/√2 + |00>/√2}
/******************************************************/
//  L(Q_1): {|10>/√2 - |11>/√2, |10>/√2 + |00>/√2} -> pass
//  L(Q_2): {|10>/√2 - |11>/√2, |10>/√2 - |00>/√2} -> fail

The program starts from an initial set of quantum states $\mathcal L(P)$. Immediately after executing each gate, AutoQ 2.0 computes the resulting transformation of the quantum states and stores it for use by the next gate. At the end of the quantum program, AutoQ 2.0 checks whether the set $\mathcal L(Q)$ contains the set $C(\mathcal L(P))$. In the above example, if we take the postcondition $Q_1$ such that $\mathcal L(Q_1) = C(\mathcal L(P))$, the verification passes. If we take another postcondition $Q_2$ such that there is some quantum state $\ket{10}/\sqrt2 + \ket{00}/\sqrt2 \in C(\mathcal L(P))$ but $\not\in \mathcal L(Q_2)$, the verification fails.

Please see the introductory video for more examples on its usage. You can also check the folder for all the files used to produce the experimental results.

---

Installation and Compilation

Currently, for Linux (Ubuntu/Debian), macOS, and WSL2, the dependency of AutoQ can be built with the command ./install-dependencies.sh. After the configuration, please run the following command.

make
make test

The first command make compiles the source code with compiler optimizations enabled, while the second command make test runs several unit tests to verify the correctness of the implementation. Under normal circumstances, you should see 12 green check marks on the Commits page for the latest commit. This indicates that the continuous integration (CI) workflow in GitHub Actions has verified that both make and make debug produce no errors and that make test passes successfully on Ubuntu, macOS, and WSL2.

If you need to compile the library for debugging, you can replace make with make debug.

---

Command-Line Execution

The following help message lists four modes, each of which can be accessed by typing its corresponding subcommand. Each subcommand also provides its own usage instructions via the -h option.

$ ./build/cli/autoq -h
AutoQ 2.0: An automata-based C++ tool for quantum program verification.
Usage: autoq [OPTIONS] [SUBCOMMAND]

Options:
  -h,--help                   Print this help message and exit.
  -v,--version                Print the full Git commit hash ID.

Subcommands:
  ex                          Execute a quantum circuit with a given precondition.
  ver                         Verify the execution result against a given postcondition.
  eq                          Check equivalence of two given quantum circuits.
  print                       Print the set of quantum states.

The most frequently used mode in our papers is ver for verifying quantum programs.

$ ./build/cli/autoq ver -h
Verify the execution result against a given postcondition.
Usage: autoq ver [OPTIONS] pre.hsl circuit.qasm post.hsl

Positionals:
  pre.hsl                     the precondition file
  circuit.qasm                the OpenQASM 2.0 or 3.0 circuit file
  post.hsl                    the postcondition file

Options:
  -h,--help                   Print this help message and exit.
  --loopsum                   Summarize loops using symbolic execution.
  -l,--latex                  Print the statistics for tables in LaTeX.

One noteworthy feature of this tool is its support for loop summarization in circuits that use the specific syntax for int i in [x:y] { C }, as described in the QASM format documentation. To enable the loop summarization algorithm, include the --loopsum flag when using the ex or ver subcommands.

This is one example usage.

$ ./build/cli/autoq ver benchmarks/all/Grover/03/pre.hsl benchmarks/all/Grover/03/circuit.qasm benchmarks/all/Grover/03/post.hsl
The quantum program has [5] qubits and [52] gates. The verification process [OK] in [0.1s] with [77MB] memory usage.

---

Input File Formats

• Quantum States
  Preconditions, postconditions, and loop invariants are all sets of quantum states. We use the *.hsl format (short for high-level specification language) which extends Dirac notation to describe sets of quantum states. The detailed grammar is described in the hsl format description.
  

• Quantum Programs
  Our program currently supports $X$, $Y$, $Z$, $H$, $T$, $T^\dagger$, $S$, $S^\dagger$, $R_x(\pi/2)$, $R_y(\pi/2)$, $CX$, $CZ$, $CCX$, $SWAP$ quantum gates. The supported version of OpenQASM can be 2.0 or 3.0, but the supported syntax is very limited. Please refer to the qasm format description for more details.

---

Citation

Please cite the following papers if you use this tool for your research.

• P. A. Abdulla, Y.-G. Chen, Y.-F. Chen, L. Holík, O. Lengál, J.-A. Lin, F.-Y. Lo, and W.-L. Tsai, “Verifying Quantum Circuits with Level-Synchronized Tree Automata,” in Proceedings of the ACM on Programming Languages 9 (POPL), 2025, pp. 923–953.

@article{10.1145/3704868,
  title = {Verifying Quantum Circuits with Level-Synchronized Tree Automata},
  author = {Abdulla, Parosh Aziz and Chen, Yo-Ga and Chen, Yu-Fang and Hol\'{\i}k, Luk\'{a}\v{s} and Leng\'{a}l, Ond\v{r}ej and Lin, Jyun-Ao and Lo, Fang-Yi and Tsai, Wei-Lun},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {POPL},
  year = {2025},
  pages = {923--953},
  doi = {10.1145/3704868}
}

• Y.-F. Chen, K.-M. Chen, M.-H. Hsieh, W.-J. Huang, O. Lengál, J.-A. Lin, and W.-L. Tsai, “AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2025, pp. 87–108

@InProceedings{10.1007/978-3-031-90660-2_5,
  author = {Chen, Yu-Fang and Chung, Kai-Min and Hsieh, Min-Hsiu and Huang, Wei-Jia and Leng{\'a}l, Ond{\v{r}}ej and Lin, Jyun-Ao and Tsai, Wei-Lun},
  booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
  title = {AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs},
  year = {2025},
  pages = {87--108},
  doi = {10.1007/978-3-031-90660-2_5}
}

---

Contact

If you have any questions or suggestions, feel free to create an issue or contact us via [email protected].