← All repos

hax

A Rust verification tool

GitHubhax.cryspen.com
formal-verificationrust
Browse cluster: Lean4 Formal Verification & Cryptography →
6,263commits
60contributors
16languages

Tech stack & purpose

hax is a Rust verification tool developed by Cryspen that translates a large subset of Rust into formal languages including Lean, F*, Rocq, ProVerif, SSProve, and EasyCrypt. The tool operates as a cargo subcommand and is built with Rust for its frontend and CLI components, OCaml for its core engine, and includes support for proc macros like `requires` and `ensures` to annotate pre- and post-conditions in Rust programs. hax supports multiple backends at varying maturity levels, with F* marked as stable, the Lean backend (via Aeneas) in active development, and others in experimental status, making it suitable for high-assurance cryptographic and formal verification use cases.

Community & reference links

Languages

OCaml
24.5%
Rust
24.5%
Rocq Prover
16.7%
Lean
16.5%
F*
15.4%
JavaScript
1.0%
Python
0.5%
Makefile
0.4%
Shell
0.2%
Nix
0.2%
Just
0.1%
HTML
0.0%
Dockerfile
0.0%
jq
0.0%
Dune
0.0%
Standard ML
0.0%

Contributors (top 30 of 60)