Author of Rosenpass here; Coq is fairly generic; it has a long history and made it possible to write some really cool proofs such as a proof of the four colors

Author of Rosenpass here; Coq is fairly generic; it has a long history and made it possible to write some really cool proofs such as a proof of the four colors theorem, but writing crypto proofs is really hard using Coq. For symbolic verification Tamarin and ProVerif are the tools of choice; I used ProVerif. For proofs of security for protocols EasyCrypt and CryptoVerif can be used. CryptoVerif, ProVerif and Coq where developed at the same Institute by the way; at Inria Paris.