This Month in Hax: January 2026
In January, we successfully merged 29 pull requests!
The Lean backend continues to get improvements, mostly thanks to @abentkamp! We now have more specs in the proof library (for while loops, negation and more), and improved tactics to reason with our annotations of pre/post-conditions (#1888). Some naming fixes, and improvements of the handling of associated types make us closer to reaching parity with the F* backend!
The other significant improvements are on the core models side. Thanks to some new models, the F* proof library is now entirely extracted from Rust core models. The Rust primitives models will remain hand-written in each backend, but they have been designed to be as small as possible, and are intended to be modelled in a very backend-specific way. The Lean library is now also partly extracted from core models! Some modules are excluded for now as they rely on Rust features that we don't support in the Lean backend for now. We will prioritize these missing features in the next few months to extend the Lean library using extraction from core models.
Full list of PRs
- #1902: Fix broken dependabot links
- #1900: feat: bump lean to v4.28.0-rc1
- #1899: Various core models fixes.
- #1898: Upstream Evit changes up to 24 dec 2025
- #1896: fix(lean): more generous timeout for bvdecide
- #1895: refactor(lean): rearrange lean lib file structure
- #1891: feat(lean): spec for negation
- #1888: feat(lean): hax_zify and hax_construct_pure tactics
- #1887: feat(lean): support for opaque impls
- #1885: [Lean] add Core_models.Slice.Impl.is_empty
- #1875: set cfg for docs.rs
- #1872: refactor(ci/nix): clean up a bit frontends cli src
- #1870: Release 0.3.6
- #1869: Blog post about my departure from Cryspen (and hax)
- #1868: OCaml engine: export namespace insensitive sort, make Lean use it
- #1867: fix(lean): escape keywords systematically
- #1865: feat(lean): core models
- #1864: docs(blog): Verifying a while loop in Hax/Lean
- #1863: feat(lean): add negated condition to while loop spec
- #1860: Lean: correctly call
fn_like_linked_expressions, fixingself_->self - #1857: feat(lean): Add support for while loops
- #1851: fix(lean): associated type projections on multiple parameters
- #1850: fix(lean): fix rendering of impl items with constraints
- #1849: feat(lean): preliminary core model extraction
- #1848: fix: replace macro should not affect other backends
- #1846: feat(lean): Add support for
#[hax_lib::opaque] - #1840: feat(lean) turn rejection phase into a transformation phase
- #1837: [lean] add casting for all integer type pairs
- #1822: feat(lean): Define usize as a newtype of UInt64