Deploy HACL* to Europe — Karthikeyan Bhargavan 🇫🇷 (INRIA Paris), the Formally Verified Cryptographic Library Running in Firefox, Linux, and Signal, on EU Infrastructure in 2026

Cryptographic implementations fail in two distinct ways. The first is algorithmic: the protocol design is broken — a distinguishing attack, a key-recovery attack, a replay. This failure mode is addressed by formal protocol verification tools like ProVerif and CryptoVerif. The second is implementational: the algorithm is correct but the C code is wrong — buffer overflows, timing side-channels that leak secret key bits, integer underflows, undefined behaviour. History is full of implementation bugs in cryptography: the original OpenSSL's RSA side-channel, the Lucky 13 padding oracle against CBC-mode TLS, the various Heartbleed-class memory errors. ECC implementations that branched on secret key bits, leaking them through timing to an adversary on the same physical machine.

HACL* (High-Assurance Cryptographic Library) closes both failure modes simultaneously. It is a production cryptographic library written in F*, a dependently typed language developed by INRIA Paris and Microsoft Research, where every implementation is formally verified to be:

1. Functionally correct against a mathematical specification (the algorithm does what it claims)
2. Memory safe (no out-of-bounds accesses, no use-after-free, no undefined behaviour)
3. Constant-time (no secret-dependent branches or memory indices — timing attacks provably impossible)
4. Cryptographically secure via EasyCrypt proofs (resistance against IND-CCA2, PRF distinguishers, CDH/DDH)

The result ships in Mozilla Firefox (since 2017), the Linux kernel (WireGuard crypto module since 5.10), and Signal Protocol — three of the most security-critical software deployments on the planet, collectively running on hundreds of millions of devices daily.

Jean-Karim Zinzindohoué 🇫🇷 and Karthikeyan Bhargavan 🇫🇷 presented HACL* at CCS 2017 as "HACL*: A Verified Modern Cryptographic Library", co-authored with Jonathan Protzenko, Benjamin Grégoire 🇫🇷 (INRIA Sophia Antipolis), and six further INRIA / Microsoft Research co-authors.

The F* Language and Low*

HACL* is written in F* (F-star), a verification-oriented functional language developed jointly by INRIA Paris (Bhargavan, the Prosecco/Cascade group) and Microsoft Research Cambridge (Cédric Fournet, Nikhil Swamy).

F* is a dependently typed lambda calculus with:

• Refinement types: x:int{x >= 0} — the type carries the proof that x is non-negative
• Hoare logic via Dijkstra Monads: pre/post-conditions on effectful computations, compiled to verification conditions discharged by Z3
• Effect system: Tot (total pure functions), ST (stateful), Lemma (proof obligations) — effect labels propagate through types
• Higher-order SMT automation: F* computes verification conditions symbolically and discharges them via Z3, falling back to manual proofs for arithmetic that Z3 cannot handle automatically

HACL* uses Low* (Low-star), a subset of F* designed for C extraction. Low* restricts F* to a stack-and-heap memory model that corresponds directly to C — no garbage collection, explicit stack buffers, manual memory management. The KreMlin compiler (also INRIA) translates verified Low* code to readable C that GCC/Clang can compile for any target.

The verification pipeline:

F* source (with EasyCrypt security proof imported)
    │
    ▼
F* type checker
    │ VCs → Z3 / SMT solver
    ▼
Low* subset: verified functional correctness + memory safety
    │
    ▼
KreMlin → C code (HACL_Chacha20.c, HACL_Poly1305.c, ...)
    │
    ▼
GCC/Clang → Linux kernel / Firefox NSS / libsignal

For the assembly-level constant-time primitives, HACL* uses Jasmin (CCS 2017, Almeida+Barbosa+Barthe+Grégoire) — an assembly-like language with a machine-checked constant-time type system. Jasmin implementations are separately verified for CT properties and then integrated into HACL*.

What Is Verified and How

HACL* covers all major symmetric, hash, MAC, and key-agreement primitives:

ChaCha20-Poly1305 (RFC 8439)

The primary AEAD construction in modern TLS 1.3 and QUIC. ChaCha20 is a stream cipher based on a quarter-round permutation:

// F* functional specification (simplified)
let chacha20_quarter_round (a b c d: uint32) : (uint32 & uint32 & uint32 & uint32) =
  let a = a +. b in let d = d ^. a in let d = d <<<. 16ul in
  let c = c +. d in let b = b ^. c in let b = b <<<. 12ul in
  let a = a +. b in let d = d ^. a in let d = d <<<.  8ul in
  let c = c +. d in let b = b ^. c in let b = b <<<.  7ul in
  (a, b, c, d)

