catalin_hritcu

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* ; thus, the C library still encapsulates the OCaml runtime system.

We have completed verification of the TLS 1.3 record layer it currently extracts to C.

The AES and SHA2 cryptographic assembly routines are verified and extract to assembly via Vale.

HaCl* provides verified C code for multiple other primitives such as Curve25519, Chacha20, Poly1305 or HMAC.

Our test client implements TLS 1.2 + TLS 1.3 Draft 18 and successfully connects to TLS 1.3 test servers. We have a prototype integration of miTLS within libcurl that one can use to git clone a remote repository."

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 correct and secure. That's of course a lot more work, but also a lot stronger than the kind of guarantees one can get informally in rust (e.g. memory safety).