Projects

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

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

• Formosa Keccak — 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.