HACL*: the research repository that tells you to use a different one

The warning at the top is the most important paragraph

The Status section says this directly. It is the research home of HACL*, and anyone looking for documentation, releases, language bindings and code that can be satisfactorily integrated into a production project should check out HACL packages at the cryspen hacl-packages repository.

That sentence redirects the entire evaluation. What remains here is the research artifact: the verification sources, the extracted code, the specifications, the tests and the build machinery that produces the proofs.

The scope is stated next. The repository contains verified code for a library of modern cryptographic algorithms, and the list is concrete: Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC and HKDF. The README notes this set is enough to support the full NaCl API and several TLS 1.3 ciphersuites.

The verification claim is stated with three properties rather than a general promise of correctness. The code is formally verified using the F* verification framework for memory safety, functional correctness, and secret independence, described as resistance to some types of timing side-channels. The qualifier matters: secret independence is a specific property about control flow and memory access patterns not depending on secrets, not a claim that no side channel of any kind exists.

The code is divided into three closely-related sub-projects, all developed as part of Project Everest, and the README states the project is under active development on the `main` branch, which tracks F*'s `master` branch.

Contributions come from students and researchers at INRIA, Microsoft Research and Carnegie Mellon University, with the primary authors of each verified algorithm noted in a corresponding `AUTHORS.md` file, and the contact address is [email protected].

HACL*, ValeCrypt and EverCrypt are three different tools

The three sub-projects differ in what language the proof is written against and what code comes out, and confusing them is the most common way to misread this codebase.

HACL*, in `code/`, is written in a subset of F* called Low* and compiled to C using a compiler called KaRaMeL. The Low* source for each primitive is verified for memory safety, functional correctness and secret independence, and the compiler generates efficient, readable, standalone C that can be integrated into any C project. The current C code for various algorithms is included in the `dist/` directory. HACL* can also be compiled to WebAssembly.

ValeCrypt, in `vale/`, provides formally verified high-performance cryptographic code for selected primitives in assembly language. It relies on the Vale tool to produce both code and proofs in F*, and Vale supports multiple platforms while proving that its implementations are memory safe, functionally correct, and that timing and memory accesses are secret independent.

EverCrypt, in `providers/evercrypt/`, is a high-performance, cross-platform, formally verified cryptographic provider that packages implementations from HACL* and ValeCrypt and automatically picks the fastest one available depending on processor support and the target execution environment. The README calls that multiplexing. It also offers an agile API that makes it simple to switch between algorithms, for example from SHA2 to SHA3.

That last feature is the one with real architectural consequences. An agile API means the algorithm choice becomes a runtime decision, which is good for policy and bad for anything relying on a single fixed implementation, and it is why EverCrypt exists as a separate layer rather than as one more primitive.

The Makefile draws the dependency graph and it is worth reading as a diagram:

            evercrypt
              /  \
          code   vale
          /   \  /
        lib   specs

`evercrypt` sits on top, `code` and `vale` are its two implementation sources, and `lib` and `specs` are shared underneath.

The Makefile is staged because F* needs a two-pass dependency graph

The root Makefile opens with an explanation that tells you why building this is not like building a C library.

It is a staged Makefile because the project first needs to generate `.fst` files out of `.vaf` files in order to have a full dependency graph for the `.fst` files. In other words, the compilation order cannot be known until a first pass has run, which is why the Makefile exposes intermediate targets to the end user.

The targets are named for what they do. `all` is the staged target for the entire build and is the default. `test` is staged. `vale-fst` is the minimum needed to compile `.vaf` files to `.fst` files. `vale-verify` is a properly staged target for re-verifying all the Vale files. `vale-asm` regenerates the Vale assemblies in `dist/vale`. `hacl-verify` is the staged target for verifying HACL* files, made up of `curve25519-verify`, `poly1305-verify`, `chacha20-verify` and `spec-verify`, and `code-verify` is a subset of it with each part staged separately.

Several environment variables change the behaviour, and they are documented because verification runs are expensive. `NOSHORTLOG=1` disables the pretty short logs. `NODEPEND=1` disables `.depend` regeneration, for debugging only. `SKIPDEPEND=1` disables even including `.depend` files, and is stated as not meant for end users. `NOOPENSSLCHECK=1` disables the OpenSSL `libcrypto.a` checks, useful for verifying files only or for non-OpenSSL configurations. `RESOURCEMONITOR=1` creates `.runlim` files with runtime and memory usage information, tallied afterwards with `res_summary.sh`.

Two CI targets exist and they answer the question of what runs on every commit. `ci` is staged, runs all plus test, without short logs, and is described as this repository's CI. `min-test` is staged and runs only a subset of verification for the purposes of F*'s extended CI.

The interactive mode is documented too: to generate a Makefile for it you run `make foo/bar/Makefile`.

Licensing splits the source from the generated C

The License section has three statements and the middle one is unusual.

All the code in the repository is released under an Apache 2.0 license. The generated C code from HACL* is also released under an MIT license. And the README says to contact the maintainers if you have other licensing requirements.

