[profquail]

Have you considered implementing any parts of this in F* (so they can be verified) and extracting back to C, as is being done for TLS?

https://project-everest.github.io/

[catalin_hritcu]

Some work on verifying QUIC packet encryption using F* is happening at Microsoft Research: https://github.com/project-everest/everquic-crypto

[protz]

Just to build on Catalin's answer. We are actively working on an implementation of QUIC's transport layer (i.e. packet encryption and decryption), along with a proof of cryptographic security. This is what Catalin linked to (https://github.com/project-everest/everquic-crypto). EverQuic-Crypto builds upon two previous projects: EverParse, a library of verified low-level parsers and serializers which we apply to the QUIC network formats, and EverCrypt, a cryptographic provider with agility and multiplexing, which we use for all the cryptography, e.g. packet number encryption, AEAD, etc.

This is not yet a full QUIC implementation, but we have plans for extending this codebase to cover more of the QUIC protocol.

[nibanks]

We do work with the Everest team. We have unofficial support on top of miTLS (which they produce). We haven't looked into actually using F* for any of the QUIC code though.