This Month in Hax: October 2025
In October, we successfully merged 15 pull requests!
The Rust engine and Lean backend gained a monadic phase that wraps pure values and binds computations through pure and lift insertions, ensuring that the Lean backend faithfully uses the Lean Result monad.
A rejection phase was added to enforce Lean's do-notation DSL, preventing interleaving of expressions and statements and providing clearer diagnostics.
We also introduced a FunctionsToConstants resugaring: Lean can now extract values from Rust consts using helper functions, guaranteeing panic-free constant evaluation.
Struct updates are now supported via base-expression syntax, and we refactored the printer traits to return static document builders, improve span handling, and simplify lifetimes.
The F* proof libraries now include a better VecDeque model and several fixes; loops without mutation are now accepted.
The Lean backend also gained improved error messages and a refactored proof library.
Stay tuned for more updates next month!
Full list of PRs
- #1746: feat(rust-engine/lean): monadic phase
- #1739: feat(rengine, lean): add rejection phase that ensures an expression is in the Lean do-notation DSL
- #1738: feat(lean): Use
FunctionsToConstants - #1737: This month in hax blog post 2025 09
- #1736: feat(lean): add support for base expression of structs
- #1735: refactor(rengine): revisit printer traits
- #1733: Fix rustc coverage tests.
- #1732: Accept loops without mutation.
- #1730: Add nightly CI job for ML-DSA lax-checking.
- #1729: Release 0.3.5
- #1728: Better VecDeque model and other F* proof lib improvements/fixes.
- #1726: Switch hax-lib to Rust edition 2021.
- #1724: fix(engine): fix owner_id
- #1717: [Lean] Proper error messages
- #1696: proof-libs/lean Library update and refactor