In the quantum computing era, the imperative role of post-quantum cryptography in securing digital communications has led to the development of computer-aided cryptography verification tools. These tools simplify the verification of post-quantum cryptography primitives and protocols, alleviating the challenges associated with manual proofs. This paper systematically reviews research in four main areas: quantum computing, post-quantum cryptography, cryptanalysis, and verification, establishing a foundation for future research. Emphasising the significance of challenges in post-quantum cryptography, we outline the current state of research on cryptography primitives and protocols. Categorising state-of-the-art computer-aided cryptography verification tools based on assumptions, models, and application levels, our analysis delves into each tool’s features, including modelling, adversary models, security properties, validation, and an in-depth analysis of their limitations. This comprehensive analysis offers insights into the nexus of post-quantum cryptography and computer-aided verification. Concluding with recommendations for researchers and practitioners, this paper explores potential future research directions.