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
- #2010: refactor: prettier barrett example
- #2005: fix(lean): make the proof of RustM.toBVRustM_bind compatible with Lean 4.29.0
- #2002: feat(lean): add resugaring for ellipsis in pattern-matching
- #2001: fix(exporter): support ellipsis patterns by adding wildcards
- #2000: feat(lean): derive Repr, BEq, DecidableEq for tuples
- #1998: This month in hax blog post 2026 03
- #1996: Rename GenericConstraint::Type to TypeClass and ::Projection to Equality
- #1995: fix(lean): fix core models extraction
- #1994: refactor: redefine RustM monad using ExceptT Error Option
- #1991: fix: remove monad_extract_simplify
- #1972: nix: fix development shell