Serving as a foundation, cryptography is the key technique for ensuring network and information security. However, cryptographic implementations suffer from various security threats. Formal verification is the most important technique for rigorously proving the security of cryptographic implementations. This article first reviews the development status and application of formal verification techniques for cryptographic implementations both in China and abroad in terms of functional correctness, memory security, and side-channel security including time and power consumption. Then the article summarizes the drawbacks, current challenges, and development trends of these formal verification techniques for cryptographic implementations. According to the security requirements and limited progress in formal verification techniques for cryptographic implementations in China, it is suggested that high-performance and high-assurance cryptographic libraries should be constructed. In addition, the article proposes to follow the top-down design principle, strengthen independent innovation, and unify intermediate representation language under the guidance of national key task, and it plans to develop a high-efficiency, high-precision, and full-automated formal verification platform and a secure compiler optimization toolchain, create high-performance and high-assurance common cryptographic library with minimized trusted computing base, and promote the integrated development of both academic and industrial communities, so as to improve national network and information security.