# 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 `get(())` array element driving a generic instantiation desyncs monomorphization discovery from the effect-op result naming (`pick$Nat` vs `pick$Int`) — a dangling call target, so the function is dropped loudly with E602. Fix direction: derive both from one result-type mirror. | [#1207](https://github.com/aallan/vera/issues/1207) |
| Slot-environment naming keeps type-argument alias spellings opaque where the checker canonicalizes them (`@Option<Cnt>` binder vs `@Option<Int>` ref) — check-green programs dangle loudly (E699) at compile outside handler clauses (PR #1202 aligned the clause bindings). The complete fix canonicalizes `type_expr_slot_name` and `slot_ref_name` together — a global naming-layer change wanting its own PR. | [#1208](https://github.com/aallan/vera/issues/1208) |
| `State<Alias>` of a composite type keys a distinct host cell family from `State<Composite>`, so cross-spelling handlers do not share state — as much a design question (is an alias the same cell?) as a bug; either resolution is mechanical once decided. | [#1209](https://github.com/aallan/vera/issues/1209) |
| State/Exn import registration never walks handler clause bodies, state-init expressions, or i32_pair cells — a family used only there is unregistered while the lowering emits its calls, so check-green programs fail loudly at the whole-module WAT compile (`unknown func $vera.state_push_Nat` / `unknown tag $exn_Int`), and `handle[State<String>]` in a pure fn is check-green invalid WASM. | [#1210](https://github.com/aallan/vera/issues/1210) |
| A bare `get`/`put` inside a NESTED handler's clause body targets different cells in the checker (the outer handler, per clause-check-time scoping) and codegen (the inner handler, per the §7.5.2 lexical rule) — check-green, valid WASM, silent wrong value; the fix is an alignment decision the spec's lexical-scoping language should settle. | [#1211](https://github.com/aallan/vera/issues/1211) |
| A Byte-typed literal inside a value-position join (`if`/`match` branch) lowers as `i64.const` into every i32 Byte boundary — `let @Byte = if ...` and the state-cell init/put/resume twins are check-green invalid WASM (the resume form is verbatim what the E602 skip message recommends); the coherent fix is one branch-descending Byte-literal lowering shared by every #865 arm. | [#1212](https://github.com/aallan/vera/issues/1212) |
| A Unit-literal call argument (`mk(())`) degrades the verifier call summary — the same call spelled `mk(1)` proves a violating refined destructure (E505) while the Unit spelling demotes it to Tier-3; conservative, never unsound, but zero-size arguments carry no information and should not weaken a summary. | [#1214](https://github.com/aallan/vera/issues/1214) |
| Bare effect-op resolution is PYTHONHASHSEED-dependent when a fn's effect row holds two effects declaring the same op name (`lookup_effect_op` iterates the row frozenset) — which signature binds flips across seeds; the op-name sibling of the fixed #1203-era State-type-mapping determinism. | [#1215](https://github.com/aallan/vera/issues/1215) |
| `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 |
|-----------|-------|
| 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 `vera verify`-clean program stores no negative `@Nat` at these sites. **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 three statically-obligated sites stay unguarded and store a negative silently: the effect-operation argument (user-declared effects; the builtin `State` `put`/`resume` boundaries are obligated and codegen-guarded) (codegen's `_effect_ops` carries only the dispatch target), the generic-instantiated constructor field (constructor layouts carry no per-field `@Nat` mono metadata), and the `nat_to_int`/`nat_to_string` conversion builtins (special-cased before the `_fn_nat_params` guard loop) — no runtime guard is emitted at those three 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 tuple/constructor component, which is both statically obligated and runtime-guarded at the function boundary.) #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) |
| 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) |
| `vera/addEffect` propagates the new effect to all transitive callers even when a caller discharges it with `handle[E]`. Handler-aware propagation bounding is roadmap Tier 3. | [#725](https://github.com/aallan/vera/issues/725) |
| 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 expression near the i64 edge can overflow-trap at entry even when its obligation is Tier-1 proved. Keep measures well inside the i64 range; the static tiers are unaffected. | [#1172](https://github.com/aallan/vera/issues/1172) guard (PR #1179 review F3) |

## 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.
