  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.
