aallan · aallan · Aug 4, 2026 · Aug 3, 2026
@@ -8,7 +8,7 @@ Read `SKILL.md` for the full language reference. It covers syntax, slot referenc
 
 ### Conformance programs as reference
 
-The conformance suite in `tests/conformance/` contains 175 small, self-contained programs — often one per language feature — that serve as minimal working examples (most are fully self-contained; the cross-module programs of Chapters 7–9 import companion `_lib`/module fixtures). Each positive program must pass its declared verification level (see `manifest.json` for mappings: `parse`, `check`, `verify`, or `run`); the twenty-two negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) instead must *fail* `check` with the E-code in their `expected_error` field. When you need to see how a specific construct works (e.g. effect handlers, match expressions, closures), check the corresponding conformance program before reading the spec.
+The conformance suite in `tests/conformance/` contains 176 small, self-contained programs — often one per language feature — that serve as minimal working examples (most are fully self-contained; the cross-module programs of Chapters 7–9 import companion `_lib`/module fixtures). Each positive program must pass its declared verification level (see `manifest.json` for mappings: `parse`, `check`, `verify`, or `run`); the twenty-three negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) instead must *fail* `check` with the E-code in their `expected_error` field. When you need to see how a specific construct works (e.g. effect handlers, match expressions, closures), check the corresponding conformance program before reading the spec.
 
 ### Workflow
 
@@ -185,7 +185,7 @@ Each stage is a module with a single public API function (`parse_file`, `transfo
 pytest tests/ -v                       # Run all tests (see TESTING.md)
 pytest tests/test_conformance.py -v    # Conformance suite only
 mypy vera/                             # Type-check the compiler
-python scripts/check_conformance.py    # All 175 conformance programs hold (positives pass; negatives fail with their E-code)
+python scripts/check_conformance.py    # All 176 conformance programs hold (positives pass; negatives fail with their E-code)
 python scripts/check_examples.py       # All 42 examples must pass
 python scripts/check_corpus_canonical.py # All 217 corpus programs in canonical form
 ```
@@ -196,7 +196,7 @@ When implementing a new language feature, write the conformance program *first*
 
 ### Invariants
 
-- All 175 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) must *fail* `check` with their `expected_error` E-code
+- All 176 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) must *fail* `check` with their `expected_error` E-code
 - All 42 examples in `examples/` must pass `vera check` and `vera verify`
 - `mypy vera/` must be clean
 - `pytest tests/ -v` must pass

