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.