What is the connection between Aeneas and Hax?

Stream: Program verification

[Oliver Butterley]

When using Aeneas with the Lean back end, it seems to use Hax. But Hax can also be used independently to produce Lean code for verification purposes?

[Clément Blaudeau]

Aeneas uses the Hax frontend, that queries rustc to extract the THIR or MIR representations. Then, both Aeneas and Hax produce code for different backends. The main difference comes from the fact that Hax targets the Thir representation, while Aeneas targets Mir (and they don't do the same code transformations)

While Aeneas has put a focus on Lean for a long time, Hax was more designed towards F* and Rocq/Coq (among others). Recently, we've been developing a Lean backend for Hax, that happens to borrow some definitions from Aeneas.

[Clément Blaudeau]

(Keeping in mind that the Hax backend for Lean is 1 month old, while the Lean backend of Aeneas has been developed for several years)

[Oliver Butterley]

Thanks, that already clarifies a lot.

Is it possible to say briefly if there is likely to be a different way that identical rust will be represented in lean?

[Oliver Butterley]

Clément Blaudeau said:

(Keeping in mind that the Hax backend for Lean is 1 month old, while the Lean backend of Aeneas has been developed for several years)

Indeed!

[Clément Blaudeau]

There are/will be two sets of differences :

1. The Lean representation of Rust primitives/intrinsics in Aeaneas and Hax might be different (although some effort is likely going to be put in trying to merge/reuse some definitions and interfaces). For instance, Aeneas has a custom integer type for i32, while Hax uses Lean's Int32. Depending on what you're using the extracted code for, that might or might not make a difference. Hax uses the recent additions to Lean.Std.Do for specifications, while Aeneas has a custom wp notion (with some impressive engineering in tactics) that predates it
2. The phases that transform the Rust code are different in the engine of Hax and Aeneas. Loops, mutability, borrowing, etc. are not treated in the same way, and this difference would show in the extracted code

[Bas Spitters]

In addition to this. Hax has already been used for many more applications than Aeneas; see https://hax.cryspen.com/publications/
Including our recent multi-prover verification of a PQ TLS implementation, accepted at CCS: https://eprint.iacr.org/2025/980
We have also used it for smart contract verification. A paper is under submission.

Historically, Hax has been designed to verify security critical (cryptographic) rust software in Rust, whereas Aeneas aimed for a wider fragment of the rust language.
Interestingly, @Son Ho is currently working on verifying cryptographic implementations, whereas Hax is extending the fragment of the rust language it is supporting.

[Son Ho]

Yes, hax and Aeneas have quite different translation mechanisms. Aeneas actually used to be completely independent of hax, but we decided to port the code which directly interacts with rustc into the hax frontend, with the hope of sharing code and engineering effort. In practice we have mostly been extending the hax frontend so that it can support MIR, but we hope sharing this code has benefits in the future.
We have put a strong focus into designing a translation mechanism which is expressive and principled. As a result, Aeneas can support some complex patterns like functions returning mutable borrows in all generality, while as far as I know hax had to hardcode support for some such patterns, to support iterators for instance (I'm curious about the work on extending the fragment supported by hax @Bas Spitters ). Part of the translation performed by Aeneas has also been formalized and proven correct (to be more precise, we have a proof that the symbolic execution performed by Aeneas, which is at the core of the translation, implements a borrow-checker, and we plan to extend this proof to have a correctness theorem about the generated code).
We are currently applying Aeneas to the verification of the open source cryptographic library of Microsoft, which is notably used in Windows and Azure Linux: we're porting the code from C to Rust, and verifying it in Aeneas. Microsoft published a blog post about this effort: https://www.microsoft.com/en-us/research/blog/rewriting-symcrypt-in-rust-to-modernize-microsofts-cryptographic-library/
Cryptographic code is only our first target, and we're in the process of extending the translation to support a larger class of programs. In particular, we're currently working on connecting the pure translation to a separation logic framework to make it possible to reason about unsafe and concurrent code.

[Son Ho]

Oliver Butterley said:

it seems to use Hax.

What made you think it uses hax by the way?

[Oliver Butterley]

Son Ho said:

Oliver Butterley said:

it seems to use Hax.

What made you think it uses hax by the way?

At some point there was an error message produced that mentioned Hax. I think it was when I hadn't properly installed some of the requirements and I think it was when running Charon but I don't remember precisely.

[Oliver Butterley]

Thanks @Bas Spitters and @Son Ho for the details related to Hax versus Aeneas. That really helps a lot getting an understanding of the two options.

[Bas Spitters]

@Oliver Butterley out of curiosity, what are you trying to prove about what rust code?

[Oliver Butterley]

Bas Spitters said:

Oliver Butterley out of curiosity, what are you trying to prove about what rust code?

I was searching for a way to verify Rust code which works well both for low level bit operations and can also express rather sophisticated mathematical properties. Of course all of that together is a big ask!

I was experimenting with a function from curve25519-dalek and it's not too hard to prove the relevant properties in Lean after extracting with Aeneas its Lean form.

In general I was rather impressed how it could be done and the Lean proof wasn't harder that proving the same in Verus even though I didn't get any advantage from grind on this occasion. I used heavily Aeneas' progress as rather than stuff from Lean's Std.do. I suspect there will be improved ways to do some of this as the Lean libraries expand and Aeneas is pinned to a more recent version of Lean.

Next I'll try Hax -> Lean with the same function to see how it goes.

[Oliver Butterley]

Given the same Rust code, how similar will the Lean version of the code be?

[Bas Spitters]

@Oliver Butterley I'm looking forward to the comparison.
In general, for efficient verified curve operations, I would likely take the fiat-cryptography route, which uses a verified compiler:
https://github.com/mit-plv/fiat-crypto/tree/master/fiat-rust

I should be possible to connect this compiler with Lean. We're looking at some options of how to do that, but that might take some time...

In general, I would expect Hax code (eventually) to be simpler, is the current semantics Hax is functional. Aeneas supports a bigger subset of rust, which needs a bi-functional semantics: https://aeneasverif.github.io/publications/

However, it is possible for Aeneas to use stactic analysis and use the functional semantics if appropriate for a specific rust program. I am not sure this is currently done. @Son Ho ?

[Oliver Butterley]

Thanks for the info!

[Son Ho]

Oliver Butterley said:

Bas Spitters said:

Oliver Butterley out of curiosity, what are you trying to prove about what rust code?

I was searching for a way to verify Rust code which works well both for low level bit operations and can also express rather sophisticated mathematical properties. Of course all of that together is a big ask!

I was experimenting with a function from curve25519-dalek and it's not too hard to prove the relevant properties in Lean after extracting with Aeneas its Lean form.

In general I was rather impressed how it could be done and the Lean proof wasn't harder that proving the same in Verus even though I didn't get any advantage from grind on this occasion. I used heavily Aeneas' progress as rather than stuff from Lean's Std.do. I suspect there will be improved ways to do some of this as the Lean libraries expand and Aeneas is pinned to a more recent version of Lean.

Next I'll try Hax -> Lean with the same function to see how it goes.

I'm happy to hear that you were successful doing this experiment! About progress: we've been following the development of Lean's Std.do very closely and we're definitely interested in using it in the future, but on the other hand maintaining our own version of progress gives us some freedom in doing experiments. For instance, you may have noticed that progress* repeatedly applies progress while progress*? generates the corresponding proof script, which is quite convenient to quickly get into the core of the proof. We are also working on more interesting extensions.
About grind: we intend to use it in the very near future, but we need to annotate our standard library with grind attributes first (it is not difficult, just a bit boring).
Also note that we have developed a collection of tactics to make the proof interaction easier. For instance:

• scalar_tac is a more powerful version of omega
• simp_{lists,scalar,lists_scalar} is an optimized version of simp which uses scalar_tac as a discharger together with specific simp sets to simplify goals containing lists and integers. They're very useful to reason about programs containing arrays (to simplify things like get (set a i) j) or performing non-linear arithmetic operations (to simplify things like a % b = a), and both of those are all over the place in cryptographic code.
• bvify n, natify, zmodify do the same as zify but target BitVec, Nat and ZMod, etc.

About the complexity of the translation: yes indeed, Aeneas uses backward functions only when needed (that is when translating functions which return mutable borrows). This is not based on static analysis: it is simply based on the signature of the functions we translate. So I believe Hax and Aeneas' output should mostly coincide on the subset they have in common. It is possible that Hax output is more respectful of the original control-flow, though, as it consumes the THIR rather than the MIR.

[Oliver Butterley]

Thanks, @Son Ho

I missed the possibility of progress*?, it's good to know! I found progress did the job well for everything I saw so I have no complaints.

I was very happy to discover bvify n, it's great.

I should experiment more with scalar_tac and the enhanced versions of simp. I didn't yet since I could solve my goals without and didn't easily find documentation about them. Another time I'll did deeper.

One day soon there will be a "Verifying Rust in Lean" book, along the lines of Theorem Proving in Lean and Mathematics in Lean then we will all get and easy way into this activity.

By the way, the availability of the lean examples (although buried a little deep in the Aeneas repo) was great for getting start. More examples are always good!

[Clément Blaudeau]

We're adding lean examples (and documentation) to the hax tutorial right now, they should be available in the coming days/weeks!

[Bas Spitters]

Thanks @Son Ho. I'm hoping Hax can reuse some of the clever tactics you've already provided for Aeneas.

[Son Ho]

Oliver Butterley said:

Thanks, Son Ho

I missed the possibility of progress*?, it's good to know! I found progress did the job well for everything I saw so I have no complaints.

I was very happy to discover bvify n, it's great.

I should experiment more with scalar_tac and the enhanced versions of simp. I didn't yet since I could solve my goals without and didn't easily find documentation about them. Another time I'll did deeper.

One day soon there will be a "Verifying Rust in Lean" book, along the lines of Theorem Proving in Lean and Mathematics in Lean then we will all get and easy way into this activity.

By the way, the availability of the lean examples (although buried a little deep in the Aeneas repo) was great for getting start. More examples are always good!

Yes, I need to document all this better and rewrite the tutorial but I've been overwhelmed with other things. ^^'
About bvify n: I also wrote a wrapper bv_tac n which calls bvify then bv_decide.

That's a good remark: we need to add more examples in the repo. I'm hoping to take some time in the near future to minimize some examples about verified code we're working on right now to exemplify the use of all those tactics on cryptographic code.