hax
Direct answerhax 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
- Repository
- https://github.com/cryspen/hax
- Category
- Verified implementations
- Targets
- Rustlibcrux ML-KEM and ML-DSAProtocol models (ProVerif)
- Approach
- Translation of a large Rust subset into proof assistants; properties proved on the extracted model
- Access
- Open source
- Status (2026-09-13)
- Active; Lean backend under development with EF funding
What hax does
hax keeps the Rust readable and moves the proof burden to the backend of your choice. It is also the tool at the centre of the February 2026 Verification Theatre paper, which found 13 vulnerabilities in libcrux and hpke-rs, four inside verified ML-KEM and ML-DSA code, all outside what the specifications stated. The lesson is not that hax failed but that the verification boundary must be published with the proof.
Where it is strong
- Production Rust stays production Rust.
- Many backends, including symbolic (ProVerif).
- Shipped verified post-quantum code at scale.
Limits and caveats
- Rust subset restrictions.
- Properties are only as good as the specification (Verification Theatre).
- Lean backend not yet complete.
When to choose it
Choose hax for Rust cryptographic libraries and ZK prover code where you want proofs without rewriting.
Who works with hax
Top-listed for implementation verification 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
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
Related frameworks in Verified implementations
Jasmin and libjade, Cryptol and SAW, Fiat-Crypto, HACL*, Vale and EverCrypt, Aeneas, Kani, CBMC, CryptoLine, Verus.