Current members

  • Aaron Kaiser (Max Planck Institute for Security and Privacy)
    Tools: EasyCrypt, Jasmin, Libjade
    Projects: Formosa X-Wing

  • Adrien Koutsos (Inria, centre de Paris)
    Tools: EasyCrypt, Jasmin

  • Alley Stoughton (Boston University)
    About: Alley is a contributor to and user of EasyCrypt. Her current projects include mechanizing proofs of Universally Composable (UC) security in EasyCrypt and formalizing algorithmic bounds using EasyCrypt.
    Tools: EasyCrypt

  • Andreas Hülsing (Eindhoven University of Technology)
    Tools: EasyCrypt

  • Bas Westerbaan (Cloudflare)
    About: Bas is one of the co-authors of, X-Wing, a concrete, simple and IND-CCA secure hybrid KEM based on X25519 and ML-KEM.

  • Basavesh Ammanaghatta Shivakumar (Virginia Tech)
    Tools: Jasmin

  • Benjamin Grégoire (Inria, centre d’Université Côte d’Azur)
    Tools: EasyCrypt, Jasmin

  • Chitchanok Chuengsatiansup (The University of Melbourne, Australia)
    Tools: Jasmin

  • Deirdre Connolly (SandboxAQ)
    About: Deirdre is one of the co-authors of, X-Wing, a concrete, simple and IND-CCA secure hybrid KEM based on X25519 and ML-KEM.

  • Denis Firsov (Input Output & Taltech)
    Tools: EasyCrypt, Jasmin

  • Fabio Campos (Hochschule Darmstadt)
    Tools: Jasmin, Libjade

  • François Dupressoir (University of Bristol)
    About: François is a core member of the EasyCrypt team. His work focuses on developing libraries of ready-to-use proof blocks and constructions that ease the development of machine-checked cryptographic proofs of all scales and intricacies, from primitives to protocols.
    Tools: EasyCrypt

  • Gaëtan Cassiers (CryptoExperts and UCLouvain)
    About: Gaëtan works on the formal verification of cryptographic implementations that employ side-channel countermeasures such as masking, using Jasmin and Easycrypt.
    Tools: Jasmin

  • Gilles Barthe (Max Planck Institute for Security and Privacy & IMDEA Software Institute)
    Tools: EasyCrypt, Jasmin

  • Gustavo Delerue (Universidade do Porto)
    Tools: Easycrypt

  • Henrique Faria (Universidade do Minho & INESC TEC)
    Tools: Easycrypt, Jasmin

  • Hugo Pacheco (Universidade do Porto & INESC TEC)
    Tools: Easycrypt

  • Jean-Christophe Léchenet (Inria, centre d’Université Côte d’Azur)
    About: Jean-Christophe is an active developer and maintainer of Jasmin, trying to enhance the language and the compiler in order to make the task of writing Jasmin programs easier.
    Tools: Jasmin

  • José Bacelar Almeida (Universidade do Minho & HASLab/INESC TEC)
    Tools: Jasmin, Libjade

  • João Diogo Duarte (Universidade do Porto & INESC TEC)
    About: João is a PhD student under the supervision of Professor Manuel Barbosa. He is one of the co-authors of X-Wing, co-wrote various Jasmin implementations of cryptographic algorithms, and has produced various formal correction proofs in EasyCrypt - most notably for the Jasmin implementation of Curve25519. Some experience in Cryptoline and OCaml.
    Tools: Easycrypt, Jasmin, Libjade
    Projects: Formosa X-Wing, Formosa 25519, Formosa ML-KEM

  • Karolin Varner (Max Planck Institute for Security and Privacy & Rosenpass e.V.)
    About: Karolin is one of the co-authors of, X-Wing, a concrete, simple and IND-CCA secure hybrid KEM based on X25519 and ML-KEM.

  • Lionel Blatter (Max Planck Institute for Security and Privacy)
    Tools: EasyCrypt, Jasmin

  • Luís Esquível (Universidade of Porto & INESC TEC)
    Tools: Libjade

  • Manuel Barbosa (Universidade do Porto & HASLab/INESC TEC)
    Tools: EasyCrypt, Jasmin, Libjade

  • Matthias Meijers (Eindhoven University of Technology (TU/e))
    About: Matthias is an EasyCrypt user first and a ‘contributor’ second. He primarily focuses on the formal verification of (post-quantum) cryptography, while always staying on the lookout for opportunities to improve and extend the tool. Additionally, he strives to enhance the tool’s usability and accessibility for the ‘average’ cryptographer, particularly by working on tutorial material and documentation (tooling).
    Tools: EasyCrypt

  • Miguel Quaresma (Max Planck Institute for Security and Privacy)
    Tools: EasyCrypt, Jasmin, Libjade

  • Peter Schwabe (Max Planck Institute for Security and Privacy & Radboud University)
    Tools: Libjade

  • Pierre-Yves Strub (PQShield)
    Tools: EasyCrypt, Jasmin

  • Rui Fernandes (Max Planck Institute for Security and Privacy)
    Tools: Libjade

  • Santiago Arranz Olmos (Max Planck Institute for Security and Privacy)
    About: Santiago is a PhD student at MPI-SP working on the Jasmin framework. Currently, his work focuses on the detection and mitigation of side-channel vulnerabilities as well as Spectre.
    Tools: Jasmin

  • Swarn Priya (Virginia Tech)
    Tools: Jasmin

  • Tiago Oliveira (SandboxAQ)
    Tools: Libjade

  • Vincent Hwang (Max Planck Institute for Security and Privacy)
    Tools: Libjade

  • Vincent Laporte (Inria, centre de l’Université de Lorraine)
    Tools: Jasmin

  • Yuval Yarom (Ruhr University Bochum)
    Tools: Jasmin

Former members

  • Christian Doczkal (Max Planck Institute for Security and Privacy)
    About: From Christian’s website: “I contributed to the mechanization of the security proof of Dilithium, a Round 3 candidate for the NIST post-quantum cryptography project.”
    Projects: EasyCrypt

  • Julian Wälde (Hochschule RheinMain)
    Tools: Jasmin, Libjade

  • Kai-Chun Ning (Max Planck Institute for Security and Privacy)
    Tools: Jasmin

  • Marc Stoettinger (Hochschule RheinMain)
    Tools: Jasmin, Libjade

  • Pierre Boutry (Inria, centre d’Université Côte d’Azur)
    About: From Pierre’s website: “I worked on building a formally verified model of Curve25519, which led to the ongoing effort of developing a field extension library for EasyCrypt.”
    Tools: EasyCrypt