Skip to the content.


hax is a tool for high assurance translations that translates a large subset of Rust into formal languages such as F* or Coq. This extends the scope of the hacspec project, which was previously a DSL embedded in Rust, to a usable tool for verifying Rust programs.

So what is hacspec now?

hacspec is the functional subset of Rust that can be used, together with a hacspec standard library, to write succinct, executable, and verifiable specifications in Rust. These specifications can be translated into formal languages with hax.



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




This should work on Linux, MacOS and Windows.

Prerequisites: Nix package manager (with flakes enabled)

Using Docker

  1. Clone this repo: git clone && cd hacspec-v2
  2. Build the docker image: docker build -f .docker/Dockerfile . -t hacspec-v2
  3. Get a shell: docker run -it --rm -v /some/dir/with/a/crate:/work hacspec-v2 bash
  4. You can now run cargo-hax --help (notice here we use cargo-hax instead of cargo hax)

Manual installation

  1. Make sure to have the following installed on your system:
  1. Clone this repo: git clone && cd hacspec-v2
  2. Run the script: ./
  3. Run cargo-hax --help


There’s a set of examples that show what hax can do for you. Please check out the examples directory

Hacking on Hax

Edit the sources (Nix)

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

Structure of this repository


You can use the .utils/ script (which is available automatically as the command rebuild when using the Nix devshell):

Publications & Other material

Secondary literature, using hacspec:


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