Hax and the Quiet Project of Making Rust Provably Correct

For most of computing history, formal verification and practical software development have lived in separate buildings. On one side sit the programs people actually run, written in languages chosen for speed, ergonomics, and ecosystem. On the other side sit the proof assistants, where mathematicians and a small cadre of specialists establish that algorithms behave as specified, usually working in languages that no production team would ever ship. The gap between these worlds has been wide enough that proving real code correct often meant rewriting it twice, once for the machine and once for the proof. Hax, a tool from Cryspen, is an attempt to narrow that gap by starting from the code people already write.

The central claim of hax is deceptively simple: take a large subset of Rust and translate it into formal languages such as F*, Rocq (the proof assistant formerly known as Coq), or Lean, where properties can be proven about it. The Rust you verify is the Rust you compile and run. There is no parallel specification drifting out of sync with the implementation, no second codebase to maintain. You annotate, you translate, you prove, and the artifact you reasoned about is the artifact that ships.

The argument for verifying the source you actually run

The deeper thesis here concerns where assurance should originate. Traditional high-assurance work tends to verify a model of a system and then trust, by hand or by convention, that the running code matches the model. Every translation between model and implementation is a place where confidence leaks out. Hax inverts the order. Rust becomes the source of truth, and the formal language becomes a derived view of it. Cryspen's own framing is that hax produces high assurance translations of Rust into formal languages, which means the proof obligations are generated from the program rather than reconstructed alongside it.

This matters most in cryptography, which is exactly where hax has found its earliest traction. Cryptographic code is unusually well suited to formal methods: the specifications are precise, the consequences of bugs are severe, and the algorithms are small enough that exhaustive reasoning is tractable. The project descends from hacspec, an effort to write cryptographic specifications in a readable subset of Rust, and the lineage shows in the supported backends. Alongside the general purpose proof assistants, hax targets tools built specifically for protocol analysis, including ProVerif for symbolic security proofs and SSProve for game-based cryptographic arguments.

How the translation actually works

Mechanically, hax presents itself as a Cargo subcommand, which is a quiet but important design decision. Verification tools that demand their own build system and their own mental model tend to stay in research groups. By living inside cargo, hax meets Rust developers where they already are. The primary command is cargo hax into BACKEND, where the backend can be fstar, coq, lean, easycrypt, or pro-verif. A developer who wants to hand stronger hints to the underlying solver can pass options straight through, as in cargo hax into fstar --z3rlimit 100, which raises the resource limit Z3 is allowed to spend discharging a proof obligation.

Under that friendly surface, the pipeline has several stages worth understanding. The rust-frontend component hooks directly into the Rust compiler and extracts its internal typed abstract syntax tree, the THIR, serializing it as JSON. This is a consequential choice. By reading the compiler's own typed representation rather than parsing Rust text independently, hax inherits Rust's real semantics, including the results of type inference and trait resolution, instead of approximating them. There is even a standalone cargo hax json subcommand that emits this typed AST, which is useful both for debugging and for building other tooling on top of the same extraction.

From there the JSON flows into the engine, written in OCaml, which performs the simplification and elaboration that turns Rust constructs into something each backend can express. The backends themselves live under engine/backends/, each responsible for the idioms of its target language. Notably, the team is carrying out an ongoing rewrite of this engine from OCaml to Rust, visible in the repository as rust-engine, a move that would let the project become more self-hosting and lower the barrier for Rust-fluent contributors who find OCaml unfamiliar.

The constraint that defines the tool

Every verification tool is shaped as much by what it refuses as by what it accepts, and hax is candid about its boundaries. The project intends to support nearly all of Rust, with one deliberate exception that reveals its philosophy: mutable references, the &mut T that pervades imperative Rust, are forbidden on return types and when aliasing. The reasoning is that hax promotes a functional style, and functional code is dramatically easier to reason about formally. A function whose output depends only on its inputs, with no hidden mutation reaching out through aliased pointers, maps cleanly onto the mathematical functions that proof assistants understand. Mutation through aliases, by contrast, is one of the hardest things to model soundly.

This is a genuine trade-off rather than a temporary limitation, and the project handles it with unusual transparency. Unsupported Rust features are catalogued as GitHub issues labeled unsupported-rust, and within that set, features the team does not plan to support soon carry a wontfix-v1 label. Developers can see in advance which corners of the language will and will not pass through the tool, which is a more honest contract than a vague promise of full coverage. The practical consequence is that code intended for verification with hax tends to be written in a particular disciplined dialect of Rust, one that happens to overlap heavily with the way careful cryptographic code is already structured.

What this connects to

Hax sits at the intersection of two longer trends. The first is Rust's steady colonization of domains that once belonged to C, including operating system kernels, browser engines, and cryptographic libraries, places where a single memory error can become a security catastrophe. Rust's type system already eliminates whole categories of those errors at compile time. Hax extends that same impulse one level higher, from memory safety toward functional correctness, asking not just whether the program avoids undefined behavior but whether it computes the right answer.

The second trend is the gradual democratization of formal methods. The body of work surrounding the project, including the hacspec paper and reports presented at venues like CoqPL and RustVerify, points toward verified pipelines that produce optimized, safe Rust from formal specifications, and toward security analyses of real systems such as blockchain voting and smart contracts. The recurring ambition across these efforts is to make proof a normal part of engineering rather than an exotic afterthought. A developer can try hax online without installing anything, or set up a local environment through manual installation, Nix, or Docker, with quick start guides available for both F* and Lean.

The honest assessment is that hax does not make verification free. Someone still has to state the properties that matter, structure the code to fit the supported subset, and wrestle with the proof assistant when an obligation refuses to close. What hax changes is the location of that effort. Instead of maintaining a separate formal model that must be trusted to match reality, the engineer reasons about the actual implementation, in a workflow that begins with a Cargo command they already know. That relocation, from a parallel artifact to the real one, is the substantive contribution, and it is the kind of unglamorous infrastructure that determines whether formal methods stay in the seminar room or finally reach the software people depend on.