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
- #2104: docs: expand AI guidelines in CONTRIBUTING.md
- #2103: chore: remove legacy lean chacha example
- #2096: fix(hax-lib): resolve
Self::Associn generated pre/post-conditions. - #2095: fix(engine): lazy resolution of UIDs to avoid crashes.
- #2094: ci: use Aeneas's olean cache
- #2093: docs: do not call the sha3 specification an "implementation"
- #2086: Core models extensions.
- #2084: chore: drop currently-unused
#![feature(rustc_private)]from rust-engine - #2082: chore: bump hax-lean pin
- #2081: ci: Free disk space by removing preinstalled packages
- #2079: docs: consistency and cleanup pass across docs and README
- #2078: Update aeneas version
- #2077: fix(core-models): restore a working state for F* proof-libs with extraction from Rust core-models.
- #2076: chore: remove coq examples
- #2075: Make -core-models-lib a default aeneas-lean arg
- #2074: Lean tutorial
- #2070: Update
barrettandadcexamples - #2067: Use core::ops::Deref instead of std::ops::Deref for
refinement_type - #2066: ci: update workflows to work on hax-evit
- #2065: docs: improve hax-lean readme + add license
- #2064: Rename backends
- #2063: [Core-models] Update aeneas version to the latest (with a fixed issue)
- #2062: chore(blog): Write 'This Month in hax'
- #2061: feat: use generated spec in loop_equivalence example
- #2059: feat: use hax_lib::ensures in aeneas-lean loop_example
- #2058: fix: lean_barrett example with aeneas
- #2057: ci: parallelize examples CI
- #2051: feat(cli): update charon aeneas flags
- #2050: feat: unify pins
- #2049: Migrate rust-core-models into hax
- #2047: fix(hax-lib): Fix refinement macro in presence of generics.