CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler

Understand

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.