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!

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

Here are some resources for learning more about hax:

• Manual (work in progress)
  • Quick start: Lean, F*
  • Tutorial: Lean, F*
• Examples: 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.

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.
• extract (cargo hax extract [NAME...]): run the proof scenarios declared in hax.toml; without names, every scenario in scope runs. See Proof scenarios in the manual.
• json (cargo hax json): extract the typed AST of your crate as a JSON file.
• tools (cargo hax tools SUBCOMMAND): manage the external tools hax depends on (e.g. Charon and Aeneas). See Managing tool versions in the manual.

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

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 quick start of the respective backend in the manual).

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.

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

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.

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:

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

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

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

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.

Prerequisites: Docker.

1. Clone this repo: git clone https://github.com/cryspen/hax.git && cd hax
2. Build the docker image: docker build -f .docker/Dockerfile . -t hax
3. 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.

hax intends to support full Rust, with one exception that promotes a functional style: mutable references (aka &mut T) are forbidden on return types and when aliasing (see #420).

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:

• 🔨 Rejected rust we want to support;
• 💭 Rejected rust we don't plan to support in v1.

• 📕 Tech report
• 📕 HACSpec: A gateway to high-assurance cryptography
• 📕 Original hacspec paper

• 📕 Last yard
• 📕 A Verified Pipeline from a Specification Language to Optimized, Safe Rust at CoqPL'22
• 📕 Hax - Enabling High Assurance Cryptographic Software at RustVerify24
• 📕 A formal security analysis of Blockchain voting at CoqPL'24
• 📕 Specifying Smart Contract with Hax and ConCert at CoqPL'24

Before starting any work please join the Zulip chat, start a discussion on Github, or file an issue to discuss your contribution. The contribution guidelines are described in CONTRIBUTING.md, including the development setup, the structure of the repository, and the build commands.

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