Write This Month in Hax

[github-actions[bot]]

This is an auto-generated issue for the "This Month in hax" blog series.

Branch this-month-in-hax-blog-post-2025-10 have been created with the following template:

---
authors:
  - clement
title: "This Month in Hax: October 2025"
date: 2025-11-01
---

In October, we successfully merged **15** pull requests**!

<DESCRIPTION>

### Full list of PRs
* \#1746: [feat(rust-engine/lean): monadic phase](https://github.com/cryspen/hax/pull/1746)
* \#1739: [feat(rengine, lean): add rejection phase that ensures an expression is in the Lean do-notation DSL](https://github.com/cryspen/hax/pull/1739)
* \#1738: [feat(lean): Use `FunctionsToConstants`](https://github.com/cryspen/hax/pull/1738)
* \#1737: [This month in hax blog post 2025 09](https://github.com/cryspen/hax/pull/1737)
* \#1736: [feat(lean): add support for base expression of structs](https://github.com/cryspen/hax/pull/1736)
* \#1735: [refactor(rengine): revisit printer traits](https://github.com/cryspen/hax/pull/1735)
* \#1733: [Fix rustc coverage tests.](https://github.com/cryspen/hax/pull/1733)
* \#1732: [Accept loops without mutation.](https://github.com/cryspen/hax/pull/1732)
* \#1730: [Add nightly CI job for ML-DSA lax-checking.](https://github.com/cryspen/hax/pull/1730)
* \#1729: [Release 0.3.5](https://github.com/cryspen/hax/pull/1729)
* \#1728: [Better VecDeque model and other F* proof lib improvements/fixes.](https://github.com/cryspen/hax/pull/1728)
* \#1726: [Switch hax-lib to Rust edition 2021.](https://github.com/cryspen/hax/pull/1726)
* \#1724: [fix(engine): fix owner_id](https://github.com/cryspen/hax/pull/1724)
* \#1717: [[Lean] Proper error messages](https://github.com/cryspen/hax/pull/1717)
* \#1696: [proof-libs/lean Library update and refactor](https://github.com/cryspen/hax/pull/1696)

### Contributors
* [@W95Psp](https://github.com/W95Psp)
* [@clementblaudeau](https://github.com/clementblaudeau)
* [@maximebuyse](https://github.com/maximebuyse)

It is an skeleton blog post with the list of PRs pushed in October 2025 and a list of contributor.

Suggested person to pick this draft PR: @clementblaudeau

Action Items

• [x] Write the blog article
• [ ] Release a new version of hax
  • [ ] Follow PUBLISHING.md
  • [ ] Create Github release

[W95Psp]

Release is currently waiting for #1742 to be merged