hax: Rust to F*, Rocq, Lean, ProVerif, SSProve and EasyCrypt
============================================================

hax translates a large subset of Rust into F*, Rocq, ProVerif, SSProve and EasyCrypt, with a Lean backend in development. Cryspen used it to verify libcrux's ML-KEM (portable and AVX2 field arithmetic, NTT and serialization) in F*; libcrux ML-KEM ships in Mozilla and Signal.

Maintainer: Cryspen
Website: https://github.com/cryspen/hax
Category: Verified implementations
Targets: Rust, libcrux ML-KEM and ML-DSA, Protocol models (ProVerif)
Approach: Translation of a large Rust subset into proof assistants; properties proved on the extracted model
Access: Open source
Status: Active; Lean backend under development with EF funding
Strengths: Production Rust stays production Rust. | Many backends, including symbolic (ProVerif). | Shipped verified post-quantum code at scale.
Limits: Rust subset restrictions. | Properties are only as good as the specification (Verification Theatre). | Lean backend not yet complete.
Firms using it: Cryspen
Sources: https://github.com/cryspen/hax | https://cryspen.com/post/ml-kem-verification/ | https://eprint.iacr.org/2026/192

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