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