# A Verified Optimizer for Quantum Circuits

arXiv: https://arxiv.org/abs/1912.02250 · HTML: https://mlsanity.com/paper/1912.02250/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 4 Dec 2019.

## Built on by (most cited first, 7 of 7)

- [Quarl: A Learning-Based Quantum Circuit Optimizer](https://mlsanity.com/paper/2307.10120/) (2023)
- [Quantum Circuit Synthesis and Compilation Optimization: Overview and Prospects](https://mlsanity.com/paper/2407.00736/) (2024)
- [Optimizing Quantum Circuits via ZX Diagrams using Reinforcement Learning and Graph Neural Networks](https://mlsanity.com/paper/2504.03429/) (2025)
- [VEL: A Formally Verified Reasoner for OWL2 EL Profile](https://mlsanity.com/paper/2412.08739/) (2024)
- [AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics](https://mlsanity.com/paper/2609.05157/) (2026)
- [Reinforcement Learning for Adaptive Composition of Quantum Circuit Optimisation Passes](https://mlsanity.com/paper/2601.21629/) (2026)
- [Bridge of Psi's: Quantum Circuit Optimization with Schr"odinger Bridges](https://mlsanity.com/paper/2609.25947/) (2026)

## Abstract (arXiv)

We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a simple quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. SQIR uses a semantics of matrices of complex numbers, which is the standard for quantum computation, but treats matrices symbolically in order to reason about programs that use an arbitrary number of quantum bits. SQIR's careful design and our provided automation make it possible to write and verify a broad range of optimizations in VOQC, including full-circuit transformations from cutting-edge optimizers.