Cătălin Hrițcu is a tenured faculty member and head of the Formally Verified Security group at the new Max Planck Institute for Security and Privacy (MPI-SP) in Bochum, Germany. He is particularly interested in formal methods for security (secure compilation, compartmentalization, memory safety, security protocols, information flow), programming languages (program verification, proof assistants, dependent types, formal semantics, mechanized metatheory, property-based testing), and the design and verification of security-critical systems (reference monitors, secure compilation chains, tagged architectures). He was awarded an ERC Starting Grant on formally secure compilation, and is also actively involved in the design of the F* verification system, which is used for building a formally verified HTTPS stack. Catalin received a PhD from Saarland University, a Habilitation from ENS Paris, and was previously also a Tenured Researcher at Inria Paris, a Postdoctoral Research Associate at University of Pennsylvania, and a Visiting Researcher at Microsoft Research Redmond.