AutoQ 2.0: quantum program verification

What AutoQ checks

A Hoare triple {P} C {Q} is a claim about a program C: run it from a state allowed by the precondition P, and if it terminates, it ends in a state allowed by the postcondition Q. This is partial correctness, and AutoQ checks claims of this kind for quantum programs, up to scaling.

In AutoQ, P and Q each describe a set of pure quantum states rather than a single state. AutoQ starts from the whole set ℒ(P), computes how it is transformed immediately after each gate, and hands the result to the next gate. When the program ends, it checks that ℒ(Q) contains the final set C(ℒ(P)), up to scaling:

C(ℒ(P)) ⊆_uts ℒ(Q)

That is, for every state |s⟩ ∈ C(ℒ(P)) there is a nonzero complex number c ∈ ℂ∖{0} with c|s⟩ ∈ ℒ(Q). A postcondition can therefore leave out normalization factors such as 1/√2; the worked example below relies on exactly that.

Sets of states as tree automata

AutoQ represents a set of states with a tree automaton. A state becomes a tree with one level per qubit, and each leaf stores one amplitude: in Figure 1 the leaf 000 stores the amplitude of |000⟩, 001 that of |001⟩, and so on. One automaton accepts many such trees, so it can stand for a whole set of states.

AutoQ 2.0 uses level-synchronized tree automata, in which each transition carries a set of choices. It also reorders qubits according to the precondition, postcondition and loop invariants, to keep the automata it builds small.

Figure 1. A 3-qubit state as a tree, one level per qubit. The leaf 000 stores the amplitude of |000⟩, and so on. Redrawn from docs/internal_structure.md.

A worked example

This two-qubit example is adapted from the README. The precondition holds two states, and the program applies three gates. Each step shows the set of states after one more gate, the tree of each state, and the output of autoq ex on the program up to that point.

pre.hsl

Extended Dirac
{|00>, 1/2 |00> + 1/2 |01> + 1/2 |10> + 1/2 |11>}

circuit.qasm

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

x qb[0];
x qb[1];
h qb[1];

circuit0.qasm, circuit1.qasm and circuit2.qasm in the steps below are the same file cut after zero, one and two gates.

0 Start from the precondition
ℒ(P) = {|00⟩, 12|00⟩ + 12|01⟩ + 12|10⟩ + 12|11⟩}

Two states: the basis state |00⟩ and the equal superposition of all four basis states.
Run on a circuit with no gates
```
$ autoq ex pre.hsl circuit0.qasm
OUTPUT:
{(1/1)|00>,
 (1/2)|00> + (1/2)|01> + (1/2)|10> + (1/2)|11>}
```
1 x qb[0];
{|10⟩, 12|10⟩ + 12|11⟩ + 12|00⟩ + 12|01⟩}

X flips the left bit, so in every tree the two halves under the root swap. The equal superposition maps onto itself, which is why its tree and its line of output do not change.
Run on the circuit up to this gate
```
$ autoq ex pre.hsl circuit1.qasm
OUTPUT:
{(1/1)|10>,
 (1/2)|00> + (1/2)|01> + (1/2)|10> + (1/2)|11>}
```
2 x qb[1];
{|11⟩, 12|11⟩ + 12|10⟩ + 12|01⟩ + 12|00⟩}

X flips the right bit, so under each node of the next level the two leaves swap.
Run on the circuit up to this gate
```
$ autoq ex pre.hsl circuit2.qasm
OUTPUT:
{(1/1)|11>,
 (1/2)|00> + (1/2)|01> + (1/2)|10> + (1/2)|11>}
```
3 h qb[1];
C(ℒ(P)) = {|10⟩/√2 − |11⟩/√2, |10⟩/√2 + |00⟩/√2}

H on qb[1] mixes each pair of sibling leaves a, b into (a+b)/√2 and (a−b)/√2. This is the final set C(ℒ(P)); AutoQ prints 1/√2 as sqrt2*1/2.
Run on the whole circuit
```
$ autoq ex pre.hsl circuit.qasm
OUTPUT:
{(sqrt2*1/2)|10> + (sqrt2*-1/2)|11>,
 (sqrt2*1/2)|00> + (sqrt2*1/2)|10>}
```

4 Check against two postconditions

Postcondition Q₁ passes

post_Q1.hsl

Extended Dirac
{|10> - |11>, |10> + |00>}

$ autoq ver pre.hsl circuit.qasm post_Q1.hsl
The quantum program has [2] qubits and [3] gates. The verification process [OK] in [0.2s] with [77MB] memory usage.

