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

• libjade release 2022.12.0 (December 5, 2022)
  

  The first version of libjade is available. Read the announcement.

• Jasmin release 2022.09.0 (October 3, 2022)
  

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

• Jasmin lecture in Nancy (July 7, 2022)
  

  During the Cyber in Nancy summer school, Vincent Laporte and Benjamin Grégoire gave a lecture on Jasmin.

• Jasmin compiler in the opam repository (June 28, 2022)
  

  The Jasmin compiler can be installed using the opam package manager. Learn how.

• EasyCrypt and Jasmin tutorial in Šibenik (June 7, 2022)
  

  Manuel Barbosa will be giving a tutorial on machine-checked cryptography in EasyCrypt and Jasmin at the Summer School on Real-World Crypto and Privacy in Šibenik, Croatia, on June 16th. More details and links to material.

• Jasmin release 2022.04.0 (May 6, 2022)
  

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

Formosa Projects

• EasyCrypt — Project Website — Project 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 — Project Website — Project Repository
  

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

• Libjade — Project Website — Project 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.

Formosa People

• Adrien Koutsos (Inria Paris)

• Alley Stoughton (Boston University)

• Andreas Hülsing (Eindhoven University of Technology)

• Basavesh Ammanaghatta Shivakumar (Max Planck Institute for Security and Privacy)

• Benjamin Grégoire (Inria Sophia-Antipolis Méditerranée)

• François Dupressoir (University of Bristol)

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

• Jean-Christophe Léchenet (Inria Sophia-Antipolis Méditerranée)

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

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

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

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

• Pierre-Yves Strub (Meta)

• Tiago Oliveira (Max Planck Institute for Security and Privacy)

• Vincent Laporte (Inria)

Formosa Supporters

Formosa and its component projects are supported by a variety of funders and institutions. We gratefully acknowledge their support, including historical support for the founding projects.