Hacspec

libcrux

The Formally Verified Crypto Library

Libcrux is a formally verified cryptographic library that brings together verified artifacts from different sources. It uses hacspec as a common language for the specifications underlying the …
/images/posts/hpke_spec.png
An Executable HPKE Specification

HPKE, published as RFC 9180, describes a scheme for hybrid public key encryption. 📚 Read our TL;DR on HPKE if you need more background on HPKE.