Cryspen: post-quantum cryptography audit services
=================================================

Cryspen 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
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
Evidence: https://cryspen.com/post/ml-kem-implementation/ | https://cryspen.com/post/fospqc/

Source page: https://pqaudit.org/auditors/cryspen/
Compiled by: PQC Audit Index editors (https://pqaudit.org/about/)
Last reviewed: 2026-09-12