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 …
The High Assurance Crypto Library
HACL is a set of formally verified cryptographic libraries in C, JavaScript, OCaml, and Rust. The libraries are based on the HACL* research project, originally developed by Inria and Microsoft …
A High-Assurance Crypto Library in Rust
Libcrux is a cryptographic library written almost entirely in Rust, a modern programming language that is known for its safety and performance. It provides a wide range of cryptographic primitives, …
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 …
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 …
