Skip to content

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