hacspec/hax

A Rust verification tool

476

stars

5,061

commits

Rust

primary language

Sep 9, 2026

updated

hax.cryspen.com

formal-verification

rust

Browse cluster: Formal Verification & Rocq Prover →

README

hax

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

Try out hax online now!

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 and macOS, on both x86_64 and aarch64. Windows is not supported; use WSL there.

Manual installation

Make sure to have the following installed on your system:

Clone this repo: git clone git@github.com:cryspen/hax.git && cd hax
Create (or use an existing) opam switch by running opam switch create hax 5.1.1
Run the setup.sh script: ./setup.sh. This installs hax; aeneas and charon are downloaded on demand when first needed.
Run cargo-hax --help

Nix

This should work on Linux and MacOS.

Prerequisites: Nix package manager (with flakes enabled)

Either using the Determinate Nix Installer, with the following bash one-liner:

curl --proto '=https' --tlsv1.2 -sSf -L https://install.determinate.systems/nix | sh -s -- install

or following those steps.

Run hax on a crate directly to get Lean/F*/Coq/... (assuming you are in the crate's folder):
- nix run github:cryspen/hax -- into fstar extracts F*.
Install hax: nix profile install github:cryspen/hax, then run cargo hax --help anywhere
Note: in any of the Nix commands above, replace github:cryspen/hax by ./dir to compile a local checkout of hax that lives in ./some-dir
Setup binary cache: using Cachix, just cachix use hax

Note: the lean backend downloads its aeneas and charon binaries on demand (see Aeneas and Charon below); no extra install step is needed.

Using Docker

Clone this repo: git clone git@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
You can now run cargo-hax --help (notice here we use cargo-hax instead of cargo hax)

Note: Please make sure that $HOME/.cargo/bin is in your $PATH, as that is where setup.sh will install hax.

Note: the lean backend downloads its aeneas and charon binaries on demand (see Aeneas and Charon below); no extra install step is needed.

Aeneas and Charon (standalone)

The lean backend (cargo hax into lean) uses the charon + aeneas pipeline instead of the hax engine. It requires the aeneas and charon binaries.

Their versions are managed by hax: pre-built binaries are downloaded on demand, verified against the version manifest shipped with the release, and cached under $XDG_CACHE_HOME/hax/tools/. To see the active versions or pre-populate the cache (e.g. in CI or before going offline), run, inside your project:

cargo hax tools show
cargo hax tools install

The default versions shipped with a hax release are tested together and are the recommended choice. Pinning versions yourself is an advanced option: combinations other than the defaults are untested, so establishing that one works is up to you. To pin versions for a project, declare them in a hax.toml at your project's root:

[tools]
aeneas = "nightly-2026.07.01"
charon = "nightly-2026.07.01"

You can also build or install aeneas and charon yourself (e.g. from source) and point to them with a path entry in hax.toml (e.g. charon = { path = "vendor/bin/charon" }).

See Managing tool versions in the manual for the full reference (cargo hax tools, the hax.toml schema, resolution order, and the hax-lib compatibility check).

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).

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.

Publications & Other material

Secondary literature, using hacspec:

Contributing

Before starting any work please join the Zulip chat, start a discussion on Github, or file an issue to discuss your contribution.

Acknowledgements

Zulip graciously provides the hacspec & hax community with a "Zulip Cloud Standard" tier.

Contributors

(top 30 of 49)

1,790 commits

861 commits

444 commits

360 commits

Similar repos

hacspec/hacspec-v2

A Rust verification tool

474

shared contributors

AeneasVerif/aeneas

A verification toolchain for Rust programs

960

shared contributors

celabshq/libcrux

The formally verified crypto library for Rust

258

shared contributors

cryspen/libcrux

The formally verified crypto library for Rust

258

shared contributors

formal-land/rocq-of-ocaml

Formal verification for OCaml, with Rocq

274

similar language mix

AeneasVerif/eurydice

Eurydice compiles (a decent subset of) Rust to C. Verify programs in Rust, still get C code for…

399

shared contributors

AeneasVerif/charon

Analyze Rust crates without touching compiler internals

411

shared contributors

FStarLang/karamel

KaRaMeL is a tool for extracting low-level F* programs to readable C code

518

shared contributors

Languages

Rust

26.1%

OCaml

24.0%

Rocq Prover

16.3%

Lean

16.1%

15.2%

hacspec/hax

A Rust verification tool

476

stars

5,061

commits

Rust

primary language

Sep 9, 2026

updated

hax.cryspen.com

formal-verification

rust

Browse cluster: Formal Verification & Rocq Prover →

README

hax

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

Try out hax online now!

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 and macOS, on both x86_64 and aarch64. Windows is not supported; use WSL there.

Manual installation

Make sure to have the following installed on your system:

Clone this repo: git clone git@github.com:cryspen/hax.git && cd hax
Create (or use an existing) opam switch by running opam switch create hax 5.1.1
Run the setup.sh script: ./setup.sh. This installs hax; aeneas and charon are downloaded on demand when first needed.
Run cargo-hax --help

Nix

This should work on Linux and MacOS.

Prerequisites: Nix package manager (with flakes enabled)

Either using the Determinate Nix Installer, with the following bash one-liner:

curl --proto '=https' --tlsv1.2 -sSf -L https://install.determinate.systems/nix | sh -s -- install

or following those steps.

Run hax on a crate directly to get Lean/F*/Coq/... (assuming you are in the crate's folder):
- nix run github:cryspen/hax -- into fstar extracts F*.
Install hax: nix profile install github:cryspen/hax, then run cargo hax --help anywhere
Note: in any of the Nix commands above, replace github:cryspen/hax by ./dir to compile a local checkout of hax that lives in ./some-dir
Setup binary cache: using Cachix, just cachix use hax

Note: the lean backend downloads its aeneas and charon binaries on demand (see Aeneas and Charon below); no extra install step is needed.

Using Docker

Clone this repo: git clone git@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
You can now run cargo-hax --help (notice here we use cargo-hax instead of cargo hax)

Note: Please make sure that $HOME/.cargo/bin is in your $PATH, as that is where setup.sh will install hax.

Note: the lean backend downloads its aeneas and charon binaries on demand (see Aeneas and Charon below); no extra install step is needed.

Aeneas and Charon (standalone)

The lean backend (cargo hax into lean) uses the charon + aeneas pipeline instead of the hax engine. It requires the aeneas and charon binaries.

cargo hax tools show
cargo hax tools install

[tools]
aeneas = "nightly-2026.07.01"
charon = "nightly-2026.07.01"

You can also build or install aeneas and charon yourself (e.g. from source) and point to them with a path entry in hax.toml (e.g. charon = { path = "vendor/bin/charon" }).

See Managing tool versions in the manual for the full reference (cargo hax tools, the hax.toml schema, resolution order, and the hax-lib compatibility check).

Supported Subset of the Rust Language

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).

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.