### Fixed - **Windows compatibility** — three Windows-specific bugs surfaced when PR #639 added `windows-latest` to the CI test matrix in advisory mode (`continue-on-error`). All three close in this release, and the matrix flips to fully strict (Windows entries are now merge gates alongside Ubuntu / macOS): - **[#640](https://github.com/aallan/vera/issues/640)** — Vera CLI's `/dev/stdin` path is Unix-only. `_load_and_parse(path)` in `vera/cli.py` previously called `Path('/dev/stdin').read_text()`; on Windows the path doesn't exist as a filesystem entry and `vera <subcmd> /dev/stdin` failed with `Error: file not found: /dev/stdin`. Now reads from `sys.stdin` directly when `path in _STDIN_PATHS` — portable across Unix and Windows, and more semantically correct (the user's intent is "read from stdin", not "read from a specific file path"). Closes 6 failing tests in `tests/test_cli.py::TestStdinInput`. - **[#641](https://github.com/aallan/vera/issues/641)** — default cp1252 file I/O encoding caused `UnicodeEncodeError` / `UnicodeDecodeError` on Windows for tests reading or writing files containing `→` or `—` characters. Set `PYTHONUTF8=1` in the CI test job environment so Python's text-mode `open()` defaults to UTF-8 regardless of locale (PEP 540), and added explicit `encoding='utf-8'` to `vera/parser.py`'s grammar load (the load-bearing site that runs on every parse). Closes ~9 failing tests across `test_codegen.py`, `test_codegen_monomorphize.py`, `test_codegen_closures.py`, `test_html.py`. Broader audit of `open()` / `read_text()` / `write_text()` call sites for explicit `encoding='utf-8'` queued as a follow-up — for now CI is covered via `PYTHONUTF8=1`, and locally users on Windows without `PYTHONUTF8=1` may still hit the bug on individual files. - **[#642](https://github.com/aallan/vera/issues/642)** — `tests/test_codegen.py::TestIOOperations::test_io_read_file_success` and `test_io_read_file_roundtrip` embedded Windows tempfile paths (e.g. `C:\Users\runner\AppData\...`) into Vera string literals via f-string interpolation. Vera's grammar correctly rejected `\U` as an invalid escape sequence, producing `[E009]` at parse time. Fix in test fixtures: convert the path to POSIX form via `tmp_path.replace(os.sep, '/')` before embedding (Windows file APIs accept forward slashes). ### Changed - **CI test matrix is now fully strict on Windows.** PR #639's advisory `continue-on-error: ${{ matrix.os == 'windows-latest' }}` is removed in this release — the three Windows entries (`{3.11, 3.12, 3.13}`) now block merges alongside Ubuntu and macOS. Total matrix coverage: 9 entries (3 OSes × 3 Python versions).

