Comment on F*: A general-purpose proof-oriented programming languageparentComments−nextaccountic1moFirefox cryptographic primitives are written and formally verified in F*Some Windows things too I think (I think F* is partially funded by Microsoft Research)They actually wrote a whole verified TLS implementation in F* and discovered a bunch of TLS vulnerabilities in other implementationshttps://project-everest.github.io/https://github.com/hacl-star/hacl-starhttps://blog.mozilla.org/security/2017/09/13/verified-crypto... (note, that's from 2017, so, not exactly new.. not sure how this is not more well known)
Comments
Firefox cryptographic primitives are written and formally verified in F*
Some Windows things too I think (I think F* is partially funded by Microsoft Research)
They actually wrote a whole verified TLS implementation in F* and discovered a bunch of TLS vulnerabilities in other implementations
https://project-everest.github.io/
https://github.com/hacl-star/hacl-star
https://blog.mozilla.org/security/2017/09/13/verified-crypto... (note, that's from 2017, so, not exactly new.. not sure how this is not more well known)