Some work on verifying QUIC packet encryption using F* is happening at Microsoft Research: https://github.com/project-everest/everquic-crypto
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* ;…
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…
Some work on verifying QUIC packet encryption using F* is happening at Microsoft Research: https://github.com/project-everest/everquic-crypto
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* ;…
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…