The Formosa Crypto project federates multiple projects in machine-checked cryptography and high-assurance cryptographic engineering under a single banner, to better support developers and users.

Join us on Zulip.

Formosa News

• Release 2025.06.2 of the Jasmin compiler (November 20, 2025)
  

  A new minor version of Jasmin is available. Read the announcement.

• Jazzline wins a Distinguished Paper Award at CCS 2025! (November 19, 2025)
  

  The paper, “Jazzline: Composable CryptoLine functional correctness proofs for Jasmin programs”, is the recipient of a Distinguished Paper Award at CCS 2025 in Taiwan. Learn more.

• Formosa Retreat in Porto (November 19, 2025)
  

  The next Formosa research retreat will take place in Porto in the week of November 24–28. Learn more.

• Debian packages for Jasmin & EasyCrypt (September 11, 2025)
  

  Debian packages for Bookworm and Trixie are available Read the annoncement.

• Release 2025.06.1 of the Jasmin compiler (August 29, 2025)
  

  A new minor version of Jasmin is available. Read the announcement.

More news.

Formosa Tools

• EasyCrypt — Tool Website — Tool Repository
  

  EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs.

• Jasmin — Tool Website — Tool Repository
  

  Jasmin is a workbench for high-assurance and high-speed cryptography. Jasmin implementations aim at being efficient, safe, correct, and secure.

• Libjade — Tool Website — Tool Repository
  

  Libjade is a cryptographic library written in jasmin, with computer-verified proof of correctness and security in EasyCrypt. The primary focus of libjade is to offer high-assurance software implementations of post-quantum crypto primitives. The implementations available in this tool are listed and detailed in the Formosa Projects page.

Formosa Projects

• Formosa 25519 — Project Repository
  Formosa 25519 is a formally verified implementation of X25519.

• Formosa Keccak — Project Repository
  Formosa Keccak is a formally verified implementation of Keccak and related functions (SHA3, SHAKE, etc.).

• Formosa ML-DSA — Project Repository
  Formosa ML-DSA is a formally verified implementation of ML-DSA.

• Formosa ML-KEM — Project Repository
  Formosa ML-KEM is a formally verified implementation of ML-KEM.

• Formosa X-Wing — Project Repository
  Formosa X-Wing is a formally verified implementation of X-Wing hybrid KEM.

More projects.

Formosa People

• Aaron Kaiser (Max Planck Institute for Security and Privacy)

• Adrien Koutsos (Inria, centre de Paris)

• Alley Stoughton (Boston University)

• Andreas Hülsing (Eindhoven University of Technology)

• Bas Westerbaan (Cloudflare)

• Basavesh Ammanaghatta Shivakumar (Virginia Tech)

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

• Chitchanok Chuengsatiansup (The University of Melbourne, Australia)

• Deirdre Connolly (SandboxAQ)

• Denis Firsov (Input Output & Taltech)

• Fabio Campos (Hochschule Darmstadt)

• François Dupressoir (University of Bristol)

• Gaëtan Cassiers (CryptoExperts and UCLouvain)

• Gilles Barthe (Max Planck Institute for Security and Privacy & IMDEA Software Institute)

• Gustavo Delerue (Universidade do Porto)

• Henrique Faria (Universidade do Minho & INESC TEC)

• Hugo Pacheco (Universidade do Porto & INESC TEC)

• Jean-Christophe Léchenet (Inria, centre d’Université Côte d’Azur)

• José Bacelar Almeida (Universidade do Minho & HASLab/INESC TEC)

• João Diogo Duarte (Universidade do Porto & INESC TEC)

• Karolin Varner (Max Planck Institute for Security and Privacy & Rosenpass e.V.)

• Lionel Blatter (Max Planck Institute for Security and Privacy)

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

• Manuel Barbosa (Universidade do Porto & HASLab/INESC TEC)

• Matthias Meijers (Eindhoven University of Technology (TU/e))

• Miguel Quaresma (Max Planck Institute for Security and Privacy)

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

• Pierre-Yves Strub (PQShield)

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

• Santiago Arranz Olmos (Max Planck Institute for Security and Privacy)

• Swarn Priya (Virginia Tech)

• Tiago Oliveira (SandboxAQ)

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

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

• Yuval Yarom (Ruhr University Bochum)

Formosa Affiliations and Supporters

Formosa and its component projects are supported by a variety of funders and institutions. Our active members work for the following institutions.

In addition, other institutions support, and have supported Formosa or its constituent projects financially. We gratefully acknowledge their support.