The world of mathematics has been shaken by an earthquake: LLMs can now generate large Lean developments autonomously: Navier-Stokes solution, FLT proof, and many more. The narrow stream of proof-work has the potential to open into a free-flowing river.

This offers a promise for software verification: what used to require multi-year effort by skilled teams might become more broadly available, provided that the flow can be tamed into useful ways, that is, that formal verification toolchains adapt and improve.

We’ve been updating and improving hax, our Rust verification framework, to leverage this newfound potential. With Rust being a popular choice for AI-written code, and with Lean seeing rapid adoption and tooling investment, we believe our Rust-to-Lean pipeline could play a key role in improving confidence in many critical codebases.

We’re proud to announce the 0.4 release of hax.

TLDR: We improved hax to:

• have a greater reach by expanding its support for the Rust language
• be more broadly accessible to users

This new release achieves that through:

• the collaboration with Aeneas as our new engine for the Rust→Lean pipeline
• a new streamlined installation and setup

For more technical details on the release, see the companion post on the hax blog. You can also try hax online!

Adopting Aeneas for the Lean backend

Hax was from the beginning thought of as a multi-backend tool, i.e. targeting several proof assistants, even though historically, F* was our preferred option. We added a new Lean backend over the course of 2025, which gave us interesting insights and promising results.

While the collaboration with the Aeneas team, which started at Inria, was still ongoing on the frontend side of hax and Charon, we decided in early 2026 to pivot and directly use the Charon+Aeneas pipeline as the translation engine for our Lean backend. Since then, we’ve been increasing our collaboration, contributing bug fixes and improvements.

While the Charon+Aeneas pipeline was made available in 0.3.7, the 0.4 release makes it officially our main Lean backend. This increases support for Rust, notably functions returning mutable borrows. Here is an example from the OpenMLS codebase, one of our ongoing proof efforts, that was previously rejected by our engine:

pub fn node_mut(&mut self) -> &mut Option<ParentNode> { ... }

Functionalizing calls to such a function, say let x = n.node_mut(), is non-trivial: it requires inserting “backward functions” at the end of the lifetime of x to “update” the value of n. Those backward functions must be computed from the code and inserted at the right locations. This is the role of the Aeneas translation.

The hax workflow

Proving properties of Rust code is not only about translation. This release also packages various extensions to Aeneas, to support the key design choices and workflows of the hax way:

• a strong library of Rust-written models for core/std/alloc
• a set of macros for writing specs directly in the code
• and use of Lean’s built-in mvcgen tactic as our main proof framework

All tools verifying Rust code have to handle its dependencies: compiler intrinsics, core/std/alloc libraries. Often, it is done by providing a hand-written model directly in the prover, say Lean for instance. This is usually error-prone, hard to audit, hard to extend and backend-specific. To solve those issues, we’ve been developing a Rust-written library of models for core. They are easily extensible, backend-agnostic, and heavily tested against their real core counterparts. Those models rely on a small, well-defined set of primitives that have to be modeled in the library of each backend. We’re very excited about the progress there; we’ll cover it in more detail in an upcoming post.

A key part of the hax methodology is the collocation of code and specs: we encourage writing the specs alongside the code, directly in Rust (when applicable). We extended Aeneas with preliminary support for those (restricted to pre/post on standalone items for now). This eases review and sync of code and proofs.

Finally, we decided to adopt the mvcgen tactic as our entry point for actual proofs. We believe in using standard, community-backed tools as much as possible. The development speed of mvcgen is astonishing, and we’ve already used it in large-scale proofs with great success.

A streamlined installation and setup

A key friction point for formal verification tools is usually installation, setup, and maintenance. With this release, hax 0.4 is available directly with cargo install cargo-hax (or via a binary installation). Once installed, hax handles the other dependencies (Charon+Aeneas) seamlessly for the user, via the versatile command cargo hax tools (fetching the binaries, managing versions, etc.). See the manual for more details.

All the relevant settings for verification can now be stored in a single, version-controlled, crate-level file hax.toml. In that file, the user can define proof scenarios, with a specific backend, that target a subset of the crate. This is key to enabling extensible verification, or to target different properties with different backends.

Trust & assumptions

Hax makes assumptions, and there are certainly bugs in the hax codebase or in dependencies. We aim to document our trusted computing base, publish in open-source and test our toolchain comprehensively. Notably:

• Hax depends on open-source tools (Cargo, rustc, Lean, F*, Aeneas) that are backed and scrutinized by a community. Hax 0.4 targets Lean v4.31.0, which has some known soundness bugs. Upgrading the Lean version is planned for the next release.
• We rely on our modeling of Rust primitives and our core models being faithful to the rustc implementation. We mitigate the risk of mismatch by heavily testing them.
• Issues can hide in the overall workflow: flawed specs, excluded code, ignored theorems, etc. We are building tools to surface the TCB for every hax project.

We welcome feedback and findings to continuously improve the trustworthiness of the toolchain.

Conclusion

Hax 0.4 is a pivotal moment for Cryspen, leveling up to the challenges ahead. The next release will contain a new ProVerif backend, increase overall robustness and improve proof engineering.

For more details on hax 0.4, look at the companion blog post on the hax blog, the docs, or the hax repo.

Stay tuned for hax 0.5!