hax

August 27, 2026 · View on GitHub

hax

hax is a tool for high assurance translations of a large subset of Rust into formal languages such as Lean, F* or Rocq.

Supported Backends

General purpose proof assistants			Cryptography & protocols
_{(via Aeneas)}	F*		ProVerif		EasyCrypt
_{🚀 active dev.}	_{🟢 stable}	_{🟠 experimental}	_{🟠 experimental}	_{🟠 experimental}	_{🟠 experimental}

Learn more

Here are some resources for learning more about hax:

Manual (work in progress)
- Quick start: Lean, F*
- Tutorial: Lean, F*
Examples: the examples directory contains a set of examples that show what hax can do for you.
Other specifications of cryptographic protocols.

Questions? Join us on Zulip or open a GitHub Discussion. For bugs, file an Issue.

Usage

hax is a cargo subcommand. The command cargo hax accepts the following subcommands:

into (cargo hax into BACKEND): translate a Rust crate to the backend BACKEND.
json (cargo hax json): extract the typed AST of your crate as a JSON file.

Backends

Backend	Command	Description
Lean (via Aeneas)	`cargo hax into lean`	Recommended for Lean. Uses Charon + Aeneas.
Lean (legacy)	`cargo hax into legacy-lean`	Uses the hax engine directly. Prefer `lean`.
F*	`cargo hax into fstar`	Stable.
Rocq/Coq	`cargo hax into coq`	Experimental.
ProVerif	`cargo hax into pro-verif`	Experimental.
SSProve	`cargo hax into ssprove`	Experimental.
EasyCrypt	`cargo hax into easycrypt`	Experimental.

Use --help on any subcommand for options (e.g. cargo hax into fstar --z3rlimit 100).

Installation

hax is supported on Linux (x86_64 and aarch64) and macOS (aarch64). Windows is not supported; use WSL there.

All methods below install hax itself; the target provers (Lean, F*, ...) must be installed separately (see the manual).

For the Lean backend

The Lean backend runs the Charon + Aeneas pipeline instead of the hax engine, so from hax 0.4.0 onwards it needs no other hax component than the cargo-hax binary.

Prerequisites: a C compiler and rustup (used by Charon at extraction time).

cargo install --locked cargo-hax

--locked uses the dependency versions the release was tested with.

To skip that build, use cargo-binstall to download the binary the release published:

cargo binstall cargo-hax

The binary is the one cargo install --locked would produce, built on stable. It needs glibc 2.35 or newer on Linux, and macOS 11 or newer. cargo binstall checks neither: it picks the archive from the platform alone, so an older system installs a binary that fails to start; cargo install --locked cargo-hax covers those systems. Releases from before 0.4.0 carry no binary at all, and cargo binstall falls back to building from source there: pass --strategies crate-meta-data to have it fail instead of compiling.

Aeneas and Charon themselves need no install step: hax downloads pre-built binaries on demand. See Managing tool versions in the manual for how they are managed, pinning versions per project, and using your own binaries.

From the repository

To use an unreleased version of cargo-hax, install it from a checkout:

git clone https://github.com/cryspen/hax.git && cd hax
cargo install --locked --path cli/cargo-hax

Pinning hax per project

cargo-run-bin can pin hax per project, next to the version of hax-lib the project depends on:

[package.metadata.bin]
# The version of hax to use, matching the `hax-lib` the project depends on.
cargo-hax = { version = "<version>", bins = ["cargo-hax"], locked = true }

hax is then invoked as cargo bin cargo-hax instead of cargo hax, and the pinned version is installed on first use. Running cargo bin --sync-aliases once adds an alias to the project's .cargo/config.toml, so that the usual cargo hax invocation uses the pinned version as well.

For all backends

The F*, Rocq/Coq, ProVerif, SSProve, EasyCrypt, and legacy Lean backends need the hax frontend driver and engine as well. Each method below installs everything, including cargo-hax:

Manual installation

Prerequisites: a C compiler, opam, rustup, nodejs, and jq.

Clone this repo: git clone https://github.com/cryspen/hax.git && cd hax
Create (or use an existing) opam switch by running opam switch create hax 5.4.1
Run the setup.sh script: ./setup.sh

Nix

Prerequisites: the Nix package manager with flakes enabled, e.g. installed via the Determinate Nix Installer.

Install hax with nix profile install github:cryspen/hax.

Alternatively, run hax on a crate without installing it (from the crate's folder): nix run github:cryspen/hax -- into <backend>. To speed up builds with the hax binary cache, run cachix use hax.

Docker

Prerequisites: Docker.

Clone this repo: git clone https://github.com/cryspen/hax.git && cd hax
Build the docker image: docker build -f .docker/Dockerfile . -t hax
Get a shell: docker run -it --rm -v /some/dir/with/a/crate:/work hax bash

Inside the container, hax is invoked as cargo-hax instead of cargo hax.

Supported Subset of the Rust Language

hax intends to support full Rust, with the one exception, promoting a functional style: mutable references (aka &mut T) on return types or when aliasing (see https://github.com/cryspen/hax/issues/420) are forbidden.

Each unsupported Rust feature is documented as an issue labeled unsupported-rust. When the issue is labeled wontfix-v1, that means we don't plan on supporting that feature soon.

Quicklinks:

Hacking on hax

The documentation of the internal crate of hax and its engine can be found here for the engine and here for the frontend.

Edit the sources (Nix)

Just clone & cd into the repo, then run nix develop .. You can also just use direnv, with editor integration.

The flake provides several dev shells:

Shell	Purpose
`nix develop .`	Hacking on hax itself: the toolchain to build the Rust CLI, the frontend and the OCaml engine. Provides no backend verifier.
`nix develop .#fstar`	The above plus F, for the F backend and the F* proof libraries. Used by CI to check the proof libraries.
`nix develop .#examples`	The above plus ProVerif and Lean (through `elan`), for running `examples/` against a hax you build yourself.
`nix develop .#ci-examples`	Running `examples/` against a hax built by the flake, rather than one you build from source. Used by CI.

The first three shells give you the toolchain to build hax, not a cargo-hax binary: run just build first (see below).

In any Nix command from the Installation section, replace github:cryspen/hax by ./some-dir to compile a local checkout of hax that lives in ./some-dir.

Structure of this repository

frontend/: Rust library that hooks into the Rust compiler and extracts its internal typed abstract syntax tree THIR as JSON.
engine/: the simplification and elaboration engine that translates programs from the Rust language to various backends (see engine/backends/). Written in OCaml.
rust-engine/: an on-going rewrite of our engine from OCaml to Rust.
cli/: the cargo hax subcommand and the custom rustc drivers it uses to run the frontend.
hax-lib/: helper crate providing hax-specific macros (e.g. requires, ensures) for annotating Rust programs.
hax-types/: types shared between the frontend, the CLI, and the engine.
proof-libs/: a symlink to hax-lib/proof-libs/, the per-backend proof libraries that the extracted code builds against.
examples/: examples showing what hax can do.
tests/: integration tests.
docs/: sources of the hax website, including the manual and the blog.

Compiling, formatting, and more

We use the just command runner. If you use Nix, the dev shell provides it automatically, if you don't use Nix, please install just on your system.

Anywhere within the repository, you can build and install in PATH (1) the Rust parts with just rust, (2) the OCaml parts with just ocaml or (3) both with just build. More commands (e.g. just fmt to format) are available, please run just or just --list to get all the commands.

hax

hax