This Month in Hax: February 2026
In February, we successfully merged 32 pull requests!
This month, the Lean backend made headway by getting new Rust proof attributes. With the new attributes, Users can choose between two proof methods, one based on symbolic reasoning (grind) and one based on bit-blasting (bv_decide). This new setup is illustrated in our updated Tutorial
and the Chacha20
example. Moreover, the Lean backend produces
prettier output by opening namespaces, handles for-loops more reliably, and its library contains more of our Rust core models.
We also made great progress on our new THIR importer, implemented in Rust. Currenlty, it can be activated using --experimental-full-def, and we intend to make it the default soon.
Special thanks to @JuanCoRo, @klausnat, and @rusch95 for their contributions this month!
Full list of PRs
- #1967: Evit upstream january 2026
- #1962: feat(lean): bump to Lean v4.29.0-rc1
- #1961: Apply resugarings to linked items.
- #1959: ADC example. documented
- #1956: feat(lean_chacha20): use new attributes
- #1955: Lean cleanup
- #1954: fix(lean): print "do" in all ITE & match-branches
- #1951: feat(lean): for-loops for all unsigned integers
- #1950: Remove
BinOpresugaring - #1947: [doc] Add AI contribution guidelines
- #1946: feat(lean): detect recursive functions and mark them
partial_fixpoint - #1943: feat(lean): prettier proof_mode annotations
- #1942: feat(lean): Rust primitives for prop
- #1941: fix(lean): default value for associated constants are pure.
- #1938: New default proof for the Lean backend & proof method attribute
- #1937: feat: communicate specs to mvcgen
- #1936: doc: add
lean-toolchainfile to quick start - #1935: Render suffixes in the rust engine and backends.
- #1934: fix(lean): Support functions without arguments in specs
- #1933: feat(lean): Separate symbolic and bit-blasting specs
- #1932: fix(lean): Extract correct
PhantomDatastructure - #1931: feat(lean): attributes for pureEnsures/pureRequires
- #1929: [Lean] Fix monadic phase bug with constants
- #1927: lean: keep Rust crate/module names unchanged
- #1925: feat(lean): add type annotation for cast_op
- #1919: feat(lean): Extract more core models
- #1918: fix(lean): support for opaque structs
- #1909: feat(lean): assoc types with constraints and inheritance
- #1908: This month in hax blog post 2026 01
- #1906: Resugaring for associated constants from associated functions without parameters
- #1901: feat(lean): Add support for namespaces (resurrected old PR)
- #1834: fix(lean): escape special characters in string literals