I do have some questions about the assurance CryptoVerif provides. I'm a non-mathematician that does research in high-assurance security that tracks formal verification results. What I've read indicates problems can kick in at places like this:
1. The logic or modelling used isn't proven sound. There's been tons of analysis into things like set theory or HOL Light. Is CryptoVerif using a proven logic?
2. Recent designs favor kernelized models where about every step or transition can be proven consistent or just not mess up to begin with. Does CryptoVerif do this or is there a lot of complexity in it?
3. The solvers might themselves make mistakes. One mitigation was them simply driving the steps in 2 that were easy to check and/or providing a log of work for a trusted checker. Any risks on automated part to worry about?
4. Small, verifiable TCB. HOL Light and Milawa were explicitly designed for this. Does CryptoVerif have a trusted checker? Are the design and implementation of above done in a tiny, easy-to-verify fashion? The EasyCrypt paper's comparisons to CryptoVerif and CertiCrypt made me think it doesn't.
5. Verification activities on the code itself, source and/or binary, from static analysis to property-based testing. Empirical evidence suggests these catch problems proofs sometimes miss, esp due to specification errors. Even CompCert had a few. Any of this on CryptoVerif's building blocks?
The answers to these questions might be helpful to people interested in boosting the assurance of this or other tools in the future. After all, the proofs can only be as strong as the foundations they're built on.