Bertie is a minimal, high-assurance implementation of TLS 1.3 written in a subset of Rust called hacspec. It is built upon the following design principles: Purely functional: no mutable data structures or externally visible side-effects. Verification friendly: written in hacspec and translates to F*. Succinct and minimal: configured with a single protocol version and cipher suite. Karthikeyan Bhargavan first authored Bertie at Inria in 2021 and transferred it to Cryspen in 2022. It is licensed u...