|
|
|
|
|
|
by jraph
1212 days ago
|
|
|
Related: Coq - https://coq.inria.fr/ And CompCert, a formally verified C compiler written in Coq: https://compcert.org/ (even then, there are parts which are not formally verified, mostly at the interfaces with the outside world) |
|
|
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.