HACL*, Vale and EverCrypt: Project Everest's verified cryptographic library in F* and Vale
================================================================================

HACL* is a library of cryptographic primitives verified in F* for memory safety, functional correctness and secret independence, with Vale providing verified assembly and EverCrypt a unified API. Its code runs in Firefox, the Linux kernel, mbedTLS and WireGuard.

Maintainer: Project Everest (Inria Prosecco, Microsoft Research, CMU)
Website: https://hacl-star.github.io
Category: Verified implementations
Targets: C and assembly primitives, Firefox NSS, Linux kernel, mbedTLS, WireGuard
Approach: Verified C extracted from F* (HACL*) and verified assembly (Vale), unified in EverCrypt
Access: Open source
Status: Maintained; post-quantum work moved to libcrux/hax
Strengths: Broadest deployment of any verified library. | Memory safety, correctness and constant-time in one framework. | Agile multiplexing in EverCrypt.
Limits: Classical primitives; post-quantum lives in libcrux. | F* expertise required to extend. | Extraction toolchain is complex.
Firms using it: none listed
Sources: https://hacl-star.github.io

Source page: https://sorryfree.com/frameworks/hacl-star/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13