Skip to content

2026

  • 3 min read

This Month in Hax: August 2026

In August, we successfully merged 46 pull requests!

We extended our CLI functionality significantly: hax can now be installed via cargo binstall cargo-hax, and it can automatically download and manage its aeenas and charon dependencies. Moreover, users can declare proof scenarios in a hax.toml file to specify exactly which options they want to use for a particular project, and then run those scenarios via a new cargo hax extract command.

We extended our models of Rust core further and improved its testing infrastructure to make sure that it is an accurate model of Rust core. These models benefit both the Lean and the F* backend.

For the new Lean backend, we added support for hax_lib::requires, hax_lib::ensures, and other attributes and for the hax_lib::prop and hax_lib::int specification helpers.

This was our final sprint towards a release candidate for hax v0.4.0. The release candidate was published yesterday. Now, we are testing it, fixing bugs, and finalizing its documentation.

Thanks to the many external contributors we had this month!

Full list of PRs

Contributors

  • 2 min read

This Month in Hax: July 2026

In July, we successfully merged 31 pull requests!

We are preparing for the release of hax 0.4.0. The main change is that the Lean backend now uses aeneas, the Lean backend relying on the hax engine has been renamed legacy-lean. The integration with aeneas has been improved and is still one of our main focuses.

This includes improvements and fixes to the core-models library. The rust models have been reintegrated in the hax repo, and now extract to both Lean, through the new Lean backend, and F*. We also fixed issues with the hax-lib annotation macros.

Finally, we worked on the documentation and updating the examples to show the latest workflow with our main backends (Lean and F*).

Full list of PRs

Contributors

  • 1 min read

This Month in Hax: June 2026

In June, we successfully merged 6 pull requests!

Our main focus right now is the integration of aeneas into hax, which we will release in July. Besides that, we worked on improving our testing infrastructure and on our Rust core models.

Full list of PRs

Contributors

  • 1 min read

This Month in Hax: May 2026

In May, we successfully merged 6 pull requests!

