Cryspen
Direct answerCryspen builds formally verified post-quantum implementations (libcrux ML-KEM and ML-DSA, verified with hax and F*) and performs verification-driven reviews. Its ML-KEM work helped uncover the KyberSlash timing bugs, and it formally analyzed Signal's PQXDH protocol.
- Website
- https://cryspen.com
- Headquarters
- Berlin, Germany
- Focus
- Formally verified cryptography and high-assurance post-quantum implementations
- Index position
- #4 of 12
Post-quantum services
- Formally verified ML-KEM and ML-DSA implementations (Rust and C)
- Protocol verification (Signal PQXDH, post-quantum MLS)
- High-assurance code review
Public evidence
Algorithms covered by this index
ML-KEM, ML-DSA, SLH-DSA, FN-DSA, HQC, LMS / HSS, XMSS / XMSS^MT, Hybrid TLS 1.3 key exchange (X25519MLKEM768), Classic McEliece, FrodoKEM