I’m a Ph.D. candidate at MPI-SP, Bochum, Germany working with Cătălin Hriţcu. My research focuses on building the first secure compiler for verified code, by developing a secure compiler from the proof-oriented programming language F^* to OCaml. Existing (insecure) compilers erase all the annotations with which the code was verified, thus, making the resulting compiled code vulnerable when linked against adversarial code.