Cryptographic primitive programs are the building blocks of computer cryptography. In this talk, I will motivate the verification problem of cryptographic primitive programs and present the automatic formal verification tool CoqCryptoLine to address the problem. CoqCryptoLine is a formally verified tool for cryptographic primitive programs. It is built upon OCAML programs extracted from algorithms verified in the proof assistant Coq. Its verification results are moreover validated by certificate checkers. We will see the design of CoqCryptoLine. Verification results of cryptographic primitive programs from Bitcoin, OpenSSL, and Kyber NTT will also be presented.