F*

Direct answerF* is the dependently typed language in which HACL* and libcrux proofs are written and the primary backend of hax. It combines proof-assistant expressiveness with SMT automation and extracts to C.

Maintainer: Microsoft Research and Inria
Website: https://fstar-lang.org
Category: Proof assistants and general verifiers
Targets: HACL*hax (main backend)DY*libcrux
Approach: Dependently typed effectful programming with SMT automation; extraction to C and OCaml
Access: Open source (Apache-2.0)
Status (2026-09-13): Active

Last reviewed 2026-09-13 by the sorryfree editors.

What F* does

Most shipped verified cryptography (Firefox, Signal, Linux) was proved in F*. Its SMT-heavy style can make proofs brittle across versions, which projects mitigate with careful lemma hints.

Where it is strong

Largest body of deployed verified crypto.
Automation via Z3.
Extraction to C.

Limits and caveats

Proof brittleness under solver changes.
Smaller community than Lean.
Not used for circuits.

When to choose it

Choose F* when building on HACL* or verifying Rust via hax's default backend.

Who works with F*

Cryspen.

Top-listed for proof engineering work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website

Lean 4 and Mathlib, Rocq (formerly Coq), Isabelle/HOL, ACL2 (R1CS and PFCS books), K framework and KEVM, Certora Prover.

Sources

Last reviewed 2026-09-13 by the sorryfree editors. Machine-readable: data.json · summary.txt

F*