Cryspen: formal verification services for cryptography and ZK
=============================================================

Cryspen builds hax, the Rust-to-proof-assistant translator, and libcrux, whose verified ML-KEM and ML-DSA ship in Mozilla and Signal. It is developing hax's Lean backend under an Ethereum Foundation grant and offers verification-driven reviews. The 2026 Verification Theatre paper documenting bugs outside libcrux's verified boundary is essential context for scoping its engagements.

Website: https://cryspen.com
Headquarters: Berlin, Germany and Paris, France
Focus: hax and libcrux: verified Rust post-quantum implementations; hax Lean backend for the Verified zkEVM program
Index position: #6 of 11
Services: Verified Rust implementations of classical and post-quantum primitives | Protocol verification (Signal PQXDH, MLS) | hax-based verification of client Rust code
Tools: hax, F*, ProVerif, SSProve
Evidence: https://github.com/cryspen/hax | https://cryspen.com/post/ml-kem-verification/

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