Cryspen
Direct answerCryspen 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
Frameworks this firm builds or uses
Public evidence
Best fit
Choose Cryspen for Rust cryptographic libraries, particularly post-quantum, and insist on a written verification boundary.
Other firms on this index
zkSecurity, Galois, Veridise, Nethermind (Formal Verification team), Formal Land, Reilabs, Runtime Verification, Certora, Trail of Bits, Symbolic Software