So a consumer has a choice of terms depending on which artefact they take: the verification sources are Apache 2.0, and the C you would actually link is also available under MIT. The dual grant is deliberate and is the sort of thing a hardware or closed-source integrator needs, which is presumably what the contact instruction is for.

The root has `LICENSE`, and the generated output lives in `dist/`, which the README says contains the current C code for various HACL* algorithms. That directory being checked in is the practical consequence of the research-versus-release split: you can read the C without running F*, but you cannot assume it matches the current sources unless you build.

Other root files describe how the project is run rather than what it contains. `GOVERNANCE.md` and `MAINTAINERS.md` cover who decides and who maintains. `SECURITY.md` is the security contact route. `CODE_OF_CONDUCT.md` and `pull_request_template.md` with `PULL_REQUEST.md` are the contribution process. `CHANGES.md` is the changelog.

The build environment is declared three ways: a `flake.nix` for Nix, a `.docker/` directory plus `build_local.sh` for containerised builds, and the Makefile family itself with `Makefile.common`, `Makefile.include`, `Makefile.local` and `Makefile.openssl`. The last of those is notable by its name alone: there is an OpenSSL comparison configuration.

The F* runtime is configured through `Hacl.fst.config.json` and `runtimeconfig.json`, and `hints/` is where verification hints live.

What to cite, and why the 2017 paper is discouraged

The README includes citation guidance, which is unusual and useful, because a wrong citation in a security paper is a real problem.

For HACL* in its current incarnation, including SIMD versions of algorithms, the guidance points to CCS'20, HACLxN: Verified generic SIMD crypto (for all your favourite platforms), by Polubelova, Bhargavan, Protzenko, Beurdouche, Fromherz, Kulatova and Zanella-Béguelin, pages 899 to 918.

For HACL* in general, the guidance points to CCS'17, HACL*: A verified modern cryptographic library by Zinzindohou, Bhargavan, Protzenko and Beurdouche, pages 1789 to 1806, and attaches a parenthetical that says this citation is discouraged since none of that code exists anymore.

That annotation is the most useful sentence in the section. It tells you the library has changed substantially since the original publication, so a paper describing the 2017 design is describing code you cannot obtain from this repository.

Three more citations cover the layers. EverCrypt, the agile multiplexing CPU-detecting API on top of HACL*, is S&P'20 by Protzenko and others, pages 983 to 1002. HACL-WASM, the WebAssembly backend, is S&P'19 by Protzenko, Beurdouche, Merigoux and Bhargavan, pages 1256 to 1274. And the streaming APIs with heap-allocated state and internal buffering, covering hashes and MACs, are ICFP'23, Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification by Ho, Fromherz and Protzenko.

That last entry describes a change in the library's shape: hashes and MACs moved to a streaming interface with internal buffering rather than a single-shot call over the whole message. If you are integrating HACL* you need to know which interface generation you are targeting.

Where HACL* is the wrong place to look

The mismatch is stated at the top of the README and it is absolute: this is a research repository.

If you need a supported dependency, look at hacl-packages. That is where releases, language bindings and production integration live, and reading this repository will not give you either.

If you need to build it, the staged Makefile and the F* toolchain are a real cost. `vale-fst` is a staged operation before the Vale files can be verified, and the verification targets run proof checking rather than compilation, which is a different order of time cost. The existence of `min-test`, a target that runs only a subset of verification for F*'s extended CI, tells you how expensive a full run is.

The algorithm set is also finite. Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC and HKDF is enough for the NaCl API and several TLS 1.3 ciphersuites, and it is not a general-purpose TLS stack. Anything needing RSA, or a signature scheme outside that list, is not here.

The alternative worth weighing is a maintained, packaged cryptographic library with published audits and production support, where the trade is that you are trusting a conventional review process rather than a machine-checked proof. That is a real trade rather than a ranking: verification covers memory safety, functional correctness and secret independence, and it does not by itself certify that the specification matched your threat model or that the API was used correctly. For most production use, the packaged route in hacl-packages is the sensible entry point, and this repository is where you go to understand how it was proved.

One maintenance note for your own tracking: the last push to this repository was on 2026-06-07, while the recent releases listed are OCaml API versions from 2022, so the tagged releases here are not where the current work is.

Editorial conclusion

Read this repository if you want to understand how verified cryptography is built, or if you are working on Project Everest's verification targets. Do not adopt it as a dependency: the README says plainly that this is the research home of HACL*, and anyone looking for documentation, releases, language bindings and code that can be satisfactorily integrated into a production project should use the hacl-packages repository instead. Verify three things before you draw conclusions from the code here: that the `dist/` directory contains the current generated C rather than something stale, since the checked-in C is a build artefact you can read without running the F* toolchain; that the licensing split suits you, because the sources are Apache 2.0 while the generated C from HACL* is also MIT, and the README says to contact the maintainers for other licensing requirements; and that the branch model suits you, since `main` tracks F*'s `master` branch and is where development happens. The last push was on 2026-06-07, and the most recent tagged releases here are OCaml API versions from 2022, which tells you where the packaging attention has gone.

Frequently asked questions

Official sources

1. hacl-star/hacl-star on GitHub
2. Issues
3. License: Apache-2.0
4. README
5. Releases