The F* proof establishes: the Low* implementation of ChaCha20 refines this specification — for all keys k, nonces n, and plaintexts m, the C implementation produces exactly the same keystream as the mathematical spec. The proof covers the 20-round double-round structure, the counter increment, and the final output mixing. Poly1305 is proved EUF-CMA (existentially unforgeable under chosen message attack) in EasyCrypt, and the F* Low* implementation is proved to match the EasyCrypt specification.

Curve25519 / X25519 (RFC 7748)

Elliptic-curve Diffie-Hellman on Curve25519 — the dominant key exchange in TLS 1.3, Signal X3DH, and WireGuard. The mathematical core is scalar multiplication on the Montgomery curve y² = x³ + 486662x² + x over 𝔽_{2²⁵⁵⁻¹₉}.

HACL* implements X25519 using the Montgomery ladder — a constant-time scalar multiplication algorithm where both branches of the conditional step do identical work, making it immune to simple timing side-channels. The F* proof:

1. Establishes functional correctness against a group-theoretic spec
2. Proves the Low* implementation is memory safe (no buffer overruns in the 255-bit field arithmetic)
3. The Jasmin implementation proves constant-time at the x86-64 instruction level — no secret-dependent conditional branches, no variable-time integer multiplications

Ed25519 (RFC 8032)

Edwards-curve digital signatures. The signing key is a 32-byte scalar; the verification key is a point on the twisted Edwards curve −x² + y² = 1 − (121665/121666)x²y² over 𝔽_{2²⁵⁵⁻¹₉}. HACL* proves: every valid signature verifies, and no adversary without the private key can produce a valid signature (EUF-CMA in the random oracle model).

SHA-3 / Keccak and SHA-2

SHA-3 (FIPS 202, Keccak by Daemen+Rijmen+Van Assche 🇧🇪) verified to match the NIST specification bitwise. SHA-256/384/512 verified similarly. These serve as building blocks for HMAC and HKDF (RFC 5869).

ML-KEM / Kyber (FIPS 203)

Post-quantum key encapsulation. The HACL* team, in collaboration with Bhargavan + Grégoire (EasyCrypt ML-KEM IEEE SP 2023), verified:

• The ML-KEM abstract specification in EasyCrypt (IND-CCA2 under MLWE assumption)
• The F*/Low* concrete implementation matches the EasyCrypt spec
• Jasmin implementations of NTT (Number Theoretic Transform) with AVX2 intrinsics, constant-time

The Jasmin ML-KEM NTT is the fastest verified ML-KEM implementation in existence — competitive with hand-optimised assembly while being machine-verified for both correctness and constant-time.

Production Deployments

Mozilla Firefox (since 2017)

Firefox NSS integrates HACL* for:

• ChaCha20-Poly1305: AEAD for TLS 1.3 and DTLS
• SHA-3/Keccak: hash function
• Curve25519: X25519 key exchange in TLS 1.3
• Ed25519: certificate signatures
• BLAKE2b: internal hash for certificate transparency

This was the first major browser to ship a formally verified cryptographic implementation. Every Firefox user's TLS handshake has been protected by machine-verified constant-time Curve25519 since 2017.

Linux Kernel 5.10+ (2020)

WireGuard VPN merged into the Linux kernel in 5.6 (2020). Its cryptographic core is drawn from HACL*:

• ChaCha20-Poly1305: the sole data encryption AEAD (no negotiation, no downgrade attacks)
• Poly1305: MAC, with an AVX2 Jasmin implementation merged into arch/x86/crypto/poly1305_glue.c
• Curve25519: the static and ephemeral key exchange in the Noise_IKpsk2 handshake

The Linux kernel crypto tree now maintains Poly1305 and Curve25519 implementations derived from Jasmin verified sources. Every Linux server running WireGuard uses HACL*-derived verified crypto.

Signal Protocol (libsignal)

Signal Protocol uses HACL* via:

• Ed25519: identity keys and signed prekeys
• X25519: Diffie-Hellman in X3DH (Extended Triple Diffie-Hellman)
• SHA-256/HMAC-SHA-256: HKDF for key derivation in Double Ratchet
• BLAKE2b: fast hash for internal operations

The Signal app on iOS, Android, and desktop — and all apps that license Signal Protocol (WhatsApp, Google Messages in RCS mode) — run HACL*-verified key agreement and signature operations.

