Short Bio

I am an independent researcher currently based in Portugal. My research interests lie in Cryptography and its intersection with Formal Methods, particularly in the formal verification of cryptographic algorithms.

The curious reader may be thinking what exactly an independent researcher is: as the name suggests, it is someone who does research without being affiliated to any research group or to any unversity. Previously, I was a Computer Scientist at the Computer Science Laboratory (CSL) at SRI International. Before that, I spent 5 years at INESC TEC. Since March 2025, however, I have taken a different path: I founded my own single-person company and set out on the adventure of conducting research independently, without the umbrella of an established institution. The challenges are many, but the freedom to pursue my own research contracts, to work without the weight of company policies and overhead, and to decide my next steps without needing anyone’s approval is truly priceless.

I am open to new collaborations so feel free to reach out if you have a nice idea where you think I would be a good fit!

I hold a Ph.D. in Computer Science from Porto University. In my thesis, entitled “Integrated Verification of Cryptographic Security Proofs and Implementations”, I addressed the gap between provable security and cryptographic practice when applied to the particular scenario of multiparty computation (MPC), contributing with new mechanically verified proofs of cryptographic protocols and also with new techniques that interpolate between cryptographic security and foundational programming languages concepts such as non-interference.

My main research contributions consist of the development of mechanically verified cryptographic proofs using the EasyCrypt framework, a deductive verification tool focused on Cryptography reasoning. I have participated in many projects involving the application of Formal Methods to the development of cryptographic software, ranging from the development of verified implementations of MPC and ZK protocols to the formalization and proof of the AWS Key Management System.