We describe the ongoing development of a verified translator between OpenQASM (Open Quantum Assembly Language) and sQIR, a Small Quantum Intermediate Representation used for circuit optimization. Verified translation from and to OpenQASM will allow verified optimization of circuits written in a variety of tools and executed on real quantum computers. This translator is a step toward a verified compilation stack for quantum computing.

This is a merged talk with A Verified Optimizer for Quantum Circuits.