Skip to content

2025

  • 2 min read

This Month in Hax: September 2025

In September, we successfully merged 44 pull requests!

After a summer slow down, we focused on improving the new rust-written engine of Hax (that progressively replaces the OCaml one), along with its flagship backend (Lean), while consolidating the documentation and tutorial. We released a new version of hax 🎉

In the rust-engine, a lot of work went into the treatment of identifiers (#1648, #1689, #1693).

We improved the caching (#1701, #1719), and the control over extraction with attributes.

The Lean backend saw a lot of new features: structs, enums, basic support for traits, support for functionalized loops. Along those, we improved the documentation in the tutorial and in the manual. The F*-parity and the official launch of the Lean backend are getting closer!

Stay tuned for more updates next month!

Full list of PRs

Contributors

  • 1 min read

This Month in Hax: August 2025

In August, we successfully merged 17 pull requests!

This month, we continued the effort of building out the new hax engine in Rust, with a focus on creating a robust infrastructure for backend development. We introduced a generic Backend trait and a new printing infrastructure, which will simplify the process of creating new backends. We also improved how global identifiers are handled and added visitors.

Building on this new infrastructure, the Lean backend saw significant progress. This month, we merged the first Lean proofs and a set of Lean examples. The Lean printer was also updated to leverage the latest improvements in the Rust engine.

Stay tuned for more updates next month!

Full list of PRs

Contributors

  • 2 min read

This Month in Hax: July 2025

In July, we successfully merged 32 pull requests!

@Nadrieril made sure that we use a recent version of rustc (PR #1534) and made new improvements to trait resolution in the frontend (PR #1522).

We continued efforts to improve the usability of hax with several f* core lib additions, and improvements to the CI.

More importantly, @W95Psp, @clementblaudeau and myself worked on improvements of the new hax engine implemented in Rust (PR #1508, #1518, #1525 and #1526).

Finally, let's celebrate the arrival of our new backend for lean (PR #1509)! @clementblaudeau is taking the lead on this project. This backend is implemented in Rust using our new infrastructure. It is still under active development and many improvements will come in the next couple of months.

Stay tuned for more updates next month!

Full list of PRs

Contributors

  • 2 min read

This Month in Hax: June 2025

In June, we successfully merged 21 pull requests!

@Nadrieril and @N1ark continued the improvements on the frontend side with the addition of unchecked arithmetic operators (#1513), regrouping generic and trait arguments in a struct (#1514), support of trait aliases in full_def (#1494), addition of Ty::FnDef (#1487), drop calls resolution (#1467) and more.

@W95Psp, @clementblaudeau and myself worked on adding infrastructure for writing backends and compilation phases for hax in Rust (instead of Ocaml). We now have a Rust version of the hax AST and we can convert back and forth from the Ocaml version (which should allow to incrementally replace Ocaml phases by Rust phases). We also offer utilities for printing this AST when implementing backends. Our plan for the next months is to use this for the new backends we will add, and experiment with Rust phases.

Stay tuned for more updates next month!

Full list of PRs

Contributors

  • 2 min read

This Month in Hax: April 2025

In April, we successfully merged 38 pull requests!

Thanks @Nadrieril, for pinning a more recent nightly version of the Rust compiler (#1391). Nadrieril also continued making the frontend more robust and complete with work on constants #1402, #1420, #1429) and item's children (#1412).

@W95Psp worked on hax-lib with improved support for writing f* lemmas in rust (#1428), and fstar post-processing with tactics (#1437).

I worked on while loops which now support invariants and variants (to prove termination) in #1375

We also worked on various improvements like removing deprecated dependencies used by hax-lib (#1385 and #1394), some ProVerif backend workarounds by @jschneider-bensch (#1360, #1401 and #1406), and multiple f* core lib additions.

Stay tuned for more updates next month!

Full list of PRs

Contributors

  • 1 min read

This Month in Hax: May 2025

In May, we successfully merged 19 pull requests!

@Nadrieril helped making the frontend more robust and complete with work on impl exprs (#1431), MIR extraction (#1444, #1457) and FnOnce (#1477).

@W95Psp worked on hax-lib with improved support for writing F* lemmas in Rust (#1456).

@cmester0 improved the Coq and SSProve backends (#1426 and #1108)

Apart from that, we contributed multiple F* core library additions.

Stay tuned for more updates next month!

Full list of PRs

Contributors

  • 4 min read

Redesigning Global Identifiers in hax

A careful treatment of identifiers lies at the heart of all code analysis frameworks, and we hope our experience here proves useful to others.

In Rust, global identifier serves to uniquely locate uniquely an item: for instance ::serde::ser::Serialize designates the Serialize trait from the Serde library. In constrat, local identifiers are relative, limited to the scope in which they are declared.

Global Identifiers from the Rust Compiler

Initially, hax assumed that all identifiers originated exclusively from Rust. While this assumption held in the early stages, it was eventually challenged as the system grew1. As hax evolved, new requirements emerged, prompting the engine to generate identifiers internally:

  • Trait pre- and post-conditions: in hax, these are explicitly represented as concrete methods within typeclasses. Conversely, in Rust, these conditions exist only as anonymous standalone functions.
  • Explicit enum cast operations: enum casts are primitive operations in Rust, but hax treats these casts as specialized operations, assigning distinct identifiers to them.
  • Cross-module mutually recursive item bundles: these bundles2 are internally introduced by hax, necessitating the generation of unique identifiers to prevent naming conflicts.

Moreover, the previous identifier system lacked detailed metadata, such as the type of identifier (struct, function, type, etc.), complicating identifier rendering for backend tools.

Issues with the Previous Design

Initially, identifiers were represented using slightly modified Rust DefIds accompanied by minimal metadata indicating the identifier's kind. This approach presumed that hax would never alter these DefIds but merely use those directly produced by the Rust compiler.

This assumption was quickly challenged. The need to prefix or suffix identifiers emerged early, but the introduction of new internal modules completely disrupted the assumption. Identifiers had to be relocated across modules, representing a significant departure from the original design.

As the API for manipulating identifiers grew increasingly permissive and transparent, the foundational assumption—that DefIds were unique, consistent, and Rust-generated—was entirely undermined. In consequence, rendering names for the backends became a complicated, error-prone process. This resulted in numerous bugs in identifier rendering in backend outputs, leading to at least 16 documented issues (#1135).

As an example, the rendering process made distinguishing the two functions c very difficult in the following snippet of code. This resulted in a bug (see #1136) where hax would extract F* code with two functions both named c in the same module Mycrate.A.B! 

mod a {
    mod b {
        fn c() { ... }
    }
}
fn a() {
    mod b {
        fn c() { ... }
    }
}

Our New Approach

The frontend has been enhanced to explicitly indicate the kind of each identifier, clarifying whether it represents a function, an associated type, a constant, etc. Additionally, it now provides detailed parent information, making the origin of identifiers more transparent. Alongside these improvements, we have redesigned our internal engine's identifier representation, introducing a layered structure where each layer addresses a distinct aspect.

  1. Raw Rust Identifiers: using Rust's DefId type, generated from Rust to OCaml, with minor normalization to address potential duplicate references. These identifiers are immutable and cannot be arbitrarily created or altered.

  2. Explicit_def_id: addresses Rust's ambiguity between a struct constructor and the type itself, explicitly distinguishing identifiers belonging to types from those belonging to values, enhancing clarity for backend translation.

  3. Concrete_ident: built upon Explicit_def_id, this layer adds capabilities for generating fresh module names or adding hygienic suffixes. It ensures identifier uniqueness and declares constraints clearly when creating new names or namespaces.

Simplified Identifier Views

Rust's namespace structure is highly flexible, allowing various forms of nesting, such as types within functions, functions within constants, and more.

Broadly, there are two kinds of nesting in Rust. Consider the following snippet:

mod a {
    impl MyTrait for MyType {
        fn assoc_fn() {
            struct LocalStruct {
                field: u8,
            };
        }
   }
}

In this example, the user has intentionally placed LocalStruct within the method assoc_fn, which itself resides inside the module a. This is an instance of user-driven nesting, where the developer freely organizes elements within the code for clarity, convenience, or structural preference.

At the same time, we observe another form of nesting: field is contained within LocalStruct, and assoc_fn is enclosed within the impl block implementing MyTrait for MyType. This represents hierarchical nesting, which is dictated by the Rust language itself. Unlike user-driven nesting, hierarchical relationships are inherent to Rust's type system: a field must belong to a struct or an enum variant, and a method must exist within an impl block.

The following diagram shows how these hierarchical relationships are structured.

Distinguishing between these two types of nesting is crucial when rendering names. Hierarchical nesting often requires special handling in backends due to its structural constraints, whereas user-driven nesting primarily serves readability and organization.

To manage this effectively, we introduced a hierarchical view for identifiers. Instead of handling Rust's deeply nested identifier paths as-is, we transform them into structured, relational representations. This approach simplifies backend processing, minimizes namespace conflicts, and ensures better compatibility with backend language constraints.

Looking back at our a::b::c example, this hierarchical view makes the problem very easy, since modules and functions are user nesting.

Conclusion: Say Goodbye to Naming Issues (Almost)!

This comprehensive redesign of identifier representation and handling has resolved most previously identified naming issues and significantly enhanced the expressiveness and robustness of backend identifier rendering in hax.

Check out the pull request #1199 on the GitHub repository of hax for more details!

We are confident that this enhanced representation is sufficiently robust and flexible to accommodate future developments and evolving project requirements.

  1. See PR #935, PR #211 or PR #571 for examples of such new features. ↩↩

  2. Rust supports cross-module mutual recursion without enforcing declaration order, an uncommon feature among programming languages. In contrast, most of our backends require some form of forward declaration. To bridge this gap and accommodate Rust’s permissive namespacing, we group related items into bundles and reorder them to eliminate cross-module recursion. ↩↩

  • 2 min read

This Month in Hax: March 2025

In March, we successfully merged 32 pull requests!

Thanks @Nadrieril, who helped move hax forward by pinning it to a more recent nightly version of the Rust compiler (#1380). Nadrieril also continued work on the frontend. Trait resolution is now more robust, especially in the presence of closures (#1376), and our handling of constants has seen significant improvements, with refinements introduced in both #1367 and #1337.

Outside of the frontend, we also focused on enhancements and fixes within hax-lib and the engine. Notably, support for mathematical integers and logical propositions has been strengthened, making reasoning more precise and expressive (#1372, #1352, #1351). Additionally, we resolved several issues related to the use of self in contracts, improving overall stability and correctness in those scenarios.

March also brought new capabilities to hax-lib. The newly introduced decreases attribute makes it possible to express termination arguments directly in Rust, giving users better control over termination checking. Furthermore, the addition of the <backend>::replace_body family of attributes allows developers to substitute the body of a Rust function with backend-specific code, offering a powerful mechanism for fine-tuned extraction when needed.

Stay tuned for more updates next month!

Full list of PRs

Contributors

  • 2 min read

This Month in Hax: February 2025

In February, we merged 23 pull requests!

The MIR translation of the frontend was improved by @Nadrieril: some bugs were fixed, and our handling of constants have been improved and is now more robust.

One of the major updates this month was the introduction of a new Prop abstraction in hax-lib, which enhances expressiveness in property-based reasoning within the Hax engine. With Prop, it is now possible to write non-computable properties that leverage universal quantifiers.

We also made significant progress in the engine, including fixing issues related to continue handling in loops and ensuring proper naming and disambiguation in bundled components (#1280, #1286).

We also tackled improvements in the F* backend, such as fixing trait inheritance in rand-core (#1322) and expanding the core library (#1292).

Stay tuned for more updates in the coming months!

Full list of PRs

Contributors

  • 6 min read

Trying to make hax usable in more contexts

The hax toolchain has been successfully used to formally verify our cryptographic implementations for ML-KEM,Bertie and more. All these projects are developed with formal verification (using hax) in mind, and use a limited subset of Rust features. However, hax is under constant development and the improvements we bring are targeted at making it more usable. With these improvements we want to bring hax to a new kind of projects that don’t have restrictions on the Rust patterns they use. We want hax to be usable in this context with minimal modifications to the code (ideally no modification at all). An example of such a project is the verification of sandwich, a high-level cryptographic library built by SandboxAQ. This project revealed the weaknesses of hax in this context which brought us to implement some improvements that will be presented in this blog post.

Challenges

The projects that use hax from the beginning can limit themselves to the subset of Rust supported by hax. Applying hax to a pre-existing project means that it may use various Rust features that are probably not supported yet in hax. The challenge is then to identify which features to prioritize for support in hax (and adding support is yet another challenge), and which features have no short-term plan for support. For the latter we need to abstract out the code (if it is not relevant for proofs) or rewrite it (when possible; ideally we try to avoid this). Having external users encourages us even more to make hax an easily-usable and well-documented tool.

Frontend improvements

The hax frontend is mostly relying on rustc and cargo to extract intermediary representations of a Rust crate. It is supposed to produce a result for any Rust crate (restrictions on the available Rust features come later in the toolchain). However the information given by rustc is sometimes partial or lacks some parts that are needed for our translations. A crucial example of this is trait resolution as we need to know the trait derivation that is used by each call of a trait method. This is a part of the hax frontend that has proven tricky and still had many bugs a few months ago. At that time, launching it on a somehow complicated crate had big chances of resulting in a crash. As part of our effort to improve the usability of hax, many of these bugs have now been fixed (in collaboration with our colleagues at Inria). This is a big step forward, since even for a project that looks small and simple, we need to handle all of its dependencies which are usually more problematic.

According to our tests on the top 500 crates (by number of downloads on crates.io), hax frontend succeeds without crashing or timing out on more than 99%. However we are still looking for a better way to measure the coverage of the Rust features, and identifying the situations where we can still improve.

Recursive Bundles

Rust code is organized in modules, where modules can be seen as a namespacing system. When translating modules to our backends (F*, Coq, ProVerif) we need to generate the corresponding module-like abstraction in the backend, which typically works quite differently. In particular our backends require the module dependency graph to be acyclic while Rust has no such restriction. It is quite common in Rust to make use of this and create cyclic dependencies between modules which means it is necessary for us to have a solution for this problem. Here is an example (you can open it in the hax playground to check the code hax generates out of it): 

pub struct Error();

mod private {
    pub(crate) fn f() -> Result<(), super::Error> {
        Ok(())
    }
}

pub fn user_f() -> Result<(), Error> {
    private::f()
}
Open this code snippet in the hax playground

In this example there is a dependency between the top level module and the private module. Our solution to break these cycles is simply to put the content of the cyclic modules in a single module (that we call bundle), and then re-exposing the items in their original modules. This solution is not perfect because it changes the architecture of the generated code compared to the original code, and it could be improved by minimizing the content of the bundles (choosing a set of definitions to break the cycle instead of the full content of the modules). But so far it has proven very useful as it removes a big limitation on the Rust we support.

Opaque items

Large projects usually contain code that we don’t support yet but we still want to reason about the rest of the project and have an abstract model (axiomatization) for the parts that we don’t support. We need to control which parts we want to fully extract and which parts we extract only as opaque items. The command-line options offered by the hax toolchain provide a solution to this, but they only allow to choose at the model level, which is inconvenient for large projects. To make this more practical we added another way to specify inside the source with the attribute hax_lib::opaque makes an item axiomatized. There is still the problem of complicated -i flags which will be solved in the future by having the corresponding information in configuration files.

Control flow rewriting without monads including inside loops

Translating imperative code to functional backends for verification implies some handling of side effects and transformation of control flow. A classic solution for this is to have a monadic encoding state which results in generated code that can be hard to read (and to reason about). This is the solution that was implemented (with some bugs) in hax but we decided to replace it with a solution without monads. The code we produce is simpler to read, but the main limitation is that there is code duplication which in some cases can lead to an extracted code that is exponentially bigger than the source.

Here is a simple example of this: 

fn f() -> i32{
    if true {
        if true {
            return 1
        }
    }
    3
}
Open this code snippet in the hax playground

The F* code extracted from this example is the following: 

let f (_: Prims.unit) : i32 =
 if true
 then if true then mk_i32 1 else mk_i32 3
 else mk_i32 3
Here the semantics is preserved, but adding the else branches results in a duplication of the return value 3. Our idea to improve in the future is to revive the monadic version, but use it only if the duplication is too big. Support for control flow (return, break and continue) in loops has been added as well. In hax, loops are translated as a functional fold in which the accumulator keeps track of the modification of the environment done by the effectful operations in the source. This extension relies on a monadic encoding of the loop result, that is passed in the accumulator to deal with the specific cases of return, break and continue.

Items sorting

A quality of life feature that we have been lacking for a long time is trying to respect, as much as possible, the same order of items in the generated code compared to the source. We need to modify the order because (as for modules), Rust allows items to be defined in any order, while our backends need items to be defined after the other items they depend on (except for mutual recursion). We rely on a graph topological sort to ensure this property, and now use a modified version of the stable topological sort provided by ocamlgraph, which produces an order that respects the dependencies, but in the absence of constraints tries respects the order of the source.

Conclusion

Bringing hax to a new kind of project revealed the gap needed for it to be usable, but thanks to our active work, we have made great progress towards this goal. Even though there is still much more to do, this has allowed us to get results in these new applications of hax (stay tuned for more details about that!).