Quantum relational Hoare logic (qRHL) is a Hoare logic for analyzing pairs of quantum programs and their relationship. Concretely, it allows us to describe how the outputs relate if the inputs satisfy a certain precondition. We describe qRHL, explain its connection to the verification of quantum cryptography, and mention some of the challenges in its use. We describe current progress towards the formalization of qRHL (in Isabelle/HOL) and what the difficulties are.