HACL

/images/hero.png
The strengths and limits of formal verification

Getting precise about the guarantees of formal verification in our open-source libraries.

I have learned that it is important to be precise when documenting the guarantees offered by formally verified code, and to resist the temptation of simplifying things too much in trying to reach a …

/images/posts/hacl-0_6.jpeg
HACL Packages v0.6

The first release of the HACL Packages, bundling the HACL C library and updated hacl-star OCaml bindings with new documentation.

Today, we announce the first release of the HACL Packages libraries. 🎉 This release of HACL packages includes the first release of the HACL C library and a new release of the hacl-star OCaml …

/images/posts/boxes.jpg
HACL Packages

A user-friendly high-assurance cryptographic library

Earlier this year, Tezos and Nomadic Labs started to work with Cryspen to improve HACL* and ensure that it is a viable long-term solution for Tezos' cryptographic needs. HACL is a set of high …