# hacl-star/hacl-star

HACL*, a formally verified cryptographic library written in F*

Repository: https://github.com/hacl-star/hacl-star
Canonical: https://ross.abutalabs.com/products/hacl-star
Language: F*
License: Apache-2.0
License Family: permissive
Topics: cryptography, verified-primitives, high-performance, security, formal-methods, formal-verification, inria, hacl, everest, verification
Last push: 2026-06-07T03:50:52+00:00

## Health v2 (maintenance only)
Score: 62/100 (v2, computed 2026-09-02T17:46:02.011165+00:00)
- activity 86, release rhythm 8, longevity 100
- inputs: {"age_days": 3723, "days_push": 87, "days_rel": null, "gap_med": null, "n_releases_24m": 0}
- flags: none
- formula: round(0.45*activity + 0.35*rhythm + 0.20*longevity); archived -> min(score, 10)

## Adoption (not part of the score)
Stars 1837, forks 193 (observed 2026-08-28T04:05:42.787354+00:00)

## What it is
HACL* is a formally verified cryptographic library written in F* (Low*) and compiled to efficient standalone C code, covering algorithms like Curve25519, Ed25519, AES-GCM, ChaCha20, Poly1305, SHA-2/3, HMAC, and HKDF. It includes ValeCrypt for verified assembly implementations and EverCrypt, an agile provider that multiplexes the fastest verified implementation per platform.

## Use cases
- verify cryptographic primitives for memory safety and correctness
- integrate high-assurance crypto into a C project
- get timing side-channel resistant implementations of Ed25519 or AES-GCM
- support NaCl API or TLS 1.3 ciphersuites with verified code
- compile verified crypto to WebAssembly
- automatically pick the fastest verified crypto implementation per CPU

## When to choose
- you need formally proven memory safety, functional correctness, and secret independence
- you want high-performance verified C code for modern primitives like Curve25519 or ChaCha20-Poly1305
- your project can tolerate a research-oriented codebase

## When to avoid
- you need production-ready packages, bindings, and documentation - use cryspen/hacl-packages instead
- you need a broad algorithm catalog beyond the supported modern primitives
- you are not comfortable tracking F* master and a research codebase

## Facets
- artifact type: library
- maturity: active
- function: cryptography, security
- domain: security, developer-tools
- platform: cross-platform, c, cpp, wasm
- tags: formal-verification, fstar, everest, nacl, tls-1-3, side-channel-resistance, research

## Member repositories
- hacl-star/hacl-star (main) score 62

## Provenance
- Observed fields: from GitHub, fetched 2026-08-28T04:05:42.787354+00:00.
- Health v2: computed from the inputs above; adoption is never an input.
- Inferred fields (summary, facets, guidance): AI-extracted, prompt v1, taxonomy v1, on 2026-08-30T03:18:26.156637+00:00, confidence not recorded.
  - readme: https://github.com/hacl-star/hacl-star (fetched 2026-08-28T04:05:42.787354+00:00, sha beffdd0a6d19)
- Data as of 2026-08-30T08:39:29.467469+00:00.