- CryptoVerif uses a probabilistic process calculus adapted to its use case, detailed in [1]; - There is no verified kernel. All algorithms, including an equat

- CryptoVerif uses a probabilistic process calculus adapted to its use case, detailed in [1]; - There is no verified kernel. All algorithms, including an equational prover for simplification of games, are implemented in ~30k to 40k LOC of OCaml. The correctness of CryptoVerif’s game transformations has been proved manually [1]. A formal link between these proofs and the OCaml code is not established; - During a proof, after each game transformation, CryptoVerif checks a list of invariants. This already allowed to find implementation errors in the past. - There are regression tests using proofs that have been done before with CryptoVerif, with both proofs that are supposed to succeed and proofs that are supposed to fail. To conclude, CryptoVerif has no high-assurance guarantees on its code like Coq and others, but is the only tool that is capable to treat complex real-world protocols. [1] https://prosecco.gforge.inria.fr/personal/bblanche/publications/BlanchetTDSC07.html https://prosecco.gforge.inria.fr/personal/bblanche/publicati...