@@ -31,7 +31,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 - **`fn old` / `fn new` declarations are rejected at the declaration site, `E153`** ([#1181](https://github.com/aallan/vera/issues/1181)). The grammar reserves `old(` and `new(` in expression position for the contract state forms — `old_expr` / `new_expr` in `vera/grammar.lark`, each of which demands an effect reference — so a bare call `old(5)` is always read as a malformed state reference (`[E030]`/`[E031]`, [#1173](https://github.com/aallan/vera/issues/1173)) and never resolves to a function — not in the declaring file, and not inside the declaring module either. One route did reach such a function: a module-qualified `mod::old(...)` parses through the module-call rule, so a module export named `old` was callable cross-module (and only cross-module) — adversarial review of the fix confirmed the shape checked and ran. The declaration is now refused outright, reserving the whole identifier rather than leaving it a trap in every unqualified position, the sibling of `E151` (built-in functions) and `E152` (built-in effects) under the same one-canonical-form rule. **Breaking**: a module export named `old` or `new` that was called via the qualified route must be renamed. The gate covers top-level and `private` functions, generic `forall<T>` functions, `where`-helpers (called in expression position exactly like top-level functions), and modules — a module declaring `fn old` surfaces `E153` into its importer, as `E151` and `E152` already do. The reservation is on the whole identifier, so `older` / `renew` / `news` stay legal.
 
-  The reserved set is exactly `{old, new}`, not every keyword the contextual lexer admits as a function name. `assert`, `assume`, `forall`, `exists`, `handle`, `match`, `if`, `let`, `fn`, `true` and `false` were all probed and share the "declares fine, cannot be called from expression position" property, but that property alone is not grounds for rejection: `public fn handle(@Request -> @Response)` is the `vera serve` entry point (spec §9.5.6), invoked by the host rather than from Vera source. The probe record lives in the test docstrings. Spec §5.2 states the rule; new conformance program `ch05_reserved_fn_name_rejected` (172, was 171) pins it as an `E153` negative. Mutation-validated: emptying the reserved set, dropping the `where`-helper recursion, dropping the module surfacing, and matching on prefix rather than whole identifier each flip their targeted tests RED.
+  This half of the gate covers the two contract state forms; the keyword class the contextual lexer also admits as a function name is reserved separately, by [#1187](https://github.com/aallan/vera/issues/1187) below. The probe record lives in the test docstrings. Spec §5.2 states the rule; new conformance program `ch05_reserved_fn_name_rejected` (172, was 171) pins it as an `E153` negative. Mutation-validated: emptying the reserved set, dropping the `where`-helper recursion, dropping the module surfacing, and matching on prefix rather than whole identifier each flip their targeted tests RED.
+
+- **A function named after a grammar keyword is rejected at the declaration site, `E153`** ([#1187](https://github.com/aallan/vera/issues/1187)). Lark's contextual lexer re-lexes `assert`, `assume`, `forall`, `exists`, `match`, `if`, `let`, `fn`, `true` and `false` as ordinary identifiers after `fn`, so each declares cleanly — and none can be written in expression position, where the spelling is always the keyword: a bare `match(3)` does not parse at all (`[E005]`), and `assert(3)` / `assume(3)` are read as the statement forms and collide (`[E121]` plus `[E172]`/`[E173]`). Every one is a declarable trap, so the reservation refuses the mistake at its source rather than letting it surface as whichever call-site error the spelling happens to produce — the same one-canonical-form rule that already covers the contract state forms ([#1181](https://github.com/aallan/vera/issues/1181)), built-in functions (`E151`) and built-in effects (`E152`). **Breaking**: a module-qualified `mod::match(...)` parses through the module-call rule rather than any keyword rule, so a module export under one of these names was callable cross-module (and only cross-module) — probed on the pre-fix tree, the shape checked and ran. Such an export must be renamed; the breakage is loud and located at the module's declaration.
+
+  `handle` is carved out and stays legal: `public fn handle(@Request -> @Response)` is the entry point the host invokes under `vera serve` and `wasi:http` (spec §9.5.6, `examples/http_server.vera`), so being uncallable from Vera source does not make it dead code. It lives in a named `_HOST_INVOKED_FN_NAMES` set subtracted from the reservation, so a future host-invoked entry point joins it deliberately rather than by editing a flat list. The `E153` rationale branches with the reason — a keyword is not described as a contract state form — while the fix stays "rename" on both. The gate inherits the #1181 shape: top-level, `private` and generic `forall<T>` functions, `where`-helpers, and modules (a module declaring `fn match` surfaces `E153` into its importer, carrying the module's own file path). Matching is on the whole identifier, so `matched` / `letter` / `iffy` stay legal, and `op <keyword>(...)` inside an `effect` block never reaches the gate — the lexer refuses that spelling at parse (`[E005]`), pinned so a grammar change that admits it shows up as a failure to widen. Spec §5.2 states both halves of the rule; new conformance program `ch05_reserved_keyword_fn_rejected` (175, was 174) pins it as an `E153` negative. Mutation-validated: emptying the keyword set flips the ten keyword tests RED with the `old`/`new` tests still green, and emptying the carve-out flips the `handle` control RED (and breaks `examples/http_server.vera` and `ch09_http_server`).
 
 - **`Vera`-prefixed type names are reserved for the prelude, `E154`** ([#1184](https://github.com/aallan/vera/issues/1184) review). The prelude's combinators resolve their parameter types through generated declarations in that namespace (`VeraOptionMapFn`; type parameters `VeraA`/`VeraB`, #869), and `inject_prelude` skips any of its declarations whose name a user program already spells — so `type VeraOptionMapFn = Int;` silently re-typed the prelude's own signatures: check-green, then a WebAssembly validation failure at run. Declaring a type or alias whose name begins with `Vera` plus an uppercase letter or digit is now refused at the declaration, with module declarations surfacing the error into their importer as the E151/E152/E153 family does. Ordinary names merely containing the letters (`Veranda`, `MyVeraThing`) are unaffected, and shadowing the *unprefixed* prelude aliases (`OptionMapFn`) remains legal. New conformance program `ch08_reserved_vera_prefix_rejected` (175, was 174) pins the rule.
 

@@ -58,7 +58,7 @@ VERA_JS_COVERAGE=1 pytest tests/test_browser.py -v  # Browser tests with JS cove
 VERA_EAGER_GC=1 vera run file.vera  # Force GC on every alloc (see ENVIRONMENT.md, debug knob for #593-class GC-rooting bugs)
 mypy vera/                        # Type-check the compiler itself
 
-python scripts/check_conformance.py    # Verify all 175 conformance programs (positives pass their level; negatives fail with their expected_error E-code)
+python scripts/check_conformance.py    # Verify all 176 conformance programs (positives pass their level; negatives fail with their expected_error E-code)
 python scripts/check_examples.py      # Verify all 42 examples parse + check + verify
 python scripts/check_corpus_canonical.py # Verify all 217 corpus programs are in canonical form (vera fmt)
 python scripts/check_examples_readme.py # Verify vera run commands in examples/README.md
@@ -90,7 +90,7 @@ See [`TOOLCHAIN.md`](TOOLCHAIN.md) for the CLI cookbook — driving the toolchai
 - `vera/` — Reference compiler: grammar, parser, AST, transformer, type checker, verifier, codegen, CLI
 - `examples/` — 42 example Vera programs (all must pass `vera check` and `vera verify`)
 - `tests/` — Test suite (unit tests + conformance suite)
-- `tests/conformance/` — 175 conformance programs validating every language feature against the spec
+- `tests/conformance/` — 176 conformance programs validating every language feature against the spec
 - `scripts/` — CI and validation scripts
 
 ## Writing Vera code
@@ -127,7 +127,7 @@ Before changing code — **adding or removing** — write the test that proves y
 ## What not to break
 
 - Pre-commit hooks run mypy + pytest + conformance suite + example validation on every commit
-- All 175 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) must *fail* `check` with their `expected_error` E-code
+- All 176 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) must *fail* `check` with their `expected_error` E-code
 - All 42 examples in `examples/` must pass `vera check` and `vera verify`
 - Version must stay in sync across `pyproject.toml`, `vera/__init__.py`, `docs/index.html`, `README.md`, and `uv.lock` (gated by `scripts/check_version_sync.py`); CHANGELOG.md must also carry a matching `## [X.Y.Z]` section
 - All tests must pass: `pytest tests/ -v`

@@ -206,7 +206,7 @@ None of this is Vera-specific, but it validates the design choices. The thesis i
 
 This is a real concern. LLMs are trained on trillions of tokens of Python, TypeScript, and JavaScript. A MojoBench study (NAACL 2025) found that even fine-tuned models achieved only 30–35% improvement over base models on Mojo code generation, illustrating the cold-start problem for new languages.
 
-Vera's approach has three parts. First, the agent-facing documentation (SKILL.md) is designed to be dropped into a model's context window, so the model works from the language specification rather than training data recall. Second, Vera's syntax is deliberately simple and regular — fewer constructs, each with exactly one canonical form — which reduces the surface area a model needs to learn. Third, the conformance test suite (175 programs covering every language feature) gives models concrete examples to learn from and conform to. Simon Willison's December 2025 JustHTML write-up illustrates the same point in practice: an LLM-assisted implementation, guided by the html5lib conformance suite, conformed to the HTML parsing spec by running against its tests — a comprehensive test suite is a strong scaffold for a model implementing to a specification.
+Vera's approach has three parts. First, the agent-facing documentation (SKILL.md) is designed to be dropped into a model's context window, so the model works from the language specification rather than training data recall. Second, Vera's syntax is deliberately simple and regular — fewer constructs, each with exactly one canonical form — which reduces the surface area a model needs to learn. Third, the conformance test suite (176 programs covering every language feature) gives models concrete examples to learn from and conform to. Simon Willison's December 2025 JustHTML write-up illustrates the same point in practice: an LLM-assisted implementation, guided by the html5lib conformance suite, conformed to the HTML parsing spec by running against its tests — a comprehensive test suite is a strong scaffold for a model implementing to a specification.
 
 
 ## How does Vera compare to Dafny / Lean / Koka / F*?
@@ -249,7 +249,7 @@ The reference compiler is under active development. The current release includes
 
 - A seven-stage pipeline: parse, transform, resolve, typecheck, verify, compile, execute
 - A 14-chapter formal specification
-- 8,796 tests, including a 175-program conformance suite
+- 8,840 tests, including a 176-program conformance suite
 - 42 working example programs
 - 164 built-in functions covering strings, arrays, math, parsing, and data types
 - Four built-in abilities (Eq, Ord, Hash, Show) with constrained generics and ADT auto-derivation