虽然量子硬件的最新进展为密码学以及其他关键领域（生物学、化学、优化、机器学习等）的显著加速打开了大门，但量子算法仍然难以正确实施，而且这种量子程序的验证是一项挑战。此外，由于量子测量的破坏性，在量子情况下引入传统编程中使用的测试和调试实践极其困难。作为一种替代策略，形式化方法很容易在量子软件这一新兴领域发挥决定性作用。最近的研究为开发过程的每个阶段出现的问题提供了解决方案：高级程序设计、实现、编译等。我们回顾了在量子计算中有效使用形式化方法所面临的挑战以及当前最有前途的研究方向。