Daniel Dia

Bridging the Gap: Authoring Comprehensive Documentation for the hax Formal Verification Tool

November 15, 2025

The Challenge

Modern cryptography demands both high performance and mathematical proof of correctness. The hax library is a vital tool for bridging this exact gap, translating idiomatic Rust into formal verification backends like F*, Lean4, and Coq. This allows developers to write a single, high-performance Rust codebase and also formally prove its correctness.

However, as I began working with the tool, I discovered a significant gap: the lack of comprehensive, user-facing documentation. For a tool this powerful, this is a major hurdle for new users, making it difficult to understand its architecture, learn the API, and leverage its full capabilities.

My Contribution

To help solve this, I took the initiative to write a complete, 8-module set of technical documentation. This isn’t just a brief overview; it’s an exhaustive guide designed to take a new user from basic setup to writing advanced, provably correct cryptographic code.

My work is structured as a complete documentation suite, with each file serving a distinct purpose:

  • README.md (Top-Level Guide): A comprehensive introduction to the entire hax ecosystem, covering the core library (hax-lib), the CLI (cargo-hax), the translation engine (hax-engine), and all supported backends. It explains the “Why” and provides a full verification workflow.

  • hax-lib-api.md (API Reference): An exhaustive API reference for the core hax-lib crate. This is the reference for writing verifiable code, detailing the mathematical types (Int, Prop), abstraction traits (Abstraction, Refinement), and all specification macros (e.g., #[requires], #[ensures], #[loop_invariant]).

  • cli-backends.md (CLI & Backends): A complete guide to the cargo-hax command-line tool. It covers installation, configuration, and specific instructions for all supported verification backends: F*, Lean4, Coq/Rocq, ProVerif, SSProve, and EasyCrypt.

  • examples-patterns.md (Examples & Patterns): A practical, hands-on guide for users. It starts with a “hello world” example and builds up to verifying real-world cryptographic algorithms, including detailed patterns for ChaCha20, Barrett Reduction, and SHA-256.

  • verification-techniques.md (Proof Strategies): A high-level guide on how to think about verification. It explains core concepts, different proof strategies (forward/backward reasoning, induction), common invariant design patterns, and techniques for arithmetic and memory safety verification.

  • internal-architecture.md (Internal Architecture): A deep dive for advanced users and contributors. It details the hax compilation pipeline, from the frontend’s THIR extraction in rustc to the OCaml-based hax-engine, its simplification phases, and the backend code generators.

  • errors-troubleshooting.md (Error Reference): A crucial guide for debugging. It categorizes common failures (Compilation, Verification, Backend), provides debugging strategies, and includes a quick-reference table for error codes.

  • INDEX.md (Navigation Index): A simple navigation index that ties all the modules together, with quick links for different user personas (New Users, Developers, Advanced Users).

Community Feedback

After completing the documentation, I reached out to the core hax team, including Dr. Karthikeyan Bhargavan. He was kind enough to share the repository with the other developers on the Hacspec Zulip channel, which started a discussion on how to best integrate these new resources.

Karthikeyan Bhargavan: Here is a repo with some docs for hax-lib: https://github.com/danieldia-dev/hax-docs

This is by Daniel Dia.

@Lucas Franceschino @Maxime Buyse : would be great to get your comments and suggestions on how we can incorporate some of these ideas. Maybe there is some documentation somewhere.

You can follow that public discussion on the Hacspec Zulip: hacspec.zulipchat.com

My goal with this project was to lower the barrier to entry and help accelerate the adoption of this critical tool. I’m hopeful this work will be valuable to the formal verification and high-assurance Rust communities.

The full 8-module documentation repository is available on GitHub.