We fixed various bugs and finally released hax 0.3.7! Our work to integrate Aeneas in the hax engine is still ongoing. Some of it is in our new external repo for the core models (https://github.com/cryspen/rust-core-models). And the changes to hax will be published later.

Full list of PRs

Contributors

  • 1 min read

This Month in Hax: April 2026

In April, we successfully merged 11 pull requests!

Besides various bug fixes, we improved the rendering of ellipsis in pattern-matching and refactored the mvcgen registration of the RustM monad to support partial correctness lemmas. Thanks to the external contributors @MavenRain, @niooss-ledger, and @remix7531!

Towards the end of the month, we participated in the Software Verification in Lean workshop and hackathon organized by the Beneficial AI Foundation and the Lean FRO. We came away with lots of new ideas for our Lean backend.

For a couple of weeks, we have been working on merging the Aeneas engine into Hax. We haven't made any public contributions to Hax in that direction yet, but we have created a new repo containing our Rust core models with an Aeneas-compatible extraction: https://github.com/cryspen/rust-core-models

Full list of PRs

Contributors

  • 1 min read

This Month in Hax: March 2026

In March, we successfully merged 8 pull requests!

This was a rather quiet month with some of us away for Real World Crypto and HACS in Taipei. But we continued to improve the Lean library with bugfixes and new additions like support for u128 and i128.

Special thanks to @JuanCoRo for improving and extending the treatment of binops in the Lean backend. And thank you @redshiftzero for your first PR!

Full list of PRs

Contributors

  • 2 min read

This Month in Hax: February 2026

In February, we successfully merged 32 pull requests!

This month, the Lean backend made headway by getting new Rust proof attributes. With the new attributes, Users can choose between two proof methods, one based on symbolic reasoning (grind) and one based on bit-blasting (bv_decide). This new setup is illustrated in our updated Tutorial and the Chacha20 example. Moreover, the Lean backend produces prettier output by opening namespaces, handles for-loops more reliably, and its library contains more of our Rust core models.

We also made great progress on our new THIR importer, implemented in Rust. Currenlty, it can be activated using --experimental-full-def, and we intend to make it the default soon.

Special thanks to @JuanCoRo, @klausnat, and @rusch95 for their contributions this month!

Full list of PRs

Contributors

  • 2 min read

This Month in Hax: January 2026

In January, we successfully merged 29 pull requests!

The Lean backend continues to get improvements, mostly thanks to @abentkamp! We now have more specs in the proof library (for while loops, negation and more), and improved tactics to reason with our annotations of pre/post-conditions (#1888). Some naming fixes, and improvements of the handling of associated types make us closer to reaching parity with the F* backend!

The other significant improvements are on the core models side. Thanks to some new models, the F* proof library is now entirely extracted from Rust core models. The Rust primitives models will remain hand-written in each backend, but they have been designed to be as small as possible, and are intended to be modelled in a very backend-specific way. The Lean library is now also partly extracted from core models! Some modules are excluded for now as they rely on Rust features that we don't support in the Lean backend for now. We will prioritize these missing features in the next few months to extend the Lean library using extraction from core models.

Full list of PRs

Contributors

  • 4 min read

Verifying a while loop in Hax/Lean

In our last blog post, the dog that didn't bark was Hax/Lean. It was missing because we did not have support for while loops then. Now, we support them and we will demonstrate it here.

You can find the results of this tutorial on https://github.com/cryspen/rust-gcd/tree/hax_lean1 on the branch hax_lean1.

Preparation

First, we need to install Hax and Lean:

  • Hax (We are using commit d1365d4, so after git clone git@github.com:cryspen/hax.git && cd hax, run git checkout d1365d4)

  • Lean

Again, we will use the gcd Rust crate as an example: 

git clone git@github.com:frewsxcv/rust-gcd.git && cd rust-gcd
git checkout 8fb3a59
We add hax-lib as a dependency, which will allow us to make annotations in the Rust code: 
cargo add --git https://github.com/hacspec/hax hax-lib --rev d1365d4

Extraction

Now we are ready to translate the Rust code into Lean code. We will limit ourselves to the euclid_u16 function here: 

cargo hax into -i '-** +gcd::euclid_u16' lean
This will create a new file proofs/lean/extraction/Gcd.lean containing the Lean version of the extracted function.

For Lean to find the required dependencies, we must add the following two files in proofs/lean:

lean-toolchain: 

leanprover/lean4:v4.23.0

lakefile.toml: 

name = "Gcd"
version = "0.1.0"
defaultTargets = ["Gcd"]

[[lean_lib]]
name = "Gcd"
roots = ["extraction.Gcd"]

[[require]]
name = "Hax"
path = "../../../hax/hax-lib/proof-libs/lean"
Make sure that the path above points to the subdirectory hax-lib/proof-libs/lean of the repository that you checked out during the installation of Hax (i.e., git@github.com:cryspen/hax.git on commit d1365d4). The path can be relative to the lakefile.toml file or absolute.

Now we can run Lean on the extracted code. 

(cd proofs/lean && lake build)
It should take a moment and then say: 
Build completed successfully (35 jobs).
So it this already verified? No, currently, we need to add a pre- or post-condition to a function to make Hax generate a specification that we can prove correct. (This will likely change in the near future.)

Verification

We can add the following hax_lib::ensures annoation above the definition of $euclid to say that we want to prove termination and panic-freedom: 

#[hax_lib::ensures(|_| true)]
pub const fn $euclid(a: $T, b: $T) -> $T
{
    ...
}
We run Hax and Lean again: 
cargo hax into -i '-** +gcd::euclid_u16' lean
(cd proofs/lean && lake build)
Now, we get lots of unsolved goals errors. We can open the Gcd.lean file to get a better impression of what is going on. The file contains a definition of Gcd.euclid_u16, which is the Lean version of our euclid_u16 function and which compiles without error. Below, we have a definition of Gcd.euclid_u16.spec, which contains the specification of the function and an attempted proof of correctness. It should have a red squiggly underline on the contract proof, indicating that the error occurs there. The default proof by mvcgen[Gcd.euclid_u16] <;> try grind fails.

If we click just behind mvcgen[Gcd.euclid_u16], we can see the verification conditions that Lean's mvcgen tactic generated in Lean's infoview. It shows a list of four goals. The second and the forth goal end in: 

ToNat.toNat 0 < ToNat.toNat 0
So this says that the u16 value 0, converted to a natural number, is smaller than itself. This is simply wrong and will be impossible to prove. These verification conditions are coming from the default termination measure associated with while loops, which is constant 0 by default. We will have to provide a better measure to prove termination, using the hax_lib::loop_decreases annotation. From our last blog post, we know that b is a useful measure for this loop: 
while b != 0 {
    hax_lib::loop_decreases!(b);
    // mem::swap(&mut a, &mut b);
    let temp = a;
    a = b;
    b = temp;

    b %= a;
}
After running Hax and Lean again, the default proof still fails, but the generated verification conditions can now be proved with some manual effort. After developing the proof in Lean, we can copy the proof into the Rust file so that it does not get overwritten when reextracting the code: 
#[hax_lib::ensures(|_| true)]
#[hax_lib::lean::proof("by
    mvcgen[Gcd.euclid_u16]
    · expose_names
      intro
      simp_all [a_1]
    · expose_names
      simp only [ToNat.toNat, h_4]
      apply Nat.mod_lt
      grind
    · expose_names
      intro
      simp_all [a_1]
    · expose_names
      simp only [ToNat.toNat, h_4]
      apply Nat.mod_lt
      grind")]
pub const fn $euclid(a: $T, b: $T) -> $T
{
    ...
}
(Be careful with the indentation here! Lean is white-space sensitive!)

After running Hax again, lake build now says: 

Build completed successfully (35 jobs).
Yay!

We are working on better automation for proofs like this one and on better coverage of the Rust core library, e.g., to be able to verify the binary gcd implementation in this crate as well.

  • 3 min read

My Departure from hax and Cryspen

Today, I want to share an update on both my professional path and my role in hax. I decided to leave Cryspen, and as a result, I will also be stepping away from hax.

Looking Back

Back in September 2023, while I was working at Inria, I started working with Karthikeyan on Hacspec. Hacspec was a domain-specific language embedded in Rust's syntax, aimed at cryptography specification and verification. It relied on the surface AST (abstract syntax tree) of the Rust compiler (rustc). Using such an early representation in the compiler pipeline gave us very limited information: no types, no name resolution -- essentially just syntax.

Both technically and in terms of intent, Hacspec had limitations. In December 2023, we decided to take a fresh start and build a new tool from the ground up: hax.

Designing and implementing hax has been a fun adventure. I had the constraint to write the "compiler" part of hax in OCaml. That led me to design hax in two main parts:

  • The frontend: hooks into rustc and dumps enhanced ASTs, inlining a large amount of semantic information about Rust programs. The frontend produces a comprehensive, complete, and easy-to-consume AST that other tools can build upon. It grew a lot, notably thanks to our collaboration with Inria (for Charon and Aeneas), and especially thanks to Nadrieril, with whom it has been a great pleasure and a lot of fun to work.

  • The engine: an OCaml binary that reads our frontend's Rust AST, applies a sequence of translation phases, and finally outputs F*, Coq, etc.

For a full year at Inria and then two years at Cryspen, I was the main developer of hax. Throughout this time, I greatly enjoyed working with Karthik; we discussed many aspects of hax countless times: its design, its applications, the workflows, and more. Those were great conversations, essential to the development of hax.

Leading the development of hax was a great and intense experience. I had to engineer a pretty large piece of software, design interesting semantic compiler passes, build debugging tools, do DevOps work, build a playground, and more. I also learned how complicated human interactions can be.

Working at Cryspen

During my time at Cryspen, the proofs and tools team grew a lot. When I arrived, it was Karthik and me. Then Maxime joined towards the end of my first year (in August 2024). In May the next year Clément arrived, and very recently, in November 2025, Alex arrived. I really enjoyed working with everyone in the proofs and tools team at Cryspen!

Beyond the proofs and tools team, it was also great to work with others at Cryspen: Jan, Jonas, Clara.

The Future

After three years working on hax, I decided it was time for me to leave. Hax is a bit my baby, so that was a very hard decision to make.

That said, the rest of the proofs and tools team at Cryspen will continue maintaining, improving, and applying hax to cool real-world Rust projects! They are already working on the new Lean backend, on better libraries, and on very exciting applications!

I'm proud of what hax has become, and I hope it will have a bright future! If hax speaks to you, consider following the project, trying it out, or contributing.