Jasmin and libjade: Verified high-speed assembly with constant-time guarantees
==============================================================================

Jasmin 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
Category: Verified implementations
Targets: ML-KEM (incl. AVX2), ML-DSA, X-Wing, Keccak / SHA-3, X25519, x86-64 assembly
Approach: Verified compiler from a low-level language to assembly; correctness proved in EasyCrypt; constant-time checked
Access: Open source
Status: Active (Jasmin 2026.03.2 released July 2026)
Strengths: Strongest end-to-end story: proof to assembly. | Post-quantum coverage. | Performance competitive with hand-written assembly.
Limits: Assembly must be written in Jasmin. | x86-64 focus. | Expertise concentrated in a few groups.
Firms using it: none listed
Sources: https://github.com/jasmin-lang/jasmin | https://github.com/formosa-crypto/libjade | https://formosa-crypto.org

Source page: https://sorryfree.com/frameworks/jasmin/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13