4 ms·

I think you you guys have formally proven some of this correct? What did you use? Was a proof-assistant like Coq or a model checker or similar? And what propert

by wsxcde 12y ago

I think you you guys have formally proven some of this correct? What did you use? Was a proof-assistant like Coq or a model checker or similar? And what properties have been proven correct (so we know what to avoid wasting time on :)?

pqwy 12y ago
No, or at least not yet. :) You are probably thinking of these guys: http://www.mitls.org http://www.mitls.org. They have a killer TLS, but it drags the entire CLR in. We are these guys: http://openmirage.org/blog/introducing-ocaml-tls http://openmirage.org/blog/introducing-ocaml-tls.
- wsxcde 12y ago
  You are right, I was thinking of miTLS.
deleted 12y ago
[deleted]