Formosa Crypto
NewsPeopleToolsProjectsPublicationsFormosa Supporters

Projects

  • Crypto-specs — Git Repository - EasyCrypt specifications of cryptographic primitives.

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

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

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

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

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

  • Libjbn — Git Repository - BigNums library for jasmin with functional correctness proofs written in Easycrypt.

  • The Formosa team
  • team@formosa-crypto.org

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