🌐 Website | 📖 Book | 📝 Blog | 💬 Zulip | 🛠️ Internal docs | 🛝 Playground

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.

Try out hax online now!

Here are some resources for learning more about hax:

• Book (work in progress)
  • Quick start
  • Tutorial
• Examples: the examples directory contains a set of examples that show what hax can do for you.
• Other specifications of cryptographic protocols.

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 (e.g. fstar, coq).
• json (cargo hax json): extract the typed AST of your crate as a JSON file.

Note:

• BACKEND can be fstar, coq, easycrypt or pro-verif. cargo hax into --help gives the full list of supported backends.
• The subcommands cargo hax, cargo hax into and cargo hax into <BACKEND> takes options. For instance, you can cargo hax into fstar --z3rlimit 100. Use --help on those subcommands to list all options.

Hax intends to support full Rust, with the two following exceptions, promoting a functional style:

1. no unsafe code (see #417);
2. mutable references (aka &mut T) on return types or 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.

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

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

• rust-frontend/: Rust library that hooks in the rust compiler and extract 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/).
• cli/: the hax subcommand for Cargo.

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.

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

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