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

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.

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.