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*, ValeCrypt and EverCrypt is deployed in several production systems, including Mozilla Firefox's NSS, the Linux kernel, mbedTLS, the Tezos blockchain, the ElectionGuard Electronic Voting SDK, 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