Project Everest and miTLS

Project Everest (MSR Cambridge + INRIA Paris + MSR Research) built a fully verified HTTPS stack:

• miTLS: TLS 1.2 and TLS 1.3 reference implementation in F*, with formal security proofs
• QUIC*: verified QUIC implementation
• HACL* supplies all cryptographic primitives, connecting the protocol-level F* proofs to verified implementations

The Full Verification Stack

HACL* sits at the apex of the INRIA verification stack that has been covered across this blog series:

The chain is complete: a CryptoVerif proof that ChaCha20-Poly1305 is IND-CCA2 → an EasyCrypt proof of the underlying PRF/UF-CMA → an F* proof that the Low* implementation matches the spec → a Jasmin proof that the x86-64 assembly is constant-time → KreMlin C extraction → Firefox.

EU Provenance

HACL* is a 100% EU and EEA research product:

Funding: ANR France + ERC Advanced Grant (Horizon Europe) + FCT Portugal.

Regulatory and Compliance Relevance

BSI TR-02102 🇩🇪 (TLS/IPSec/QUIC): HACL*'s ChaCha20-Poly1305, Curve25519, and ML-KEM implementations provide machine-verified compliance artefacts for BSI's TLS 1.3 algorithm mandate. The Jasmin constant-time proofs directly address BSI's requirement for side-channel-resistant implementations.

ANSSI 🇫🇷 (CSPN / PQC migration): ANSSI's PQC roadmap cites the INRIA/IMDEA ecosystem. HACL* ML-KEM Jasmin implementation + EasyCrypt proofs constitute highest-assurance ANSSI evidence for ML-KEM migration. ANSSI funded CryptoVerif, ProVerif, and EasyCrypt — HACL* is the implementation layer of this ANSSI-funded stack.

NIS2 Art. 21(2)(h) — "appropriate cryptographic measures": Formally verified constant-time implementations exceed pen-and-paper assurance for operators of essential services. Memory-safety proofs eliminate a class of cryptographic implementation attacks (Heartbleed-class). The F* machine-checked proofs constitute auditable NIS2 technical documentation.

CRA 2027 — "state of the art" security: CWE-208 (observable timing discrepancy) + CWE-385 (covert timing channel) formally eliminated by Jasmin CT certificates. CWE-119/121/122 (buffer overflows) formally eliminated by F*/Low* memory-safety proofs. HACL* provides CRA-compliant "state of the art" evidence for cryptographic components at the highest possible assurance level.

EU AI Act Art. 9 — risk management for high-risk AI: Cryptographic authentication and integrity components in high-risk AI systems (biometric systems, critical infrastructure AI) verified for correctness and side-channel resistance.

FIPS 140-3 (CMVP): Project Everest is pursuing FIPS 140-3 module validation using HACL* implementations. NSA Suite B algorithm requirements (P-256, SHA-256, AES-GCM, ECDSA) have F*/Low* formal verification from the HACL* team.

Deploying HACL* on sota.io

HACL* is a C library produced by KreMlin extraction from verified F* Low* source. You can use it as a dependency in any C, Rust, or Python project. The most common deployment pattern is via libsodium (which includes HACL* primitives for Curve25519 and Poly1305) or directly via the hacl-packages distribution.

# Dockerfile for a service using HACL* via hacl-packages
FROM debian:bookworm-slim

RUN apt-get update && apt-get install -y \
    cmake ninja-build gcc libssl-dev \
    && rm -rf /var/lib/apt/lists/*

# Build HACL* from source (KreMlin-extracted C)
RUN git clone --depth 1 https://github.com/hacl-star/hacl-star /opt/hacl-star
WORKDIR /opt/hacl-star/dist/karamel
RUN cmake -B build -G Ninja && cmake --build build

COPY . /app
WORKDIR /app
RUN cmake -B build -G Ninja \
    -DHACL_INCLUDE_DIRS=/opt/hacl-star/dist/karamel \
    && cmake --build build

CMD ["./app"]

Push this to sota.io:

sota deploy --region eu-central-1 \
  --app my-crypto-service \
  --dockerfile Dockerfile

Your verified cryptographic service runs in Frankfurt, Germany — EU-native, GDPR-compliant, never touching US infrastructure.

HACL* is MIT licensed. Source: github.com/hacl-star/hacl-star. Try sota.io free tier — deploy your first HACL*-based service to EU infrastructure in minutes.