I will present our recent advances in the formal verification of post-quantum security. Our framework includes a logic for reasoning about quantum programs (qRHL, quantum relational Hoare logic) and a tool for computer-aided verification in qRHL. We have used this framework to verify the post-quantum security of the Fujisaki-Okamoto transform for building encryption schemes. I will give an overview of the logical foundations and of our experiences when verifying a real-life cryptosystem.