### Fixed - **Tail-call optimization for non-allocating tail-recursive functions** ([#517](https://github.com/aallan/vera/issues/517), closes) — pre-fix, every Vera `call` site emitted a plain WASM `call` regardless of tail-position status, so a tail-recursive function pushed one WASM frame per iteration and trapped with `call stack exhausted` at ~tens of thousands of frames. The documented "iteration is tail recursion" idiom from `SKILL.md` thus silently failed past ~5–10K iterations. The fix is a per-fn analyzer (`vera/codegen/tail_position.py`) that marks `id(FnCall)` AST nodes in syntactic tail position; `_translate_call` emits `return_call $foo` instead of `call $foo` when the call's id is in the marked set AND the callee's WASM return type matches the caller's (required for WASM `return_call` semantics — the signature must match). Non-allocating tail-recursive functions now run in **constant stack space**: the canonical `count_down(50000)` reproducer succeeds, as does a 1M-iteration stress test. ### Tail-position analysis - **Marking rules** (recursive on the function body): - The body's trailing expression IS in tail position. - If a sub-expression is in tail position and is an `IfExpr`, both branch bodies are in tail position. The condition is NOT. - If a sub-expression is in tail position and is a `MatchExpr`, every arm body is in tail position. The scrutinee is NOT. - If a sub-expression is in tail position and is a `Block`, only the trailing expression is in tail position. Statement values (`let` initialisers, `ExprStmt` expressions) are NOT. - All other constructs (call arguments, quantifier bodies, `assert`/`assume`, `handle` bodies, `AnonFn`, indexing) are NOT tail-transparent — calls inside them are not in tail position regardless of the parent's status. - **Type-safety guard at emit time:** WASM `return_call` requires the callee's signature to match the caller's, so the translator falls back to plain `call` whenever the resolved callee's WASM return type doesn't match the current function's return type. The recursive case (call to the same function) trivially matches; cross-function tail calls match when signatures align. ### Allocating-function fallback - **Allocating functions revert `return_call` → `call`** in a post-process step at the end of `_compile_fn`. WASM `return_call` discards the current frame, which means the GC epilogue (restore `$gc_sp`, unwind shadow-stack pointer slots) never runs. For an allocating function with tail calls, that leaks shadow-stack slots once per iteration and would eventually trap on the next `$alloc` once `gc_sp` passes the worklist boundary — strictly worse than the pre-fix "stack exhausted" trap. Until full GC-aware tail-call support lands ([#549](https://github.com/aallan/vera/issues/549) tracks the follow-up), allocating functions pay the WASM frame cost in exchange for correct shadow-stack management. Non-allocating functions (the common iteration-style tail recursion case) keep the optimization. ### Tests - New `TestTailCallOptimization517` in `tests/test_codegen.py` (9 tests): 50K-iteration behavioural test (the issue's canonical reproducer), 1M-iteration stress test (pins constant-stack-space behaviour rather than just "deeper than the broken limit"), structural assertion that `return_call $count_down` appears in WAT for the recursive call, structural assertion that a let-bound (non-tail) call emits plain `call`, allocating-function fallback assertion (allocating tail-recursive function emits plain `call` not `return_call`), plus 4 analyzer unit tests covering each tail-transparent construct (Block trailing, both branches of IfExpr, let-value NOT marked, call args NOT marked). - Existing fixtures in `tests/test_runtime_traps.py` updated for the TCO interaction: the `_DIVIDE_BY_ZERO_USER_FN`, `_CONTRACT_VIOLATION_PROGRAM`, and `_DIVZERO_FOR_FIX` test programs originally had `main` calling the trapping function in tail position, which #517 would now optimize away — discarding `main`'s frame and shortening the backtrace assertions expect to see. The fixtures now bind the call result with `let` and produce it via slot reference, keeping the call non-tail and preserving `main`'s frame on the WASM call stack. Comments document the intentional non-tail shape so a future contributor doesn't "simplify" them back into tail position. ### Improved - **`stack_exhausted` trap Fix paragraph rewritten** to reflect the v0.0.126 reality. Pre-rewrite: "Vera doesn't yet emit `return_call` ... wait for #517 to ship". Post-rewrite: "Vera compiles tail-position calls to WASM `return_call` ... if you're still hitting this trap the recursion isn't actually in tail position. Restructure with an accumulator parameter so the recursive call is the LAST thing the function does (no work after it, no `let`-binding of its result, no enclosing arithmetic). Allocating functions are an exception ... iterate via `array_fold` / `array_map` (which compile to WASM loops rather than recursion)." ### Documentation - **KNOWN_ISSUES.md** — #517 row removed (closed); new row added pointing at [#549](https://github.com/aallan/vera/issues/549) (GC-aware TCO follow-up for allocating functions, with restructure/array-fold workarounds). - **ROADMAP.md** — #517 dropped from the bug-killing campaign queue (closed by this release); intro updated to "eight remain"; priority rows renumbered (#520 promoted to position 1).

### Added - **`Random` effect for non-deterministic value generation** ([#465](https://github.com/aallan/vera/issues/465)) — new built-in `Random` effect with three operations: `Random.random_int(@Int, @Int) -> @Int` (inclusive range), `Random.random_float(@Unit) -> @Float64` (uniform `[0.0, 1.0)`), `Random.random_bool(@Unit) -> @Bool`. Functions drawing random values must declare `effects(<Random>)`, making non-determinism visible in the type signature. Python runtime backs onto `random.randint` / `random.random()`; browser runtime backs all three onto `Math.random()` (fast, non-cryptographic, adequate for games and simulations). No seeding API yet — `handle[Random]`-based deterministic testing is future work. Unblocks games, simulations, shuffling, Monte Carlo methods, and randomized initial states (Conway's Life soup, etc.). Conformance: `ch07_random_effect.vera`. Closes [#465](https://github.com/aallan/vera/issues/465).

### Fixed - **GC shadow stack overflow causing silent array corruption** ([#464](https://github.com/aallan/vera/issues/464)) — the 4K shadow stack overflowed into the GC worklist during deep recursive array accumulation (450+ frames), causing silent corruption of the first array elements. Shadow stack increased to 16K with overflow guard trap. 3,253 tests.

## What's new ### Added - **Mistral AI provider for the Inference effect** ([#413](https://github.com/aallan/vera/issues/413)) — `Inference.complete` now supports Mistral models. Set `VERA_MISTRAL_API_KEY` to use; default model is `mistral-small-latest`. ### Changed - **Provider registry refactor** — `_call_inference_provider()` and auto-detection in `execute()` are now table-driven via a `_ProviderConfig` dataclass and `_PROVIDERS` registry dict, replacing the `elif` chain. Adding further providers (Grok, DeepSeek, Gemini) is now a one-row change. `_call_inference_provider` signature simplified from six parameters to four. - **Early-fail guard** — `execute()` now returns a clear `Err` immediately when a provider is explicitly set via `VERA_INFERENCE_PROVIDER` but its API key env var is missing, rather than making a live HTTP request with an empty key. - **Kimi brand update** — docs updated to reflect Moonshot's developer portal migration from `platform.moonshot.ai` to `platform.kimi.ai`. API endpoint (`api.moonshot.ai`) and `VERA_MOONSHOT_API_KEY` are unchanged. Full changelog: https://github.com/aallan/vera/blob/main/CHANGELOG.md