The same two states without the 1/√2 factors. They match up to scaling, so the check passes.

Postcondition Q₂ fails

post_Q2.hsl

Extended Dirac
{|10> - |11>, |10> - |00>}

$ autoq ver pre.hsl circuit.qasm post_Q2.hsl
The quantum program has [2] qubits and [3] gates. The verification process [failed] in [0.1s] with [77MB] memory usage.

One sign is flipped. The state |10⟩/√2 + |00⟩/√2 is in C(ℒ(P)), but no nonzero factor turns it into a state of ℒ(Q₂).

Get started

To try AutoQ without installing anything, open the playground: it runs the same tool in your browser, compiled to WebAssembly, with the examples from this page ready to run.

To install it, AutoQ builds from source on Linux (Ubuntu or Debian), macOS and WSL2. Four steps take you from a fresh clone to a verified program.

Clone the repository

Clone

git clone https://github.com/fmlab-iis/AutoQ.git
cd AutoQ

Install the dependencies
Ubuntu, Debian, WSL2
```
sudo ./install-dependencies.sh
```
macOS
```
./install-dependencies.sh
```
On Ubuntu and Debian, including under WSL2, the script installs g++, make, cmake, libboost-filesystem-dev, libboost-test-dev and libantlr4-runtime-dev with apt, so run it with sudo. On macOS, run it without sudo: it uses Homebrew to install gcc, make, cmake, boost and antlr4-cpp-runtime.
Build and test
Build and test
```
make
make test
```
make compiles AutoQ with optimizations, and make test runs the unit tests. The binary is build/cli/autoq. For a debug build, run make debug instead of make.
Verify a program

ver is the mode used most often in the AutoQ papers. It takes a precondition, a circuit and a postcondition. Here it checks the README’s example, a Grover’s search benchmark on five qubits.
Verify the example
```
$ ./build/cli/autoq ver \
    benchmarks/all/Grover/03/pre.hsl \
    benchmarks/all/Grover/03/circuit.qasm \
    benchmarks/all/Grover/03/post.hslThe quantum program has [5] qubits and [52] gates. The verification process [OK] in [0.1s] with [77MB] memory usage.
```
Times and memory figures in the outputs on this page come from one machine and will vary on yours.
pre.hsl
```
Constants
c1 := 1
Extended Dirac
{c1 |00000>}
```
post.hsl
```
Constants
aH := 11 / (sqrt2 ^ 7)
aL := -1 / (sqrt2 ^ 7)
Extended Dirac
{aH |01001> + aL ∑ |i|=3, i≠010 |i01>}
```
The demo folder has more small examples, including Bernstein–Vazirani and a Grover iteration.

Commands

ex: autoq ex [OPTIONS] pre.hsl circuit.qasm
Execute a quantum circuit with a given precondition.
Option: --loopsum
ver: autoq ver [OPTIONS] pre.hsl circuit.qasm post.hsl
Verify the execution result against a given postcondition.
Options: --loopsum, -l, --latex
eq: autoq eq [OPTIONS] circuit1.qasm circuit2.qasm
Check equivalence of two given quantum circuits.
Option: --loopsum
print: autoq print [OPTIONS] states.hsl
Print the set of quantum states.

--loopsum summarizes loops using symbolic execution. -l, --latex on ver prints the statistics for tables in LaTeX. autoq -v prints the full Git commit hash.

From circuits to programs

AutoQ 2.0 goes beyond straight-line circuits. It verifies programs that measure, branch and loop, and it accepts symbolic amplitudes in specifications. AutoQ can also check whether two circuits are equivalent.

4.1 Symbolic amplitudes

An amplitude may use names that are not declared in the Constants section. AutoQ treats them as free symbolic variables, which the optional Constraints section can restrict. The precondition below, {x|0⟩ + y|1⟩}, therefore stands for every state of that form, and the postcondition requires each amplitude to come back unchanged.

benchmarks/all/H2Sym/pre.hsl

Extended Dirac
{x |0> + y |1>}

H2Sym/post.hsl

Extended Dirac
{p1 |0> + p2 |1>}
Constraints
real(p1) = real(x)
imag(p1) = imag(x)
real(p2) = real(y)
imag(p2) = imag(y)

Applying H twice passes. In the H2BugSym benchmark the second H is replaced by Y, and verification fails.

Gates of H2Sym/circuit.qasm, and the run

h qubits[0];
h qubits[0];
$ autoq ver pre.hsl circuit.qasm post.hsl
The quantum program has [1] qubits and [2] gates. The verification process [OK] in [0.2s] with [85MB] memory usage.

