← All repos

hax

A Rust verification tool

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

Tech stack & purpose

hax is a Rust verification tool built with OCaml that translates Rust code into formal verification backends. The tool works through a series of phases that sequentially transform Rust's internal typed representation into other representations, ultimately targeting backends like F*, Lean, and ProVerif. The project includes a web-based debugger for visualizing code transformations step-by-step, numerous internal utilities for code generation and phase management, and a collection of examples demonstrating extraction and formal verification of real-world algorithms like SHA-3, ChaCha20, and Barrett reduction.

Community & reference links

Languages

Rust
26.1%
OCaml
24.0%
Rocq Prover
16.3%
Lean
16.1%
F*
15.2%
JavaScript
1.0%
Python
0.4%
Makefile
0.4%
Nix
0.2%
Shell
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 61)