A High Assurance Cryptographic Library¶
HACL* is a formally verified cryptographic library written in F* and compiled to C, developed as a collaboration between the Prosecco team at INRIA Paris, Microsoft Research, and Carnegie Mellon University. The library, its applications, and the verification tools it relies on are being actively developed and maintained as part of Project Everest.
EverCrypt is a cryptographic provider that into a single library combines HACL*, described above, and ValeCrypt, a collection of verified assembly code for cryptographic primitives. This manual describes the HACL* and EverCrypt APIs. Read HACL*, Vale, and EverCrypt for a detailed description of how they relate to each other.
HACL* is an open source project hosted at hacl-star, along with ValeCrypt and EverCrypt. HACL*, Vale and EverCrypt are distributed together as a collection of C and assembly files. These can be used either as individual components, or as a full-fledged library through the EverCrypt provider.
Code from HACL* has been incorporated into Firefox, the Windows kernel, the Linux kernel, the Tezos blockchain, the Microsoft MSQuic implementation of the QUIC protocol, and the Wireguard VPN. Still, HACL*, Vale, and EverCrypt remain ongoing research projects and should be treated as such. If you want to integrate this code into a production environment, or if you have any questions, comments, or feature requests for HACL*, Vale, or EverCrypt, initiate a conversation with the HACL* maintainers
- HACL*, Vale, and EverCrypt
- List of supported algorithms
- Underlying research
- Using the crypto library
- Digging into the F* source code
- HACL APIs
- EverCrypt APIs
- Which API to use
- Verified Applications