catalin_hritcu

6 ms·

1. 1.▲
   by catalin_hritcu 6y ago

   Some work on verifying QUIC packet encryption using F* is happening at Microsoft Research: https://github.com/project-everest/everquic-crypto
2. 2.▲
   by catalin_hritcu 9y ago

   One can always look at the empty part of the glass, but the quote does continue with a big full part: "The TLS 1.3 handshake verification is work in progress and still relies on the OCaml extraction mechanism of F* ; thus, the C librar
3. 3.▲
   by catalin_hritcu 9y ago

   Rust is a cool language for safe low-level programming with concurrency, but it is not targeted at program verification. F* can also do safe low-level programming by extraction to C, while also verifying that the code is functionally correc