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 assurance cryptographic primitives used by Tezos for most of its cryptography.
The original HACL* has been developed as part of Project Everest and is a collection of high-assurance cryptographic algorithms. Its source is written in F*, which is used to generate C code. It also contains verified assembly code from the Vale project and an agile multiplexed cryptographic provider called EverCrypt.
To increase the usability and performance of the library, Cryspen is also in the process of improving some algorithms, adding more usable APIs, and writing documentation.
We reached the first milestone for the HACL transition by providing a library that is easy to build and use on all major platforms and operating systems.
If you use cryptography anywhere, we’d be happy if you used HACL and told us if it’s working for you or (why) not.
Please get in touch if you have any questions about high assurance cryptography or the HACL library in particular.