FStarLang/FStar v2026.10.18

F* v2026.10.18

on GitHub

What's Changed

• check-friends: use EverParse default (master) branch by @tahina-pro in #4665
• Custard: do not treat admit as unreachable by @gebner in #4666
• Custard: interface-only modules are realized on the ML backends by @gebner in #4668
• Rel: try congruence before unfolding when deciding an equation (#4663) by @nikswamy in #4673
• Cherry: prototype reference-counting C backend for Custard by @gebner in #4667
• Make FStar.Option not a realized module by @funemy in #4676
• Compilation targets: target-specific module files by @gebner in #4660
• Bit vector support: extract, concat, signed arithmetic, overflow checks by @amosr-msft in #4677
• Pulse: join if-branch postconditions without opaque conditional leftovers by @nikswamy in #4648
• SMT encoding: split a query under its context without closing it over gamma by @nikswamy in #4678
• main: let OCAMLRUNPARAM override F*'s GC settings by @nikswamy in #4688
• Core: no SMT query for exhaustive bool matches by @nikswamy in #4680
• Rel: subquadratic binder-set inclusion checks in flex-rigid/flex-flex solving by @nikswamy in #4681
• Pulse: with_context renders context strings once and pushes them in one go by @nikswamy in #4685
• Tactics: early-exit no_uvars_in_term / no_univ_uvars_in_term by @nikswamy in #4686
• Normalizer: decide FStar.UInt.size / FStar.Int.size on constants by @nikswamy in #4679
• Upgrade default Z3 to 5.3.0 (F* release candidate) by @nikswamy in #4654
• Custard: compile an empty match to EUnreachable by @gebner in #4691
• Custard: avoid plugin module collisions on load (#4692) by @gebner in #4693
• Require an implementation or model for every library interface by @gebner in #4694
• Cap rlimit by @nikswamy in #4696
• Replace realized OCaml modules with F* implementations and custard_extern FFI by @gebner in #4690
• Custard C: rename clashing static names instead of rejecting by @gebner in #4698
• Custard: generate krml closer to the legacy Pulse extraction by @gebner in #4699
• Cherry: implement FStarC.Hash in F* by @gebner in #4702
• Cherry: clean-room FStar.Pprint in F* by @gebner in #4703
• Bump version to 2026.10.18 by @dzomo in #4706

New Contributors

• @funemy made their first contribution in #4676

Full Changelog: v2026.10.11...v2026.10.18