This Month in Hax: November 2025
In November, we successfully merged 16 pull requests!
The frontend continues getting improvements thanks to @Nadrieril.
So does the lean backend, with support for default methods and lib improvements including renaming the Result monad to RustM.
The lib has been the focus as we now have started incorporating the new core models written in Rust.
A first batch of changes already happened in November and are automatically extracted to the F library (manually for lean).
We continue the development of these models which will hopefully cover all we already have in the F lib as manual F* models.
Full list of PRs
- #1778: Change impl_u64__rotate_right second parameter type to u32
- #1777: feat(lean): add support for default methods
- #1775: docs(blog): add avatar pictures locally
- #1770: Update author avatars in .authors.yml
- #1769: Fix broken links in README.
- #1768: refactor(lean): rename Result to RustM
- #1767: fix(engine/fstar): print [Fstar.Char.char] instead of [char]
- #1765: Incorporate charon changes to the frontend
- #1754: chore(examples): reserve extraction folder for auto-generated files
- #1752: fix(docs): fix a few typos in tutorial
- #1751: fix(gha): fix this month in hax template: drop extra
**markdown - #1750: This month in hax 2025-10
- #1749: Merge hax-evit approved changes
- #1747: feat(proof-lib/lean) core models
- #1743: chore(deps): bump playwright and @playwright/test in /docs/.test
- #1742: [F* lib] Tls codec panic freedom