Jasmin and libjade
Direct answerJasmin is a language and verified compiler for writing cryptographic assembly whose functional correctness is proved in EasyCrypt and whose constant-time behaviour is checked by the compiler. libjade is the resulting library of verified implementations, including ML-KEM with AVX2 rejection sampling, ML-DSA, X-Wing, SHA-3 and X25519.
- Maintainer
- Formosa Crypto
- Website
- https://github.com/jasmin-lang/jasmin
- Repository
- https://github.com/formosa-crypto/libjade
- Category
- Verified implementations
- Targets
- ML-KEM (incl. AVX2)ML-DSAX-WingKeccak / SHA-3X25519x86-64 assembly
- Approach
- Verified compiler from a low-level language to assembly; correctness proved in EasyCrypt; constant-time checked
- Access
- Open source
- Status (2026-09-13)
- Active (Jasmin 2026.03.2 released July 2026)
What Jasmin and libjade does
Jasmin is the only pipeline where the security proof (EasyCrypt), the functional spec and the shipped assembly are all connected by machine-checked steps. The mlkem-libjade AVX2 work was published at IEEE S&P 2025.
Where it is strong
- Strongest end-to-end story: proof to assembly.
- Post-quantum coverage.
- Performance competitive with hand-written assembly.
Limits and caveats
- Assembly must be written in Jasmin.
- x86-64 focus.
- Expertise concentrated in a few groups.
When to choose it
Choose Jasmin/libjade when you ship a primitive and want the verified implementation itself, not a proof about someone else's code.
Who works with Jasmin and libjade
No firm on this index lists Jasmin and libjade as a core tool yet; the firms below cover the same problem class.
Top-listed for implementation verification work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Related frameworks in Verified implementations
hax, Cryptol and SAW, Fiat-Crypto, HACL*, Vale and EverCrypt, Aeneas, Kani, CBMC, CryptoLine, Verus.