My research concerns the design and implementation of new program verification techniques that would enable formal analyses of real-world security applications. My recent work focuses on using dependent type systems, such as F*. to investigate the (in)security of cryptographic protocols, such as TLS, and to build verified cryptographic libraries, such as HACL*.