Skip to content

Introduction

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

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

Note:

  • BACKEND can be lean, legacy-lean, fstar, coq, pro-verif, ssprove or easycrypt. See the backend overview for the maturity of each backend. This manual covers the Lean and F* backends.
  • The subcommands cargo hax, cargo hax into and cargo hax into <BACKEND> take options. For instance, you can cargo hax into fstar --z3rlimit 100. Use --help on those subcommands to list all options.

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

  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.

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.

  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.