Gates of H2BugSym/circuit.qasm, and the run

h qubits[0];
y qubits[0];
$ autoq ver pre.hsl circuit.qasm post.hsl
The quantum program has [1] qubits and [2] gates. The verification process [failed] in [0.2s] with [86MB] memory usage.

4.2 Measurement, branching and loops

A program can measure a qubit into a classical bit and then branch on it with if and else, or loop on it with while. The if block runs on the states where the outcome is 1, the else block on those where it is 0, and AutoQ joins the two results. Both if (!c) and while (!c) are allowed, and else is optional.

A while loop needs a measurement just before the loop and at the end of its body, plus a loop invariant: a set of states in its own .hsl file, named in a comment on the while line. AutoQ checks that the states reaching the loop lie in the invariant, and that one pass of the body maps the invariant’s continuing states back into it. It then carries on with the states that leave the loop.

benchmarks/all/control_mini/while/circuit.qasm

OPENQASM 3;
include "stdgates.inc";
qubit[2] qb;
bit[2] outcome;

h qb[0];
cx qb[0], qb[1];
outcome[0] = measure qb[0];
while (!outcome[0]) { // loop-invariant.hsl
    x qb[0];
    h qb[0];
    cx qb[0], qb[1];
    outcome[0] = measure qb[0];
}

loop-invariant.hsl

Extended Dirac
{|00> - |11>,
 |01> - |10>}

pre.hsl and post.hsl (identical)

Extended Dirac
{|10>, |11>}

$ autoq ver pre.hsl circuit.qasm post.hsl
The quantum program has [2] qubits and [6] gates. The verification process [OK] in [0.2s] with [84MB] memory usage.

4.3 Loop summarization

A loop for int i in [x:y] { C } runs its body C exactly y − x + 1 times. By default AutoQ applies the body’s gates one iteration after another. With --loopsum on ex or ver, AutoQ applies its loop summarization algorithm, which uses symbolic execution, to the loop’s body.

From docs/qasm_description.md

...
qreg qb[1]; // quantum register
...
for int i in [1:2] {
    h qb[0];
    t qb[0];
}
...

4.4 Circuit equivalence

autoq eq checks whether two circuits are equal. A CX gate equals a CZ placed between two H gates on the target qubit; reversing control and target gives a different circuit.

a.qasm

OPENQASM 2.0;
include "qelib1.inc";
qreg q[2];
cx q[0], q[1];

b.qasm

OPENQASM 2.0;
include "qelib1.inc";
qreg q[2];
h q[1];
cz q[0], q[1];
h q[1];

$ autoq eq a.qasm b.qasm
The two quantum programs are verified to be [equal] in [0.0s] with [7MB] memory usage.
$ autoq eq a.qasm c.qasm  # c.qasm: cx q[1], q[0];
The two quantum programs are verified to be [unequal] in [0.0s] with [7MB] memory usage.

4.5 Gate set

AutoQ documents the fourteen gates below, written in OpenQASM with the spelling shown under each. Gates the parser does not recognise, such as u3 or cy, stop the run with an unsupported gate error.

Xx
Yy
Zz
Hh
Tt
T†tdg
Ss
S†sdg
R_x(π/2)rx(pi/2)
R_y(π/2)ry(pi/2)
CXcx
CZcz
CCXccx
SWAPswap

Writing specifications

Preconditions, postconditions and loop invariants are all sets of quantum states. Specifications are written in .hsl or .lsta; programs in .qasm.

.hsl: A high-level specification language that extends Dirac notation to describe sets of quantum states. A file has a Constants section (optional), an Extended Dirac section, and a Constraints section (optional), in that order.
The .hsl format
.qasm: OpenQASM 2.0 or 3.0, with very limited syntax: a single quantum register, classical bits used only right before control flow, the fourteen gates above, if/else, while and for.
The supported OpenQASM subset
.lsta: A set of states written directly as a level-synchronized tree automaton. It keeps Constants and Constraints and replaces Extended Dirac with Root States and Transitions.
The .lsta format

Reading an .hsl file

The GHZall/002 benchmark runs a two-qubit circuit, h qubits[0]; cx qubits[0], qubits[1];, on all four basis states at once.

GHZall/002/pre.hsl

Constants
c1 := 1
Extended Dirac
{c1 |ji> : |j|=1, |i|=1}

GHZall/002/post.hsl

