Benjamin Beurdouche is a last year PhD candidate in the Prosecco team at INRIA and ENS Paris. He is working on formal verification of security protocols and cryptographic primitives such as the HACL* cryptographic library used in Mozilla Firefox and Microsoft Windows. Benjamin is one of the co-authors of IETF's Messaging Layer Security (MLS) protocol and one among many contributors to the TLS 1.3 protocol.