# Known issues

Bugs and limitations tracked against the [issue tracker](https://github.com/aallan/vera/issues). This file is a curated snapshot — the issue tracker is the source of truth, and priority/sequencing live in [ROADMAP.md](ROADMAP.md). Every row follows the same shape: one sentence on what the issue is, one sentence on impact and the path forward.

## Bugs

Defects in shipped compiler, runtime, or tooling behaviour — this table matches the issue tracker's open [`bug`-labelled issues](https://github.com/aallan/vera/issues?q=is%3Aissue%20state%3Aopen%20label%3Abug) one-to-one. Verification-soundness gaps carry the `limitation` label instead and are tracked under [Limitations](#limitations).

| Bug | Issue |
|-----|-------|
| A fact that verification itself has just DISCLOSED as neither proved nor guarded is still assumed at full strength downstream, so a postcondition proves at Tier 1 from a fact the same run admitted it cannot establish, and `vera verify` exits 0 on a program the runtime refutes.  Measured: a `mk` returning `Tuple<PosInt, Int>` whose component comes from `float_to_int` records its `refine_bind` as **`tier3_unguarded`** with an E506 warning — the honest "I could neither prove nor guard this" bucket — while the caller's `ensures(@Int.result > 0)`, which reads that component straight back out, is reported **`verified`**; `vera run --fn f -- -7.0` then fails the postcondition.  Distinct from its two neighbours on the same axis: [#1332](https://github.com/aallan/vera/issues/1332) was a fact asserted circularly at its OWN construction site, and this one crosses a call boundary — the boundary rule that a call-produced value's obligation was *discharged* in the callee's context has a third case it never covered, *disclosed*; [#1362](https://github.com/aallan/vera/issues/1362) is a mis-BUCKETED obligation claiming a guard it does not have, where here the bucketing is honest and the leak is the downstream ASSUMPTION.  A sibling variant reaches the same assumption through the `_translate_if` sort-decline route: the opaque joined value's declared-type fact is asserted at base level, nothing is demoted and nothing warned, and the postcondition check fires at run time instead.  Pre-existing — measured identical at `b4256509` and at every commit of the PR that found it.  Fix direction: a fact whose own obligation resolved to `tier3_unguarded` — or to any not-proved, not-guarded status — must not be asserted at full strength for downstream obligations in the same run: weaken it out of the solver context, or demote every obligation leaning on it out of Tier 1 (the honest transitive reading), or plant the guard that would make the assumption true (the #754 family's work).  The obligation stream already carries the status; the assumption side never consults it. | [#1363](https://github.com/aallan/vera/issues/1363) |
| A handler-clause `@Nat` payload narrowing is classified **`tier3`** — counted in `verify --json`'s `tier3_runtime`, whose meaning is *runtime-guarded* — while no runtime guard exists at the site, and no disclosure fires either: zero warnings, zero `tier3_unguarded`.  `handle[Exn<Int>] { throw(@Nat) -> nat_to_int(@Nat.0) } in { throw(@Int.0) }` verifies clean and `vera run --fn f -- -7` then returns `-7` through the `@Nat` binder with no trap.  The missing GUARD is squarely the [#754](https://github.com/aallan/vera/issues/754) / [#757](https://github.com/aallan/vera/issues/757) / [#765](https://github.com/aallan/vera/issues/765) residual family, but the ACCOUNTING is not: that family's documented contract — the four-site row below — is that an unguarded residual is disclosed statically as an E504 warning / `tier3_unguarded`, the honest "nothing guards this" bucket.  This site takes the other path, so both halves are wrong at once: the summary overcounts guarded obligations, and the disclosure machinery that exists precisely for unguarded residuals never engages.  Corpus-wide there are currently **0 E504 warnings and 0 `tier3_unguarded` obligations**, so that path is entirely unexercised by the suite — which is why a site quietly taking the wrong bucket is invisible to it.  Loud in neither direction: the program is check-green, verify-green, and simply wrong at run time.  The classification is fixable independently of the guard — the binder site should either carry a real guard (#754's work) or be classified `tier3_unguarded` + E504 like its documented siblings, never plain `tier3`.  Fix direction: locate where the clause binder's `nat_bind` is bucketed after an undecided solver result and route it through the same guarded-versus-unguarded classification the other narrowing sites use, keyed on whether codegen actually plants a guard there — the obligation<->guard parity discipline of [#1205](https://github.com/aallan/vera/issues/1205). | [#1362](https://github.com/aallan/vera/issues/1362) |
| A module-declared generic never discovers an instantiation whose type argument is PIPED from an effect-operation result. `get(()) \|> idg()` under `handle[State<Int>]` is `vera check`-green and `vera verify`-green and then compiles to a module missing its caller, dropped through `[E602]`/`[E620]`; the identical pair declared in the entry file runs correctly in both forms, so the module path is necessary rather than incidental. The DIRECT form `idg(get(()))` is [#1310](https://github.com/aallan/vera/issues/1310), whose fix this PR carries — the piped form fails on **both** discovery walks and survives it, and the [#1207](https://github.com/aallan/vera/issues/1207) `BinaryExpr` arm that would appear to cover a pipe does not reach this shape. The two module forms fail with different signatures, which is the tell: the direct one names the mangled clone that was never registered, while the pipe leaves a bare `idg` unresolved — the call-site rewrite never resolved a clone at all. Fix direction: thread the op-result registry through the pipe shape on both walkers, with the cross-component differential this PR adds as the harness that keeps the class closed. | [#1357](https://github.com/aallan/vera/issues/1357) |
| Internal Lark terminal names leak into user-facing `Expected one of:` lists. A parse error whose expected-token set contains an anonymous terminal prints the generated name (`__ANON_0`) instead of the literal it stands for, so the reader is told to supply a token that appears nowhere in the language. `vera/errors.py` already translates one of them — it recognises `__ANON_9` as `::` to detect the old dot-syntax module call — so the repair is to complete that mapping for every anonymous terminal the parser can surface, not to invent a mechanism. | [#1349](https://github.com/aallan/vera/issues/1349) |
| String interpolation refuses a refinement type that resolves to an interpolable primitive. `"n=\(@PosInt.0)"` under `type PosInt = { @Int \| @Int.0 > 0 };` is rejected with `E148`, while the identical interpolation through a plain alias (`type Plain = Int;`) checks clean — so the conversion test consults the written type rather than the resolved one. The resolved-type precedent is SKILL.md's own `vera test` documentation. Workaround: convert explicitly and concatenate — `string_concat("n=", int_to_string(@PosInt.0))` checks clean. | [#1347](https://github.com/aallan/vera/issues/1347) |
| Two of Chapter 6's normative MUSTs are unimplemented, so `vera verify` stays silent about work it did not prove. `spec/06-contracts.md` §6.2.6 requires a warning for every `assume` statement and §6.5 one for each runtime-checked contract; neither is emitted by any phase. `VerifySummary.assumptions` (`vera/verifier.py`) is hardcoded to `0` — its own docstring records it as retained for backward shape compatibility, with no obligation kind mapping to it — and the `verify --json` summary omits the field entirely. `tests/conformance/ch06_assert_assume.vera` measures both halves: one `assume` statement and `tier3_runtime` 3, against zero warnings from `check --json` and `verify --json` alike. The spec's MUSTs stand as written; whether to emit the warnings or soften the normative claim is the open question. | [#1345](https://github.com/aallan/vera/issues/1345) |
| A user `data` declaration taking a built-in container's name compiles at the built-in's width. `_type_expr_to_wasm_type` consults the `Array` / `Map` / `Set` / `Decimal` / `Future` branches **before** `_adt_layouts`, so `data Array { Mk(Int) }` is measured as the built-in's `i32_pair` rather than the ADT pointer `i32`.  The program is check-green; codegen then refuses the function matching on it with a located E602 ("a scrutinee whose representation is a (ptr, len) pair"), drops its callers, and emits a module with **no exports at all** — `vera run` reports `Available exports: (none)` where a fresh-name control prints its value.  Loud, not a wrong answer.  Only `Array` misbehaves: `Map`, `Set` and `Decimal` already answer `i32`, the ADT pointer's own width, so they are inert by width-luck — the same coincidence that kept most of [#1309](https://github.com/aallan/vera/issues/1309)'s alias cases hidden.  Pre-existing: v0.1.11 carries the identical ordering, and #1309 moved only the *alias* branch above these.  The fix needs at least three derivations to agree and two are not enough — `_type_expr_to_wasm_type` (`vera/codegen/core.py`) and `_canonical_wasm_type` (`vera/wasm/inference.py`) were both corrected and the program still lost its exports, so a third site is unlocated.  Note the trap between them: the emitter mixin does not own `_adt_layouts` but `_adt_type_names`, so a `getattr(self, "_adt_layouts", {})` there is a silently disabled shadow rule rather than a failure. | [#1331](https://github.com/aallan/vera/issues/1331) |
| The nightly stress workflow never exercises `TestHostHandleReclamation573` — its 10 stress-marked instances are deselected from the per-PR suite (`-m 'not stress'` addopts) and `.github/workflows/nightly-stress.yml` runs `pytest -v -m stress tests/test_stress.py`, file-scoped, so no automated lane runs the #573/#575/#576/#706 GC-reclamation battery; the class comment's "Run via `pytest -m stress` or nightly CI" states the unmet intent. Run `pytest -m stress` manually until the workflow adds the file or the comment is re-scoped. | [#1328](https://github.com/aallan/vera/issues/1328) |
| Monomorphization's Vera-level type namer has no `IndexExpr` arm, so a generic argument that is an array index drops its caller. `idg(@Array<Int>.0[1])` — a `forall<T>` identity called on an element of a local `Array<Int>` — is `vera check`-green and then dies at `vera run` with `[E602] Function 'main' body contains unsupported FnCall: call target 'idg$Int' not registered in this module`, leaving `Available exports: (none)`: instantiation discovery (`Monomorphizer._infer_vera_type_name`) answers nothing for the index expression and falls to the phantom-var `Bool` default, while the WASM call-rewrite consultor (`InferenceMixin._infer_vera_type`), which DOES have an `IndexExpr` arm, names `idg$Int` at the call — the two consultors disagreeing, which is the clone-name agreement contract's (#772) failure mode. Loud, never a wrong answer. Measured during #1286's review sweep and unchanged by its fix, which closed the same consultor-parallelism gap for `Block`, `MatchExpr`, `IfExpr` and `HandleExpr` — each an exact one-line mirror of its twin — and deliberately left this one: the rewrite's arm delegates to `_infer_index_element_type`, which resolves chained indexing, type aliases and representation-transparent `Future` payloads against codegen tables the monomorphizer does not carry, so a partial mirror would answer differently from the rewrite for those cases, replacing a shape where both consultors say "unknown" with one where they disagree. Fix direction: lift the element-type derivation into one helper both consultors call, rather than a second partial copy that can drift from the first — the shape #1286 argues for throughout. | [#1327](https://github.com/aallan/vera/issues/1327) |
| A match binding's GC shadow-stack push is never popped, so the shadow stack grows with recursion depth until it traps. Both `_translate_match`'s scrutinee rooting and `_setup_match_arm_env`'s binding rooting push onto `$gc_sp` and leave it advanced for the rest of the body; a function restores `$gc_sp` only on the way out, so a recursive function whose body matches pushes once per live frame and eventually crosses `$gc_stack_limit`, whose overflow check is a bare `unreachable`. Bisected on a `decreases`-guarded recursion carrying one match: an ADT (i32) scrutinee survives depth 2046 and traps at **2047**, **identically before and after [#1305](https://github.com/aallan/vera/issues/1305)**, which is what makes this pre-existing rather than new — the i32 rooting has behaved this way since #705/#707. What #1305 changed is reach: a `String` / `Array<T>` scrutinee now takes this path too, and because the pair form roots twice per frame (scrutinee pointer and binder pointer) it survives only 1364 and traps at **1365** — two thirds of the ADT depth, which is what the slot arithmetic predicts: an ADT frame roots the parameter and the binder, a pair frame roots the parameter, the scrutinee pointer and the binder pointer, so three slots per frame against two and 2047 x 2/3 = 1364.7. Loud in every case — `unreachable`, never a wrong value — but the trap names no source construct and the depth at which it arrives is an artefact of how many pushes a body happens to make. Fix direction: pop what a match arm pushes at the arm's end (or scope the rooting to the arm body), so the depth a program can recurse to stops depending on how many matches its body contains. | [#1322](https://github.com/aallan/vera/issues/1322) |
| Codegen's built-in-container branches are tested before `_adt_layouts`, so a user `data` declaration named after a container is classified by the container's representation instead of its own. `_type_expr_to_wasm_type` answers `Array` with `i32_pair` before it ever consults the registered ADT layouts, so `private data Array { MkArr(Int) }` — a perfectly ordinary declaration spec §8.4.1 permits — has its parameter classified as a two-word pair rather than the one-word heap pointer its constructor actually builds. `Map`, `Set`, `Decimal`, `Tuple` and `Future` are inert instances of the same ordering (their branch answers `i32`, which is what the ADT branch would have answered anyway) and compile and run correctly; `Array` is the one name whose two answers differ, and it fails on both sides of [#1309](https://github.com/aallan/vera/issues/1309) — as an unassemblable `i32_pair` local before it, and as an `[E602]` skip after. That E602 currently misattributes the cause, since the message it inherits from the [#1305](https://github.com/aallan/vera/issues/1305) pair guard describes the scrutinee's representation rather than the declaration that produced it; the wording no longer names `String` / `Array<T>` as the source types, but a reader still has to know that a user `data Array` is why a pair representation was claimed at all. Sibling of #1309 (which reordered the alias branch ahead of these same container branches) and of [#1316](https://github.com/aallan/vera/issues/1316) (which is the environment those branches are consulted in) — one function, three orthogonal questions. Fix direction: consult `_adt_layouts` before the built-in container branches, matching `_resolve_named`, where a DECLARED ADT precedes the built-in absorption. | [#1321](https://github.com/aallan/vera/issues/1321) |
| The checker admits literal patterns over scrutinees that can never match them, which is the general disease behind the container-ADT case in [#1315](https://github.com/aallan/vera/issues/1315). `match <String> { true -> 100, _ -> 200 }` and its `1 ->` integer twin are **check-green** — no diagnostic of any kind — although a `String` can equal neither a boolean nor an integer. Nothing downstream is obliged to catch this: codegen refuses the pair-represented spellings since [#1305](https://github.com/aallan/vera/issues/1305) only because a pair has no comparable scalar word, which is an accident of representation rather than a rule about patterns, and the same nonsense over a scrutinee that IS one word has no such backstop. The two holes are one question asked twice — #1315 is "does this constructor belong to this scrutinee's type", this is "does this literal belong to it" — and both fall out of the checker validating a pattern against the arm's own shape rather than against the scrutinee's type. Fix direction: type each pattern against the scrutinee, once, for every pattern kind; the exhaustiveness pass is where the constructor half already half-lives, but the literal half has no home at all today. | [#1320](https://github.com/aallan/vera/issues/1320) |
| `E609` refuses two modules' same-named `data` declarations, and `E610` two modules' same-named **constructors**, by DECLARATION — consulting neither visibility nor the importing namespace's import filter nor local shadowing — the over-breadth [#1281](https://github.com/aallan/vera/issues/1281) removed from the function-side twin `E608`, still in place on the data side. Three remedies were measured against a diamond where `liba` and `libb` both export `public data Shape`, and all three fail identically: **narrowing** the second import so it no longer supplies the type, **declaring** `Shape` in the importing module (which spec §8.5.2 makes shadow both imports), and marking one module's declaration **`private`** (which exports nothing at all) each leave `vera check` and `vera verify` green and then die at `vera compile` with `[E609]` located at line 0 of the entry file, naming modules the entry never imports. `E610` behaves identically on its own axis, and its shape shows the collision is not about the type name at all: `liba` exporting `public data Alpha { Sq(Int), … }` beside `libb` exporting `public data Beta { Sq(Bool), … }` — two DIFFERENT types sharing only the constructor `Sq` — is `[E610]` at compile, and the same three remedies fail it in the same way (narrow the second import, declare a local `data Own { Sq(Int), … }`, or make one supplier `private`: each is check-green and verify-green and each is still `[E610]` at `vera compile`). Renaming in one of the source modules is therefore the only remedy for either code, which is why [#1304](https://github.com/aallan/vera/issues/1304)'s `E156`/`E157` prescribe renaming where their function-side sibling `E155` can offer a selective import or a local declaration — and why spec §8.5.4's "constructor names follow the same shadowing rules as function names" holds of resolution but not of compilation. Sibling of [#1312](https://github.com/aallan/vera/issues/1312): both are the flat namespace's data-collision rails mishandling declarations that occupy distinct identities. Fix direction: give `E609`/`E610` the #1281 treatment — read the same per-owner classification the clone namespace already does, so a declaration no importing namespace can name does not collide with one it can. | [#1317](https://github.com/aallan/vera/issues/1317) |
| A main-file `type` alias named after a prelude ADT leaks into the PRELUDE's own bodies. Codegen's `_type_expr_to_wasm_type` resolves an alias against the flat `self._type_aliases` map (`vera/codegen/core.py`), which holds every namespace's aliases at once, so a prelude combinator emitted into the module renders its own parameters through the main file's shadow: under `type Json = Int;` the prelude's `json_get` takes the alias's i64 where its body wants the ADT's i32 pointer, and the module dies at load (`type mismatch: expected i32, found i64` in `wasm[0]::function[10]::json_get`) on a check-green, verify-green program. `type HtmlNode = Int;` is the same failure in `html_attr`. Spec §8.4.1 makes the alias namespace module-scoped and `vera/naming.py` states the consequence — every consumer must render against the env of the module that DECLARED the enclosing function — but this derivation has no module-scoped env; `_prelude_type_aliases` is already populated in Pass 1.2 and is what a scoped rendering would read. Sibling of [#1309](https://github.com/aallan/vera/issues/1309) but not the same defect: that one was the branch ORDER inside this function (ADT before alias, now corrected to the checker's primitive-alias-ADT spine); this is which alias ENVIRONMENT the function is asked in, and the order fix leaves that mechanism untouched. It does MOVE the failure downstream within prelude scope, though — the reorder flips 17 prelude `json_*` signatures from `(param $p0 i32)` to `(param $p0 i64)`, reverses the loader's complaint from `expected i64, found i32` to `expected i32, found i64`, shifts its offset, and costs `html_attr` one shadow-stack push — so a repro captured before #1309 will not match byte for byte after it. Measured by sweeping `type X = Int;` over all 16 built-in ADT and container names: **15 of 16 broken before #1309, 2 of 16 after** — and both survivors fail in a prelude body rather than the user's, at the branch point and after, which is what separates the two defects. A user ADT that merely SHARES a prelude name is the membership question [#1277](https://github.com/aallan/vera/issues/1277) closed and [#1312](https://github.com/aallan/vera/issues/1312) continues, not this one. Fix direction: give the derivation the declaring module's env, as the checker, verifier and monomorphizer already receive. | [#1316](https://github.com/aallan/vera/issues/1316) |
| The checker accepts a constructor pattern over a container ADT that has no constructors. `match <Array<T>>` and `match <Map<K, V>>` with `Some(...)` / `None` arms check **completely clean** — `ok: true`, zero diagnostics, zero warnings — because the exhaustiveness pass reads `self.env.data_types.get(raw_ty.name)` and returns early on the miss (`vera/checker/control.py`, `return  # unknown ADT, can't check`), and no pattern-type rule objects either. The same nonsense over a primitive scrutinee IS refused: an `@Int` or `@String` scrutinee reaches the infinite-domain branch and reports **E313**, so the hole is exactly the built-in containers, which are `AdtType`s the constructor registry does not know. This is how the ill-typed program in [#1305](https://github.com/aallan/vera/issues/1305) reached codegen at all — its `Some(@Array<String>)` arm over `json_keys`' `Array<String>`, which the issue mistook for an `Option` payload; since that fix, codegen refuses the arm with a located **E602** naming the pair scrutinee's absent tag rather than emitting an unassemblable local, so for a PAIR-represented scrutinee the shape is loud, never a wrong answer, and merely reported against the compiler's back stop instead of against the program. That loudness does not extend to the rest of the hole: a `Map<K, V>` or `Set<T>` scrutinee is an opaque i32 handle, which the pair guard cannot see and codegen happily emits a tag read over — `match map_new() { Some(@Int) -> 1, None -> 2 }` exits 0 printing 2, identically before and after that fix. So the wrong answers this hole admits are live, and only the pair corner of it is currently caught. Fix direction: rule on constructor patterns whose scrutinee names no constructor registry — a checker change, whose new rejections need their own blast-radius pass, and which would both close the handle-scrutinee case and make the E602 back stop unreachable from source. | [#1315](https://github.com/aallan/vera/issues/1315) |
| An entry-file `data` declaration and a module's of the same name silently drop the caller when their shapes differ. `private data Json { JMine(Int) }` in the entry beside `private data Json { JBlob(Int) }` in an imported module is `vera check`-green and then compiles with **exit 0**, `ok: true`, and nothing but `[E602]`/`[E620]` **warnings** — and the entry's `main`, which calls the module's function, is absent from the exports (measured: `exports == ['consume']`, the one function that touches only the entry's own declaration). The artifact loads and simply lacks its entry point. The flat namespace holds one layout per name and the entry's declaration takes it — Pass 1 registers the main file's `data` over the Pass-0.5 module harvest, which only `setdefault`s — so the module's own constructors become `unknown constructor` inside its own bodies. Same one-layout-per-name defect as [#1277](https://github.com/aallan/vera/issues/1277) and **not** closed by its E621 rail, for a structural reason rather than an oversight: that rail compares a PRELUDE declaration against a module's, and an entry-file declaration *suppresses* the prelude's injection outright, so no prelude declaration ever reaches Pass 1.2 and the contending pair here — entry versus module — is one the rail cannot be asked about. Behaviourally identical at `8e08ec90` and after #1277's fix, so pre-existing rather than introduced. Fix direction: put the entry-versus-module pair through the same contention check, reusing the machinery #1277 installed — `vera/prelude.py`'s `data_decl_shape` already decides whether two declarations of one name can share a layout (it is what keeps a module's restatement of a prelude type legal), and the conformance manifest's `expected_error_stage: "compile"` already expresses a check-green/compile-refused negative — leaving the ruling: a new code, or E609 widened from module-versus-module to take the entry file as a namespace, located at both declarations. | [#1312](https://github.com/aallan/vera/issues/1312) |
| The checker resolves a bare call to a SIBLING function's `where` helper. Spec §5 makes a helper local to its parent, and the checker's own `_lookup_function_scoped` implements that — it walks the enclosing frame stack and reads each frame's direct helpers — but it then falls back to `env.lookup_function`, and `vera/registration.py` has recursed every helper into that flat `TypeEnv`. So a top-level `other()` calling `helperx(7)`, where `helperx` is a helper of an unrelated `holder`, is **check-green and verify-green** and then refused by codegen (`Function 'helperx' is not defined in this module and was not found in any imported module`) — the helper is emitted as `holder$where$helperx`, so the bare call has no target. Loud, never a wrong answer. The op-name variant is the one that matters for the #1284 ownership predicate: with the helper named `get` and the sibling reading a `State<Int>` cell by bare `get(())`, the checker binds the HELPER and reports `[E202] Argument 0 of 'get' has type Unit, expected Int` where spec §7.4 resolves the operation — so the checker rejects a program codegen compiles correctly, the two tables disagreeing in the CHECKER's direction for the first time. Codegen's `_scoped_fns` (#1299) implements the spec rule; the fix here is a checker change, whose new rejections need their own blast-radius pass. | [#1307](https://github.com/aallan/vera/issues/1307) |
| `md_parse` diverges between the native and browser runtimes on **211 of 1,471** adversarial inputs (14.3%) and **329 of 4,858** blank-line-separated sections of the project's own documentation (6.8%), measured at [PR #1303](https://github.com/aallan/vera/pull/1303) by comparing the two ADTs directly rather than their renders. The second denominator is the repository's own Markdown, so it moves whenever a document gains or loses a section; 11 of those 4,858 also differ in the rendered output. Nine classes, each with a one-line repro. The largest by a wide margin — 173 of the 211 — is *plain-text run grouping*: the browser emits one `MdText` per scan segment where the reference coalesces adjacent runs, so `**unclosed` is `[MdEmph([]), MdText("unclosed")]` natively and `[MdText("*"), MdText("*unclosed")]` in the browser. That class is invisible to `md_render` (the runs concatenate to the same text) but not to a Vera program that matches on the ADT, which is what makes it a §12.9.3 violation rather than a cosmetic one. The rest are render-visible: emphasis/strong scanning (`***both***` renders `**both****` natively, `***both***` in the browser); list-continuation indent width, where the reference strips exactly two (or three) characters and the browser strips all leading whitespace (`- a\n   b` → `- a  b` vs `- a b`); a `+` bullet, unrecognised in the browser; an `n)` ordered marker, likewise; a loose list, one list natively and two in the browser (`- a\n\n- b`); nesting past two levels, flattened in the browser (`- a\n  - b\n    - c`); a thematic break with internal spaces (`*   *   *`); and a table without a separator row (`\| a \| b \|\n- li`). Neither implementation is the specification — §9.7.3 pins the ADT, not the grammar that produces it — so closing this means choosing a parse for each class and stating it, then mirroring. Successor to [#1294](https://github.com/aallan/vera/issues/1294), which closed the `md_render` half; the parity suite pins the shapes they do agree on, so a regression on one of those goes red. | [#1301](https://github.com/aallan/vera/issues/1301) |
| A postcondition may name a `State<T>` the function's effect row never declares, and `vera check` accepts it: `ensures(new(State<Bool>) == false)` under `effects(<State<Int>>)` reports OK, then `vera compile` fails with **E699** — the internal-compiler-error diagnostic whose own text says the type checker should have rejected the input, which is exactly the situation. Both forms land there for the same reason (no cell of that family exists, so `old()` finds no snapshot local and, since [#1285](https://github.com/aallan/vera/issues/1285), `new()` finds no getter). Loud and never a wrong answer, so this is diagnostic quality rather than soundness — but it is a check-green program that cannot compile, reported against the compiler instead of against the program, with a bug-report request the user should not act on. Before #1285 the `new()` side was worse than loud: the name-keyed lookup found the row's other getter and silently read the wrong cell. Fix direction: validate an `OldExpr`/`NewExpr`'s effect reference against the declared row where the checker already validates the rest of the clause, one rule for both forms; `test_a_family_the_row_does_not_declare_is_loud_on_both_sides` pins today's E699 and is the test to flip. | [#1298](https://github.com/aallan/vera/issues/1298) |
| `ch05_closure_nat_return` (a run-level conformance program in the pre-commit + CI gate) trapped **once** in a full `check_conformance.py` run (`unreachable` in `main` — the sentinel `assert` or a GC shadow-stack guard) and has not reproduced in ~960 attempts across isolated, parallel, eager-GC, and hash-seed-swept executions; the emitted WAT is deterministic and correct. Suspected rare runtime/GC/wasmtime interaction, tracked so a future intermittent CI red resolves here instead of starting fresh. | [#996](https://github.com/aallan/vera/issues/996) |

## Limitations

Things Vera cannot do yet, as distinct from defects in what it claims to do.

| Limitation | Issue |
|-----------|-------|
| Nested handlers over the SAME `State<T>` cannot honour spec §7.5.2's enclosing-context rule for a clause-body bare `get`/`put`. The clause TRANSFORM half routes outward correctly, but the host cell intrinsics (`state_get_T` / `state_put_T`) address only the innermost pushed cell of a family, so the operation would read or write the INNER cell where the rule names an outer one — including at a distance, as in an `Int`/`Nat`/`Int`/`Nat` nest whose third level routes to the second. The shape is a loud `E602` codegen skip rather than hybrid semantics; the fix is depth-indexed host access (`state_get_at`/`state_put_at` or push-time cell handles) across the native, browser and WASI hosts, plus the verifier's obligation keying for depth-addressed cells. Different-family nesting is unaffected. Outward clause re-entry is separately capped at 8 levels (`STATE_CLAUSE_INLINE_DEPTH_CAP`), because each re-entry re-expands another clause body and the emitted code is exponential in the nesting depth. | [#1233](https://github.com/aallan/vera/issues/1233) |
| An ADT `decreases` measure is runtime-ranked only when its type's reachable field structure is fully concrete: a parameterized measure (`List<Int>`), or a concrete type whose recursion rides through a parameterized field, gets no runtime guard (never a wrong one — the registered generic layout does not describe concrete construction), staying statically checked and Tier-3-disclosed. Per-instantiation `$dec_size_<T>` helpers (the `$eq_<type>` pattern) close it. | [#1177](https://github.com/aallan/vera/issues/1177) |
| Tier 2 verification (Z3 guided by `assert`/lemma hints) is specified in §6.3.2 but not implemented, so contracts that need hints fall to Tier 3 runtime checks. Per-monomorphization verification (#732) has since landed; full Tier 2 (hint-guided) stays on the Milestone 4 horizon. | [#427](https://github.com/aallan/vera/issues/427) |
| `data invariant(...)` clauses (spec §2.6, §6.2.3) are not implemented — every documented form fails with E130 because the slot environment for the invariant predicate isn't wired up. Refinement types (`{ @T \| predicate }`, §2.6) are the working alternative until this lands. | [#686](https://github.com/aallan/vera/issues/686) |
| **Statically**, every narrowing *binding site* is obligated: a provably-negative value is an E503 error, and an untranslatable narrowing at an unguarded site is an E504 warning — so a program whose narrowings are all statically PROVEN stores no negative `@Nat` at these sites. `vera verify` exits 0 on the E504 warnings too, so verify-clean is the weaker property: a disclosed narrowing is one the static proof did not reach, and at an unguarded site nothing else does either. **At runtime** (an unverified `vera compile`/`run`), the guard covers every concrete *direct* binding site (a nested constructor sub-pattern is the exception, #765 below), generic function-formal calls, and the string/markup builtin `@Nat` parameters (`string_repeat`, `string_pad_start`/`_end`, `string_from_char_code`, `md_has_heading`), but four statically-obligated sites stay unguarded and store a negative silently: the effect-operation argument of a USER-declared effect — the built-in `State` `put`/`resume` boundaries and the built-in `Exn` `throw` payload are obligated and codegen-guarded, the latter with the #1203 sign/widening pair on unrefined payloads and, on a refined payload, the §2.6.5 predicate guard (its lowered check includes the base's range) plus the independent `@Nat`-to-`@Int` widening guard ([#1268](https://github.com/aallan/vera/issues/1268)) — (codegen's `_effect_ops` carries only the dispatch target for the rest), the generic-instantiated constructor field (constructor layouts carry no per-field `@Nat` mono metadata), the `nat_to_int`/`nat_to_string` conversion builtins (special-cased before the `_fn_nat_params` guard loop), and a **tuple component at construction** (the built-in variadic `Tuple` carrier has no per-field metadata either) — no runtime guard is emitted at those four sites; the unguarded residual is disclosed statically as an E504 warning instead. (The static obligation now also covers the function **return** position — an `@Int` value narrowing into a `@Nat` return is an E503 obligation backed by a codegen return guard, #758 — and the value-position constructor component, which is both statically obligated and runtime-guarded where the field is CONCRETE. The value-position *tuple* component is the fourth unguarded site above: measured `tier3_unguarded`/E504 with no guard emitted where the narrowing is untranslatable, at construction and at the function boundary alike — a tuple that is destructured is checked at the destructure, while one that is only returned or passed on gets no RUNTIME check; statically the positions still obligate, which is why a provably-negative return control reports E503.) #820 threaded the per-component target-type table into codegen (the metadata these narrowing guards need); the generic-field and effect-op sites are now unblocked for wiring, though the narrowing direction is not yet guarded here. | [#754](https://github.com/aallan/vera/issues/754), [#757](https://github.com/aallan/vera/issues/757) |
| A refinement / `@Nat` narrowing bound in a **nested** constructor sub-pattern (`Some(Some(@PosInt))` on `Option<Option<Int>>`) is statically obligated — a `vera verify`-clean program is sound; a bad nested refined narrowing is `E505`, a bad nested `@Nat` narrowing is `E503` (#763) — but the runtime guard covers only the `@Nat` nested bind (verified by run probes: a negative payload traps in both direct and closure positions) — the *refined* nested bind is not guarded, so an unverified compile doesn't trap on a violating nested refined payload; the verifier discloses that residual as `tier3_unguarded`/E506 | [#765](https://github.com/aallan/vera/issues/765) |
| A refinement whose base carries a **non-plain type argument** (`{ @Array<{ @Int \| ... }> \| array_length(...) > 0 }`, an `Array<fn(...)>` base) gets **no runtime guard at any boundary** — `_refinement_guard_parts` cannot spell the binder slot for such a base, so named-function and closure parameters and returns alike leave the predicate unchecked at run time. The verifier discloses this honestly (`tier3_unguarded`, E506, excluded from runtime-checked totals — `_refined_boundary_codegen_guardable` mirrors the codegen bail, KEEP IN SYNC); the guard itself is the open work. Same disclosure family as #754 / #757 / #765. | [#1036](https://github.com/aallan/vera/issues/1036) |
| Contracts that depend on a `handle[...]` expression's value fall to Tier 3 — the verifier does not model the `handle[...]` expression's value or handler-clause state, so an `ensures` over a handle result is runtime-checked rather than statically proved. (Primitive-op and binding obligations *inside* the handle body walk at enclosing-scope precision and can prove Tier-1; a clause body's slot-dependent obligations are fresh-scope Tier-3, while a manifest violation there — `5 / 0` — stays a loud compile error.) | [#439](https://github.com/aallan/vera/issues/439) |
| `IO.read_line` / `IO.read_char` block indefinitely — there is no non-blocking or timed stdin read, so a program cannot wait on a key press and a clock at once (input concurrency). | [#770](https://github.com/aallan/vera/issues/770) |
| A value's postcondition / refinement is not propagated **through an ADT field**: storing a provably-constrained value (e.g. a `mag(@Int -> @Int) ensures(@Int.result >= 0)` result) into a `data` constructor field and recovering it with `match` forgets the constraint, so a postcondition whose truth depends on it cannot be discharged at Tier 1 — it degrades to a Tier-3 runtime check (or, on some shapes, is reported as an unprovable obligation). Conservative incompleteness, not unsoundness: the false variant is still correctly rejected and the contract is enforced at runtime; identical for same-file and cross-module callees. Same reporting/completeness family as the (since-closed) #764 and #779. | [#909](https://github.com/aallan/vera/issues/909) |
| `vera test` cannot generate inputs for functions with ADT parameters, so those functions are skipped with a warning. Constructor synthesis with recursive field generation is the planned fix (Milestone 1). | [#440](https://github.com/aallan/vera/issues/440) |
| `vera test`'s input generator builds its `SmtContext` without the function lookup, ADT registry, or recorded-type hook the verifier has, so a `requires` that calls a user function — or any built-in without an explicit translation branch — is untranslatable there and the target is skipped, though the verifier translates the same contract fine. Every such skip is disclosed by name; threading the function lookup and callee-scope machinery through recovers the coverage. | [#1249](https://github.com/aallan/vera/issues/1249) |
| Effect row variables cannot be unified, so higher-order functions polymorphic over their effect rows are not expressible. Full effect polymorphism is Milestone 4 work. | [#294](https://github.com/aallan/vera/issues/294) |
| Every `vera` invocation re-parses and re-checks the whole module graph from scratch. Incremental compilation is Milestone 4 work; the LSP server's warm `VerificationSession` already covers the editor loop. | [#56](https://github.com/aallan/vera/issues/56) |
| A module cannot re-export an imported symbol, so deep module trees force consumers to import from the defining file. Sequenced behind module-qualified call disambiguation (#187) in Milestone 4. | [#127](https://github.com/aallan/vera/issues/127) |
| There is no package system or registry — all code shares one module tree resolved from the filesystem. Milestone 4 work; the issue carries the design discussion. | [#130](https://github.com/aallan/vera/issues/130) |
| There is no interactive read-eval-print loop; the shortest feedback path is `vera run` on a file. Milestone 3 developer-experience work. | [#224](https://github.com/aallan/vera/issues/224) |
| The language server resolves module imports from disk rather than open editor buffers, so unsaved changes in imported files aren't seen. Buffer-aware resolution is roadmap Tier 3. | [#724](https://github.com/aallan/vera/issues/724) |
| `vera lsp` will not run on Python 3.16+: its `pygls` dependency calls `asyncio.iscoroutinefunction`, removed in 3.16. Out of Vera's hands until pygls migrates to `inspect.iscoroutinefunction`; tracked so the `[lsp]` extra's support window is explicit (the rest of the toolchain is unaffected). | [#753](https://github.com/aallan/vera/issues/753) |
| LSP slot go-to-definition covers parameters only — `let` and `match` bindings aren't navigable, and there is no mechanical slot-index rewriting on signature change. Roadmap Tier 3. | [#181](https://github.com/aallan/vera/issues/181) |
| There is no date or time handling beyond `IO.time` — no ISO 8601 parsing, formatting, or arithmetic. Milestone 2 server-adjacent work. | [#233](https://github.com/aallan/vera/issues/233) |
| There are no cryptographic primitives — no hashing, no HMAC. Milestone 2 work, needed for API-authentication patterns like webhook signatures. | [#235](https://github.com/aallan/vera/issues/235) |
| There is no CSV parsing or generation. Milestone 2 server-adjacent work; JSON is the workaround interchange format today. | [#236](https://github.com/aallan/vera/issues/236) |
| The experimental `--target wasi-p2` (v0.0.194) routes IO, clocks, and random through standard component interfaces and `--world server` (v0.0.195) serves `wasi:http`, but the surface is IO + Random only — Http and every other host family are rejected under wasi-p2 with a diagnostic, and the default `wasm` target still uses ad-hoc `vera.*` host imports. Extending the wasi-p2 target to `wasi:http` outbound, streaming filesystem, and sockets is Milestone 2 server-effect work. | [#853](https://github.com/aallan/vera/issues/853) |
| WASM execution has no configurable fuel, memory, or timeout limits, so pathological computation runs unbounded. Milestone 2 work, essential for server workloads on untrusted input. | [#239](https://github.com/aallan/vera/issues/239) |
| `Http.get`/`Http.post` send fixed headers — callers cannot add custom ones such as `Authorization`. Milestone 2 Http-hardening work. | [#351](https://github.com/aallan/vera/issues/351) |
| Http responses surface only the body — status codes are not accessible, so callers cannot distinguish a 404 from a 500. Milestone 2 Http-hardening work. | [#352](https://github.com/aallan/vera/issues/352) |
| Http requests have no per-request timeout control. Milestone 2 Http-hardening work; today a hung server hangs the program. | [#353](https://github.com/aallan/vera/issues/353) |
| The browser runtime implements Http via deprecated synchronous XMLHttpRequest, which browsers throttle. Milestone 2 Http-hardening work, currently blocked (see the issue's relationships). | [#355](https://github.com/aallan/vera/issues/355) |
| Http supports GET and POST only — no PUT, PATCH, or DELETE. Milestone 2 Http-hardening work. | [#356](https://github.com/aallan/vera/issues/356) |
| `Inference.complete` hardcodes `max_tokens` and `temperature`. Configurability is Milestone 2's first Inference-hardening item — agent workloads need both for cost gates and deterministic replays. | [#370](https://github.com/aallan/vera/issues/370) |
| `Inference.embed` (vector embeddings) is not implemented. Blocked on the float-array host-alloc infrastructure (#373). | [#371](https://github.com/aallan/vera/issues/371) |
| The Inference effect cannot be handled in user code — `handle[Inference]` is rejected. Full handler support enables mocking, caching, and routing strategies (Milestone 2). | [#372](https://github.com/aallan/vera/issues/372) |
| Host imports cannot return `Array<Float64>` — the `alloc_result_ok_float_array` infrastructure doesn't exist. Required by `Inference.embed` (#371). | [#373](https://github.com/aallan/vera/issues/373) |
| The `<DB>` effect is Phase 1: SQLite-only, a single connection per run, and positional stringly-typed rows (`Array<Array<Option<String>>>`). Named columns, typed cells, additional backends, and transactions are later phases. (`handle[DB]` is separately blocked on host-effect handlers, #372.) | [#1143](https://github.com/aallan/vera/issues/1143) |
| `runtime.mjs` doesn't export its string-marshalling helpers, so JavaScript cannot pass `String` arguments into Vera functions in the browser. This forces browser programs into the compute-upfront/drain-stdout pattern; exporting the helpers is roadmap Tier 3. | [#603](https://github.com/aallan/vera/issues/603) |
| `IO.sleep` busy-waits the browser's main thread, freezing the tab for the sleep duration — animations and paced simulations don't run meaningfully under `--target browser`. The JSPI-based suspend/resume fix is roadmap Tier 3, demoted below correctness work. | [#609](https://github.com/aallan/vera/issues/609) |
| ANSI escape sequences render as literal control characters in the browser DOM, so terminal-style programs display garbage under `--target browser`. A minimal ANSI-subset interpreter in `runtime.mjs` is roadmap Tier 3. | [#610](https://github.com/aallan/vera/issues/610) |
| The runtime `decreases` guard evaluates the measure with machine i64 arithmetic where the prover reasons over unbounded integers, so a measure whose arithmetic reaches the i64 edge disagrees with its proof: it overflow-TRAPS at entry even though the obligation is Tier-1 proved, because the #798 guards on `@Int`/`@Nat` `+`/`-`/`*` (`vera/wasm/operators.py`) cover a measure expression like any other arithmetic. Silent WRAPPING is the narrow residual rather than the common case — it needs a site where `_overflow_arith_codegen_type` returns `None`, i.e. the checker's resolved-type table does not classify BOTH operands as `Int`/`Nat`, so no guard is emitted at all. Keep measures well inside the i64 range; the static tiers are unaffected. | [#1222](https://github.com/aallan/vera/issues/1222) |

## Refactoring needed

No files currently need decomposition.

## Test coverage gaps

Internal test-quality items that don't affect correctness today but would make the suite more durable to refactoring.

No known test coverage gaps.

## CI workarounds

Defensive measures currently applied in CI (CVE ignores, forced upgrades, etc.) with explicit removal triggers — bridges, not permanent exceptions.

| Workaround | Where | Rationale | Remove when | Issue |
|------------|-------|-----------|-------------|-------|
| `codecov/codecov-action` SHA-pinned to a commit (`e79a696` = v6.0.1) instead of the floating `@v6` tag | Both Codecov upload steps in `.github/workflows/ci.yml` | Codecov was acquired by Harness (June 2026), elevating the risk that the floating tag is repointed and silently flows into CI; pinning to a reviewed commit closes that. Coverage enforcement is unaffected — the 80% gate is the on-runner `--cov-fail-under`, and uploads are `fail_ci_if_error: false`. | The Codecov → Harness migration stabilises — then re-evaluate, including whether to adopt a repo-wide SHA-pin policy. | [#712](https://github.com/aallan/vera/issues/712) |

## Runtime workarounds

Defensive measures applied in compiler / runtime code that exist to bridge an upstream-fixed-but-unreleased bug — same shape as the CI workarounds table, but the workaround sits in shipped code rather than CI config.

No runtime workarounds currently in place.