We present CertiQ, a verification framework for writing and verifying compiler passes of Qiskit, the most widely-used quantum compiler. To our knowledge, CertiQ is the first effort enabling the verification of real-world quantum compiler passes in a mostly-automated manner. Compiler passes written in the CertiQ interface with annotations can be used to generate verification conditions, as well as the executable code that can be integrated into Qiskit. CertiQ introduces the quantum circuit calculus to enable the efficient checking of equivalence of quantum circuits by encoding such a checking procedure into an SMT problem. CertiQ also provides a verified library of widely-used data structures, transformation functions for circuits, and conversion functions for different quantum data representations. This verified library not only enables modular verification but also sheds light on future quantum compiler design. We have re-implemented and verified 26 (out of 30) Qiskit compiler passes in CertiQ, during which three bugs are detected in the Qiskit implementation. Our verified compiler pass implementations passed all of Qiskit's regression tests without showing noticeable performance loss.We present CertiQ, a verification framework for writing and verifying compiler passes of Qiskit, the most widely-used quantum compiler. To our knowledge, CertiQ is the first effort enabling the verification of real-world quantum compiler passes in a mostly-automated manner. Compiler passes written in the CertiQ interface with annotations can be used to generate verification conditions, as well as the executable code that can be integrated into Qiskit. CertiQ introduces the quantum circuit calculus to enable the efficient checking of equivalence of quantum circuits by encoding such a checking procedure into an SMT problem. CertiQ also provides a verified library of widely-used data structures, transformation functions for circuits, and conversion functions for different quantum data representations. This verified library not only enables modular verification but also sheds light on future quantum compiler design. We have re-implemented and verified 26 (out of 30) Qiskit compiler passes in CertiQ, during which three bugs are detected in the Qiskit implementation. Our verified compiler pass implementations passed all of Qiskit's regression tests without showing noticeable performance loss.

arXiv:1908.08963Aug 23, 201910 citations

Automated Compilation Including Dropouts: Tolerating Defective Components in Stabiliser Codes

Stasiu Wolanski

Utility-scale solid-state quantum devices will need to fabricate quantum devices at scale using imperfect processes. By introducing tolerance to fabrication defects into the design of the quantum devices, we can improve the yield of usable quantum chips and lower the cost of useful systems. Automated Compilation Including Dropouts (ACID) is a framework that works in the ancilla-free (or `middle-out') paradigm, to generate syndrome extraction circuits for general stabiliser codes in the presence of defective couplers or qubits. In the ancilla-free paradigm, we do not designate particular qubits as measurement ancillas, instead measuring stabilisers using any of the data qubits in their support. This approach leads to a great deal of flexibility in how syndrome extraction circuits can be implemented. ACID works by constructing and solving an optimisation problem within the ancilla-free paradigm to find a short syndrome extraction circuit. Applied to the surface code, ACID produces syndrome-extraction circuits of depth between $1\times$ (no overhead) and $1.5\times$ relative to the depth of defect-free circuits. The LUCI algorithm, the best prior art, yielded a $2 \times$ overhead, so ACID offers a significant time saving. The yield of surface code chips with a logical error rate at most $10\times$ the dropout-free baseline is up to $3\times$ higher using ACID than using LUCI. I demonstrate the broad applicability of ACID by compiling syndrome extraction circuits for bivariate bicycle codes and the colour code. For these circuits, we incur a circuit-depth overhead of between $1\times$ (no overhead) and $2.5\times$ relative to defect-free circuits. I believe this work is the first to simulate both of these families of codes in the presence of fabrication defects.Utility-scale solid-state quantum devices will need to fabricate quantum devices at scale using imperfect processes. By introducing tolerance to fabrication defects into the design of the quantum devices, we can improve the yield of usable quantum chips and lower the cost of useful systems. Automated Compilation Including Dropouts (ACID) is a framework that works in the ancilla-free (or `middle-out') paradigm, to generate syndrome extraction circuits for general stabiliser codes in the presence of defective couplers or qubits. In the ancilla-free paradigm, we do not designate particular qubits as measurement ancillas, instead measuring stabilisers using any of the data qubits in their support. This approach leads to a great deal of flexibility in how syndrome extraction circuits can be implemented. ACID works by constructing and solving an optimisation problem within the ancilla-free paradigm to find a short syndrome extraction circuit. Applied to the surface code, ACID produces syndrome-extraction circuits of depth between $1\times$ (no overhead) and $1.5\times$ relative to the depth of defect-free circuits. The LUCI algorithm, the best prior art, yielded a $2 \times$ overhead, so ACID offers a significant time saving. The yield of surface code chips with a logical error rate at most $10\times$ the dropout-free baseline is up to $3\times$ higher using ACID than using LUCI. I demonstrate the broad applicability of ACID by compiling syndrome extraction circuits for bivariate bicycle codes and the colour code. For these circuits, we incur a circuit-depth overhead of between $1\times$ (no overhead) and $2.5\times$ relative to defect-free circuits. I believe this work is the first to simulate both of these families of codes in the presence of fabrication defects.

quant-pharXiv:2512.01943Dec 2, 20250 citations

Automated Design of Quantum Circuits

Colin P. Williams, Alexander Gray

Lecture notes in computer scienceJan 1, 199953 citations

1\times

(no overhead) and

1.5\times

relative to the depth of defect-free circuits. The LUCI algorithm, the best prior art, yielded a

2 \times

overhead, so ACID offers a significant time saving. The yield of surface code chips with a logical error rate at most

10\times

the dropout-free baseline is up to

3\times

higher using ACID than using LUCI. I demonstrate the broad applicability of ACID by compiling syndrome extraction circuits for bivariate bicycle codes and the colour code. For these circuits, we incur a circuit-depth overhead of between

1\times

(no overhead) and

2.5\times

relative to defect-free circuits. I believe this work is the first to simulate both of these families of codes in the presence of fabrication defects.