Constants
cp := 1/sqrt2
cn := -1/sqrt2
Extended Dirac
{cp |0i> + cp |1i'> : |i|=1} ∪
{cp |0i> + cn |1i'> : |i|=1}

{c1 |ji> : |j|=1, |i|=1} lets j and i range over 1-bit strings, so the precondition holds all four basis states. autoq print pre.hsl lists them.
In |1i'>, i' is the bitwise complement of i.
∪ joins two sets: here, the states with a plus sign and those with a minus sign.

$ autoq print pre.hsl
{(1/1)|11>,
 (1/1)|10>,
 (1/1)|01>,
 (1/1)|00>}

$ autoq ver pre.hsl circuit.qasm post.hsl
The quantum program has [2] qubits and [2] gates. The verification process [OK] in [0.1s] with [77MB] memory usage.

Table 1. Extended Dirac notation at a glance

Extended Dirac notation
Notation	Meaning	ASCII
S ∪ T	union of two sets of states
S ⊗ T	tensor product of two sets	`S * T`
S ^ n	tensor power
\|i⟩, \|1i′⟩	binary-string variable (lowercase), and its complement	`\|1i'>`
∑ \|i\|=4, i≠0101 \|i⟩	sum over strings that meet the constraints	`Σ`, `!=`
{ … : \|s\|=4, s≠0101 }	set-builder notation with constraints	`!=`
= ≠ < ≤ > ≥ ¬ ∧ ∨	operators in the `Constraints` section, one conjunct per line	`!= <= >= ! && \|\|`

Kets can be closed with ⟩ or >. Constants may use real(c), imag(c), eipi(r), ei2pi(r), sqrt2, nonnegative integers and + - * / ^.

Papers

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

Verifying Quantum Circuits with Level-Synchronized Tree Automata

Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen, Lukáš Holík, Ondřej Lengál, Jyun-Ao Lin, Fang-Yi Lo, Wei-Lun Tsai

Proceedings of the ACM on Programming Languages 9 (POPL), 2025, pp. 923–953

doi:10.1145/3704868 Benchmarks: POPL25

BibTeX

@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}
}

AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs

Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Wei-Jia Huang, Ondřej Lengál, Jyun-Ao Lin, Wei-Lun Tsai

International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2025, pp. 87–108

doi:10.1007/978-3-031-90660-2_5 Benchmarks: TACAS25

BibTeX

@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}
}

The benchmarks folder holds all the files used to produce the experimental results.

Learn more, ask questions

Watch

The introductory video shows more examples of how to use AutoQ.

Watch the introductory video on YouTube

Read

READMEOverview, installation, usage
The .hsl formatExtended Dirac, constants, constraints
The OpenQASM subsetGates, measurement, if-else, while, for
The .lsta formatWriting tree automata directly
Internal structureHow trees encode quantum states

Ask

If you have any questions or suggestions, create an issue on GitHub or contact us via alan23273850@gmail.com.

AutoQ 2.0

What AutoQ checks

Sets of states as tree automata

A worked example

0 Start from the precondition

1 `x qb[0];`

2 `x qb[1];`

3 `h qb[1];`

4 Check against two postconditions

Postcondition Q₁ passes

Postcondition Q₂ fails

Get started

Clone the repository

Install the dependencies

Build and test

Verify a program

Commands

From circuits to programs

4.1 Symbolic amplitudes

4.2 Measurement, branching and loops

4.3 Loop summarization

4.4 Circuit equivalence

4.5 Gate set

Writing specifications

Reading an .hsl file

Papers

Verifying Quantum Circuits with Level-Synchronized Tree Automata

AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs

Learn more, ask questions

Watch

Read

Ask

AutoQ 2.0

1What AutoQ checks

Sets of states as tree automata

2A worked example

0 Start from the precondition

1 x qb[0];

2 x qb[1];

3 h qb[1];

4 Check against two postconditions

Postcondition Q1 passes

Postcondition Q2 fails

3Get started

Clone the repository

Install the dependencies

Build and test

Verify a program

Commands

4From circuits to programs

4.1 Symbolic amplitudes

4.2 Measurement, branching and loops

4.3 Loop summarization

4.4 Circuit equivalence

4.5 Gate set

5Writing specifications

Reading an .hsl file

6Papers

Verifying Quantum Circuits with Level-Synchronized Tree Automata

AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs

7Learn more, ask questions

Watch

Read

Ask

What AutoQ checks

A worked example

1 `x qb[0];`

2 `x qb[1];`

3 `h qb[1];`

Postcondition Q₁ passes

Postcondition Q₂ fails

Get started

From circuits to programs

Writing specifications

Papers

Learn more, ask questions