  As quantum computing progresses steadily from theory into practice,
programmers will face a common problem: How can they be sure that their code
does what they intend it to do? This paper presents encouraging results in the
application of mechanized proof to the domain of quantum programming in the
context of the SQIR development. It verifies the correctness of a range of a
quantum algorithms including Grover's algorithm and quantum phase estimation, a
key component of Shor's algorithm. In doing so, it aims to highlight both the
successes and challenges of formal verification in the quantum context and
motivate the theorem proving community to target quantum computing as an
application domain.
