HACL Packages

HACL packages is a collection of cryptographic libraries developed by Cryspen on top of HACL*. It contains a portable C crypto library as well as Rust, OCaml, and JavaScript bindings.

Get Started on Github


hacspec is a language for writing succinct, executable, formal specifications for cryptographic components embedded in Rust.

hacspec is used at Cryspen to specify and prototype cryptographic components that can later be replaced with verified implementations.


HPKE (RFC 9180) describes a scheme for hybrid public key encryption. It is co-authored by Cryspen co-founder Karthikeyan Bhargavan.

Cryspen provides reference and production implementations of the standard.

Read our blog post for more details:


OpenMLS is a software library that implements the MLS protocol and can serves as a building block in applications that require end-to-end encryption.

Cryspen provides services for using MLS and uses OpenMLS to build zero trust applications. OpenMLS is maintained and developed at Cryspen and our partners at Phnx.


Cryspen collaborates with the Prosecco team at Inria to develop a usable, robust, development environment and verification toolchain for security critical software.

Want to know more?

Get in touch with us.