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

More news.

Formosa Tools

  • EasyCryptTool WebsiteTool 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.

  • JasminTool WebsiteTool Repository

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

  • LibjadeTool WebsiteTool 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

More projects.

Formosa People

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.