F*: Dependently typed language behind HACL*, hax and DY*
========================================================

F* 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: Active
Strengths: Largest body of deployed verified crypto. | Automation via Z3. | Extraction to C.
Limits: Proof brittleness under solver changes. | Smaller community than Lean. | Not used for circuits.
Firms using it: Cryspen
Sources: https://fstar-lang.org

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