## Fixed - **Type inference for bare `None`/`Err` constructors in generic combinator calls** ([#293](https://github.com/aallan/vera/issues/293)) — `option_unwrap_or(None, 99)`, `result_unwrap_or(Err("oops"), 0)`, and `option_map(None, fn(...) {...})` now type-check and compile correctly without requiring a typed `let` binding workaround. Three-layer fix: (1) the checker's fresh-TypeVar overwrite rule; (2) the monomorphizer's sparse-constructor field-to-type-param mapping; (3) added missing `StringLit` / `InterpolatedString` / `ArrayLit` cases to the monomorphizer's type inferencer. Closes [#293](https://github.com/aallan/vera/issues/293). - **`Exn.throw()` qualified form now compiles correctly** ([#430](https://github.com/aallan/vera/issues/430)) — `Exn.throw(@Int.0)` passed `vera check` and `vera verify` but crashed at WASM runtime with `unknown func: $vera.throw`. The qualified call path now correctly dispatches user-defined effect ops (`Exn.throw`, `State.get`, `State.put`) through the effect_ops table rather than falling through to a host import call. The dispatch also guards against built-in qualifiers (`Http`, `Inference`, `IO`) to prevent future naming collisions. Closes [#430](https://github.com/aallan/vera/issues/430). - **`grammar.lark` missing from wheel** ([#429](https://github.com/aallan/vera/pull/429)) — `pip install git+https://github.com/aallan/vera` silently omitted `grammar.lark` from the built wheel, causing an immediate crash on import. ## Added - Conformance test `ch09_none_err_inference.vera` (level: run) covering all four bare-constructor inference cases. - Citation section in README.md.

## Json standard library type Closes [#58](https://github.com/aallan/vera/issues/58) — the single most requested feature for agent interoperability. ### Json ADT ``` data Json { JNull, JBool(Bool), JNumber(Float64), JString(String), JArray(Array<Json>), JObject(Map<String, Json>) } ``` ### 8 built-in operations | Function | Signature | Implementation | |----------|-----------|----------------| | `json_parse` | `String -> Result<Json, String>` | Host import | | `json_stringify` | `Json -> String` | Host import | | `json_get` | `Json, String -> Option<Json>` | Prelude (Vera source) | | `json_array_get` | `Json, Int -> Option<Json>` | Prelude (Vera source) | | `json_array_length` | `Json -> Int` | Prelude (Vera source) | | `json_keys` | `Json -> Array<String>` | Prelude (Vera source) | | `json_has_field` | `Json, String -> Bool` | Prelude (Vera source) | | `json_type` | `Json -> String` | Prelude (Vera source) | ### Architecture - **Normal ADT, not opaque handle** — Json values are constructed directly in Vera code and support full pattern matching, unlike Map/Set/Decimal - **Conditional prelude injection** — Json ADT and utility functions only injected when user code references Json types or constructors - **JObject wraps Map\<String, Json\>** — reuses the existing Map host-import infrastructure - **WASM serialization** — new `vera/wasm/json_serde.py` for bidirectional Python↔WASM marshalling - **Browser runtime** — `writeJson`/`readJson` + host bindings in `runtime.mjs` ### New files - `vera/wasm/json_serde.py` — WASM memory marshalling for Json ADT - `tests/conformance/ch09_json.vera` — 28 test functions - `examples/json.vera` — Weather API scenario example ### Stats - 61 conformance programs (was 60) - 27 examples (was 26) - 2,990 tests (was 2,921) **Full changelog**: https://github.com/aallan/vera/compare/v0.0.97...v0.0.98

Adds the `<Async>` algebraic effect with `Future<T>` type (#59). ### New features - **`async(expr)`** — wraps an expression in `Future<T>` (eager evaluation in reference implementation) - **`await(future)`** — unwraps a `Future<T>` to get the inner value - **`Async` marker effect** — functions using `async`/`await` must declare `effects(<Async>)` - **`Future<T>` ADT** — WASM-transparent (zero runtime overhead) ### Design The reference implementation evaluates `async(expr)` eagerly and `Future<T>` is identity at the WASM level. This is the simplest correct algebraic handler. True concurrent scheduling will be available via `handle[Async]` (#270) and WASI 0.3 native futures (#237). ### Stats - 2 new built-in functions (`async`, `await`) - 50 conformance programs (was 49) - 22 examples (was 21) - 127 Tier-1 verified contracts, 134 total