• EasyCrypt — Tool Website — Git 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 — Git 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 — Git 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.