Testing

This is the single source of truth for Vera's testing infrastructure, coverage data, and test conventions.

Overview

Metric	Value
Tests	12,290 across 181 files (~157,000 lines of test code; 12,091 passed + 26 stress-deselected, 173 skipped)
Compiler code coverage	95% Python, 87% JavaScript (CI minimum: 80%)
Conformance programs	244 programs across 9 spec chapters, validating every language feature
Example programs	43, all validated through vera check + vera verify
Spec code blocks	189 parseable blocks from 14 spec chapters: 92 parse, 86 type-check, 85 verify (the rest carry inline vera:skip annotations, #538)
README code blocks	4 Vera blocks (4 validated, 0 annotated)
FAQ code blocks	3 Vera blocks in FAQ.md (2 validated, 1 annotated snippet)
HTML code blocks	5 Vera blocks in docs/index.html (5 validated: parse + check + verify)
Contract verification	411 of 533 obligations (77.1%) across the 43 examples verified statically (Tier 1) — the denominator grew with the auto-synthesised primitive-op obligations of the soundness campaign
CI matrix	13 combinations (Python 3.11/3.12/3.13 × ubuntu-latest/macos-15/macos-26/windows-latest, plus an advisory ubuntu-24.04-arm × 3.12 cell) + browser parity (Node.js 22) + wheel-availability preflight

Running Tests

All commands assume the virtual environment is active (source .venv/bin/activate).

# Test suite
pytest tests/ -v                                     # full suite, verbose
pytest tests/test_codegen_expressions.py             # single file
pytest tests/test_codegen_expressions.py::TestArithmetic  # single class
pytest tests/test_conformance.py -v                  # conformance suite only
pytest tests/ --cov=vera --cov-report=term-missing   # with coverage

# JavaScript coverage (browser runtime)
VERA_JS_COVERAGE=1 pytest tests/test_browser.py -v  # V8 coverage via c8

# GC-rooting diagnostic (forces $gc_collect on every alloc, see ENVIRONMENT.md)
VERA_EAGER_GC=1 pytest tests/test_codegen_closures.py::TestClosureReturnShadowPushBalance -v

# Host-binding diagnostic (re-raises a host callback's own exception, see ENVIRONMENT.md).
# The suite sets and unsets VERA_DEBUG_HOST_ERRORS itself, so run it without a prefix:
pytest tests/test_runtime_traps.py::TestHostErrorDebugKnob1302 -v

# Type checking
mypy vera/                                           # strict mode

# Validation scripts
python scripts/check_conformance.py                  # conformance suite (244 programs, see manifest.json)
python scripts/check_examples.py                     # 43 example programs
python scripts/check_spec_examples.py                # spec code blocks
python scripts/check_readme_examples.py              # README code blocks
python scripts/check_skill_examples.py               # SKILL.md code blocks
python scripts/check_faq_examples.py                 # FAQ.md code blocks
python scripts/check_pypi_readme_examples.py         # PYPI_README.md code blocks (parse + check + verify)
python scripts/check_html_examples.py               # docs/index.html code blocks
python scripts/check_version_sync.py                 # version consistency
python scripts/check_wheel_availability.py           # pre-flight: every runtime dep has wheels for all supported platforms (#691 backstop)

Test Files

File	Tests	Lines	What it covers
test_parser.py	171	1370	Grammar rules, operator precedence, parse errors
test_ast.py	138	1,145	AST transformation, node structure, serialisation, string escape sequences, ability declarations
test_checker_types.py	249	3,830	Primitive types, literals, binary/unary ops, generics, constructors, refinement types, arrays, tuples, zero-size container rejection (E135 for Map/Set — #1075), return/match-arm types, the fresh-ctor-var family (a bare None adopting the expected type at return/let/match #971, nested ctor fields #979, comparison operands #981, and call/op/init arguments #993 — with cross-ADT and None == None guardrail rejections), byte-arithmetic + integer-literal-range rejection (#420 split), the #898 cross-argument type-argument merge (eq2(MkErr(5), MkOk("x")) fully determines Res<String, Int> and type-checks; a per-parameter conflict eq2(MkOk("x"), MkOk(5)) is a clear E205; a determined-non-Eq type still type-checks), the #900/#939 generic-over-zero-size rejection (E206 fires only when the forall<T> READS @T and T erases to no WASM local — bare Unit OR a transparent Future<Unit> (#939) — in the body (direct return, match scrutinee, nested let/if) OR in a requires/ensures clause (#939); a @T-unread generic like firstInt/ignore, a boxed Option<Unit>, a Future<Int>, and the built-in async(IO.print(...)) over Unit all stay accepted), the #945 array-of-zero-size rejection (Array<Unit> / a bare [()] is E135 at both the type-resolution and array-literal gates — emitted exactly once, the literal gate defers to the annotation when both apply (including a refined { @Array<Unit> | p } annotation, whose RefinedType the guard strips via base_type), and a zero-size Array param reports E135 once via the general exact-duplicate diagnostic dedup (PR #938); Array<Int> stays accepted), the #1204 quantifier-bound gate (E128 for array/String/Float64 domains; count form, @Nat, refined-integer, and TypeVar bounds accepted), the #1206 handler-state cell gate (E336 when the declared state type diverges from the builtin State effect's resolved T — state_cell_decl_equal on resolved types, since is_subtype conflates Int/Nat and erases refinements, with refined predicates compared structurally so a refined-vs-refined divergence is caught; aliases of T, a refined alias on both sides, and two textually identical refinement aliases stay accepted, a TypeVar cell defers to instantiation, and a user effect's handler state stays free), and the E337 builtin-effect handle arity gate (bare handle[State], State<A, B>, and the Exn twin)
test_checker_int_nat.py	8	153	#755 — mixed Int <op> Nat arithmetic joins to the formal LUB Int (not Nat); direct expr_types observation that @Int.0 - 2, @Int.0 + @Nat.0, @Int.0 * @Nat.0, @Int.0 / @Nat.0, and @Int.0 % @Nat.0 synthesise Int (the DIV/MOD pins kill a per-operator numeric_join bypass nothing else in the suite catches), with Nat/Nat → Nat and Int/Int → Int guards against over-correction
test_checker_patterns.py	59	932	Pattern matching, match-arm typing, exhaustiveness, pattern/match coverage, bidirectional inference, typed holes (#420 split)
test_checker_functions.py	86	1103	Function signatures, slot references, result refs, calls, control flow, higher-order, where-blocks (incl. #969 closed-scope isolation over bodies + contract clauses, nested-where hint targeting, handler-vs-where hint ordering), expression diagnostics, IO operations, string interpolation (#420 split)
test_slot_naming.py	56	810	The rule table for vera/naming.py, the ONE slot/family naming renderer (#1208/#1209): each clause of THE RULE pinned to an exact rendered string — syntactic (alias-opaque) head vs fully-resolved type arguments, refinement at top level (base) vs argument position (the elided {@Int | ...} form) with alias parameters substituted BEFORE the refinement branch, Fn at top level vs the full fn(...) effects(...) spelling with a SORTED effect row in argument position, the total ? paths (arity mismatch, Decimal with arguments, a removed alias, an unresolvable type expression), type parameters shadowing same-named aliases, declaration-order alias visibility (a cycle and a forward reference terminate on the checker's opaque placeholder; a 40-deep in-order chain resolves, and a 400-hop chain — bare names and composites alike — resolves without a per-hop frame; a 300-level alias graph whose bodies mention SIBLINGS as well as ancestors resolves too, and at 1000 levels the resolver is instrumented to prove its nesting is CONSTANT rather than merely under this machine's recursion limit), slot-reference keys matching the binding side, family_name collapsing scalar / composite / parameterised-composite aliases and its fallbacks, family_base_name (identity vs representation, #1218), the refinement-binder derivation (including its deliberately syntactic argument naming), a declared ADT outranking the Decimal and removed-alias branches (a user data Float / data Decimal renders as itself and keeps its type arguments) while an alias still outranks a same-named ADT, ADT visibility bounded by declaration index in BOTH directions (an ADT declared below the alias body that names it is invisible to it, above it is not — and the bound stops at the alias body, so a top-level slot names the ADT whatever the order), and the env builder
test_slot_naming_differential.py	6	912	The load-bearing proof behind vera/naming.py (#1208/#1209): the checker's two naming entry points (_type_expr_to_slot_name and _slot_type_name, the latter also carrying every _slot_ref_key reference) are instrumented to record a (reference, module) rendering pair on EVERY call, and the whole .vera corpus (examples, conformance programs and their module fixtures, the PR #1202 probe corpus) plus a 31-program inline battery aimed at the alias / refinement / function-type / shadowing / declared-ADT corners (four of them carrying their own preludes, because the declaration-ORDER corner is about where the data sits relative to the type) is swept for ZERO divergence. The checker DELEGATES its naming, so the module side is what the checker returns and the reference side is a test-local statement of the rule (syntactic head, arguments through the checker's own _resolve_type, joined by canonical_type_name, plus the refined-top recursion) — independent by design, so a future edit to the module has to disagree with a written-down rule rather than re-baseline both sides at once. It is also what pins the join: vera/naming.py renders each argument through type_arg_name and restates only the Head<a, b> bracketing, and this side calls canonical_type_name itself. Check failures still contribute observations (naming runs while diagnostics accumulate); only parse failures are skipped, and counted. Self-protecting: floors on total observations, observations under a non-empty alias env, and — counted over the CORPUS alone, so battery growth cannot mask corpus decay — both the number of .vera files swept and the arguments naming an alias pre-resolution; a battery reach test that names the exact string each corner must render, so an entry contributing nothing fails instead of reading as agreement; a VeraError-only absorption around the check, so a compiler-level raise propagates rather than silently emptying an entry; and a live proof the gate can go red (perturb the module renderer, assert the harness reports it and that the reference side stands still)
test_slot_naming_blast_radius.py	15	337	The MEASURED radius of the #1208 core flip: every subsystem downstream of the checker (the monomorphizer, codegen, the verifier, the SMT layer) derives slot names AND slot-reference keys from vera/naming.py, and the radius is measured over the whole .vera corpus (check --json diagnostics for every file, run for every probe). Six shapes differ, all one class: a program that died on a dangling-slot [E699] now resolves and runs with the value the CHECKER's binding rule gives — each pinned by path and entry point with its expected value, so a regression that re-splits the naming names the program rather than failing diffusely. The six live in tests/conformance/, which is where the assertions read them. No check diagnostic moved anywhere (the checker was already delegating), and five slot-heavy sentinels outside the radius are asserted still clean. Also pins the two things the corpus cannot show: --explain-slots reporting the merged parameter stack under the checker's own name, and the module-scope rule — an imported generic's clone has its De Bruijn recount rendered in the DEFINING module's alias namespace (§8.4.1), not the importer's, or the merge goes unseen and the clone silently resolves onto the wrong parameter
test_family_naming.py	66	1,583	The State/Exn cell FAMILY is the cell the CHECKER typed (#1209): the checker resolves an effect instance's type arguments in full, so State<MaybeInt> under type MaybeInt = Option<Int> and State<Option<Int>> are ONE instance, and the family is named from the resolution rather than from the source spelling — a spelling-keyed family mints two host cells behind a green check for anything that does not resolve to a scalar. Pins the collapse where it is OBSERVABLE (a mixed-spelling program returns the shared cell's 7, not the split cell's -1 — bare alias, parameterised alias, and an Exn<Msg>/type Msg = String payload whose i32_pair (ptr, len) has to arrive through the SAME tag), the import surface collapsing with it (one state_get_ import, not two), the same collapse across a MODULE boundary (each side resolving in its own alias namespace), the negative (Option<Int> and Option<Bool> stay two cells, and the outer cell keeps its value — a renderer that dropped type arguments passes every positive and fails here), the resolved function-carrying family (#1219 — State<Handler> under type Handler = Option<fn(Int -> Int) effects(pure)> takes its resolution's name, and the alias and the resolution share one cell, proved by the value), the surviving bare-function-type fallback (the residue, refused downstream so the split is free), the refined cell's own family (#1218 — nested Pos/Neg route to their own cells, and a refined cell keeps its base's write guards and pair-ness), the linear-in-the-predicate symbol length with its MAX_CELL_FAMILY_SYMBOL backstop refused loudly on both targets, and the two formatter-coverage gates behind the predicate renderer, byte-stable family symbols for seven alias-free corpus programs (the emitted names are ABI), and the whole measured radius: the six shapes the flip moved (now in tests/conformance/), each at the symbols AND the value it renders to
test_naming_env_provenance_1208.py	45	2,097	The other half of the #1208 contract: every consumer is handed the ENVIRONMENT the checker rendered under, not just the same renderer. Four provenance seams, each pinned by the adversarial probe that exhibited it — an IMPORTED callee's contract rendered in its DEFINING module's alias namespace (a violated precondition that vanished, and its mirror, a correct call spuriously rejected, both under a Cnt that names different bodies on the two sides), an imported GENERIC monomorphized and verified in that same namespace (a lying postcondition that proved clean, plus a verifier↔codegen clone differential over the recounted slot references — the desync is invisible to a unit test on either side), a forall variable shadowing a same-named module alias wherever a generic signature renders (the mono clone, a body let, the verifier's collapsed premises, and the exported uninstantiated template), and the tester's SmtContext holding the narrowed scope its own names were keyed in — the last one behavioural, since a generator handed the wrong scope collapses two parameters onto one variable and returns NO inputs at all. Three of the seams are also crossed against a SECOND component rather than checked for internal consistency, because a wrong-but-consistent scope is invisible from inside one: the verifier's declared parameter names against slots.slot_table's, its where-helper scope against slots.fn_scopes' accumulation, and the monomorphizer's post-substitution names against what the consumers rebuild on the clone — each independent on the axis under test (which variables the two sides narrow by) but sharing fn_slot_scope/slot_name below it, so the hand-derived literal rendering beside every comparison is what a shared-renderer defect cannot satisfy. An imported generic nested under a non-generic function is pinned too — both its discovery-time recount and its verification-time clone must run in the DEFINING module's namespace. Three more seams arrived from the PR #1224 review, each with the false Tier-1 or miscompile that exhibited it: an UNPINNED callee (an imported generic's own where-helper, which the origin registry never pins) rendering in the module under verification rather than the entry program, whose absence let a violated precondition discharge as true and trap at run time; a callee's refined-RETURN predicate translated in the callee's namespace alongside its requires/ensures, pinned by provenance because today's bare-headed binder masks it behaviourally; and codegen's declaration-index space keyed PER NAMESPACE, without which a module's stamp turned the main file's forward alias reference into a backward one and a check-clean, verify-clean program read the wrong parameter through valid WASM. Two seams from the #1213 burndown close the same shape from the other side: the prelude's own aliases are injected only into the reserved Vera namespace, so no name a program can spell resolves on the codegen side alone (#1221 — the differential compares the checker's and codegen's partition of one signature, with the emitted WAT beside it), and an imported ADT is ordered at the index its OWN module gave it rather than the built-in floor (#1227), each with the control that differs by exactly the namespace under test. Controls carried alongside: the same programs with the alias renamed or the shadowing declaration removed, and the runtime oracle that shows the new E500/E501 agrees with the emitted code rather than merely reporting more
test_callee_contract_scope_1220_1225_1226.py	40	1,433	A callee's contract is READ in the callee's own module. Three burndown defects, each asserted against the runtime oracle wherever the two directions of a wrong namespace (an obligation that vanishes, one that fires for no reason) look identical from inside the verifier: an E501's Precondition: line quoted from the file that DECLARED the clause (#1220 — in the misattribution direction too, both files carrying a plausible requires on the same line number, plus the imported-generic where-helper whose clause sits past the end of a short importer and used to quote nothing at all); a bare-name call inside an IMPORTED callee's contract resolved through the CALLEE's module registry (#1225 — the false Tier-1 whose run traps and its mirror spurious E501, through the requires and the ensures path, against a no-collision control); and the refined-RETURN binder derived through the naming layer, so a refinement over a PARAMETERISED base pushes the key its own predicate looks itself up under (#1226 — single-module and cross-module, the second proving the derivation happens INSIDE the callee scope); plus the PR #1239 review round — a module's pinned registry holds what its OWN file imports (a DEPTH-2 chain, the shape the single-level corpus could not exhibit: requires and ensures directions, bare-vs-qualified tier agreement, a name outside the middle module's import filter still missing per §8.5.1, and the mirror gate that filling the registry does not re-export), and every part of a diagnostic follows the declaring module (location, file name and excerpt, including a clause past a shorter importer's end, with a multi-line clause quoted whole), and the characterization of the binder-reference walk's one documented exception — a CLOSURE inside a predicate owns the first @T.n in traversal order, whose consequence is a Tier-3 demotion rather than a fact assumed about the wrong term; and the mini-review round — an obligation carries the FILE its line number belongs to, so the documented (file, line, column) join between the two --json arrays holds for a module-located obligation, with the entry-file control and warm==cold parity, and a multi-line clause is quoted with its -- comments blanked (a -- inside a string literal surviving, which a naive split would corrupt)
test_alias_application_refinement_base_1237.py	11	398	A parameterised alias APPLICATION substitutes its arguments in the verifier's own resolver (#1237). type Box<T> = T; applied as @Box<Cnt> resolved to AdtType('T') — the alias's binder leaking as an ADT name — so a refinement over it failed the modelled-primitive gate, the refined-return fact was dropped, and a valid program was rejected with a spurious E501 while vera run returned the right answer. Both halves of the fix are asserted separately: the alias body registers its own parameters as type variables (substitute maps type variables, so an ADT-named binder is unsubstitutable however the application side is written) and the application substitutes. Plus depth (an argument that is itself an application, and an alias whose body applies another alias), the bounded direction (a consumer wanting >= 100 where the refinement grants >= 18 is still rejected, and the runtime agrees), and the gate that must NOT move — an unmodelled @Byte base resolves correctly and still degrades to a Tier-3 runtime check, with a consumer of its predicate still refused
test_exn_throw_payload_1268.py	42	1056	throw's payload is obligated AND runtime-guarded like every other narrowing site (#1268). throw(0 - 5) under effects(<Exn<Nat>>) verified at 4/4 Tier 1 with ZERO obligations while vera run returned -5 out of the @Nat payload — check-green, verify-green, silently wrong — because throw is a bare call with no function-registry entry, so the argument loop never saw it and the table-driven fallback added for the same hole at the State put was keyed on that one name. All three arms are asserted (the @Nat refutation, the refined refutation over a modelled base, and the @Nat->@Int widening obligation appearing where none existed), plus the #1251(b) concrete gate reaching the payload for free (throw(200) into an Exn<{ @Byte | @Byte.0 < 10 }> names the value; the satisfying twin proves at Tier 1), the user-effect contrast that localized the bug (a declared op's argument was loud for the same value — both are loud now, at the same site name), and the refined-alias payload spelling. The GUARD is checked against codegen rather than asserted: an undischargeable payload must land on the runtime-guarded tier3 leg, counted in the totals, and a run must confirm the payload really is stopped — the two together go red whichever side moves without the other (delete the emission and the runs go red; flip the flag back and the statuses do). Both arms are run at the boundary: a @Nat payload traps on -5 and delivers 5, a refined { @Int | @Int.0 > 0 } payload traps through the $vera.contract_fail channel on BOTH -5 and 0 — the value that clears the base's >= 0 and violates the predicate, so a sign guard standing in for the predicate guard fails here — and delivers 7. The type gate carries its own over-refusal control: an Exn<Int> payload has no invariant to violate, so a negative one is a correct program and must still return -5. Both REPRESENTATIONS are covered — a scalar payload in one local, and a @String-based one whose (ptr, len) pair has to be saved in two, checked over the ptr and put back in the right order (the satisfying twin is what shows the order). The soundness differential is the point of the guard rather than a property of it: the clause parameter's type is what the verifier hands every downstream consumer, so a consumer discharging ensures(@Bool.result) at Tier 1 from its @Nat parameter alone is asserted PROVED and then run — pre-fix the run reported a postcondition violation on that proved postcondition, with nothing else in the path (the argument is already @Nat-typed, so no call-site narrowing guard fires). A dischargeable twin proves the site is not merely always-loud, and the six Exn conformance programs are verified whole as canaries so obligating a position that had none names itself instead of arriving as one line of a corpus sweep. The adversarial round adds the three places the guarded PROMISE and the emitted guard could disagree in a direction no value oracle can see, because the program either never runs or runs identically either way: a refinement OVER a refinement is asserted tier3_unguarded AND E618-refused at compile in one cell (the mirror claimed a runtime check for a program that cannot be compiled at all — either half alone reads as consistent); the bare and qualified spellings of one operation are asserted to record IDENTICAL statuses as a differential rather than two literals, on both arms, with the run confirming which value is the true one (Exn.throw was disclosed unguarded while codegen delegated it to the guard-emitting dispatcher, and State.put had been since #1203); the #820 INTERSECTION at this boundary — a refinement over @Int keeps the widening obligation AND its guard beside the predicate's, pinned as a differential against the unrefined spelling (both must trap at u64.MAX, where the refined one used to return -1) with an in-range control so the guard is not simply always-on; and E504's rationale is read from a real diagnostic — reached through the site that IS still unguarded, a user-declared effect's operation argument — to pin that it no longer lists the throw payload among the sites with no runtime guard
test_refinement_binder_convergence_1208.py	16	459	Codegen's refinement boundary guard and vera/naming.py derive the predicate binder ONCE (#1208). A per-shape differential over a direct refinement, an alias hop, @Nat- and @Byte-based refinements (both range-conjoining), a composite base whose binder is a RESOLVED argument list, and two non-refinements that must be None on both sides — plus the property the convergence exists to hold, that the guard's binder equals the key a predicate's own @Base.n resolves to. A per-shape differential is green either way while two copies agree — which is exactly how a duplicated derivation drifts unnoticed — so the load-bearing assertion is a MUTATION: perturb naming.refinement_binder_parts and codegen's guard must report the perturbed binder. Codegen's two layered WASM decisions are pinned alongside — the loud E618 for a nested refinement base, reported ONCE per declaration however many call sites consult the derivation and however many clones a generic is instantiated into (two genuinely distinct sites still report twice), and no guard at all for an erased one (parametrized over @Unit and Future<Unit>, the corner that erases identically but is not spelled Unit) — plus runtime traps proving BOTH the @Byte and the @Nat range conjunctions reach the emitted check, each pinned by trap kind as well as by the conjunct its message names. The mutation perturbs the predicate as well as the binder name: the two travel by different routes, and the range conjunction lives on the predicate. The once-per-site dedup is keyed on a resolved location, so a cross-module pin holds up the premise that a location carries its owning file: two imported library modules of identical shape, declaring their nested refinement at the same line and column, must produce two diagnostics attributed to two files — each quoting its own module's declaration, which is also what catches an attribution pointing past the importer's last line
test_checker_effects.py	90	1,465	Effect declarations, abilities, effect subtyping, async effect, handler typing (#420 split), and the #1149 built-in-effect redeclaration gate (E152: divergent and faithful effect IO, codegen-only Exn<E>, a registry-parametrised sweep, and a differential pinning the gate's name set to what vera effects --json publishes)
test_state_exn_registration.py	30	1,298	#1210 — State/Exn host-import registration covers the whole handler, not just its body. Four shapes, one per sub-expression position the walk used to miss (a nested handler in a clause body, in the state-init expression, in a clause's with update, and an Exn handler in a clause body), each check-green and verify-clean and therefore required to COMPILE — pre-fix every one died at whole-module WAT compilation with unknown func / unknown tag; plus the i32_pair cell (handle[State<String>] in a pure function) that the walk skipped in silence, now the same loud E607 the declared-effect gate emits. The registration-completeness differential is the cross-component invariant itself: over every examples/ + tests/conformance/ program that compiles, every state_* / exn_* symbol the emitted WAT REFERENCES must have a matching import or tag DECLARATION — a desync between the registration pass and the lowering pass is invisible to a unit test on either. Round two adds the Exn twin of the silent skip (handle[Exn<Unit>] in a pure function — the walk called the shared tag registration and discarded the verdict, so it compiled where the declared-row spelling was a clean E612) and the four CONTRACT positions, which are lowered code: a handler in a requires, an ensures, an assert, or a decreases measure. The differential gained a validation leg — every HANDLER-BEARING module is handed to wasmtime.Module through the exceptions-enabled engine execute() uses, because a symbol declared at the WRONG TYPE passes the name comparison while being invalid WASM, and 10 of the 30 handler-bearing modules fail to load with wasm_exceptions off — a supported wasmtime configuration, though the current runner defaults it on. The conformance suite's deliberate negatives are filtered out of the sweep: they never reach codegen through vera check. Carries floors on programs swept, modules validated, summed symbol references and globally distinct symbols, plus three can-go-red tests: the State and Exn extractions each stripped of their declaration lines, and a planted retyped import that only the validation leg catches. Round five adds the three positions no corpus program contained — a destructuring let's value (which also disarmed the E612 gate), a module call's ARGUMENTS, and a signature refinement predicate reached through the alias table — and a cross-module shape test for the module-call leg. Round seven adds the boundary-guard routes that enumeration missed (a tuple parameter's components, a tuple return's, and a closure's refined formal and return) and the co-extensiveness half those shapes cannot show: a refined tuple behind a CLOSURE formal must declare nothing, since the closure path emits no component guards, and the nested-refinement (E618) and erased-base bails must stay silent registrars too. Plus the cycle guard on the closure signature leg, asserted in both directions — the walk terminates, and with the guard neutered the same walk blows the recursion limit
test_closure_lift_boundaries_1234_1235_1245.py	18	757	Closure lifting at refinement boundaries — three burndown defects of one seam. #1245: _lift_pending_closures ran BEFORE _compile_postconditions, so a closure created while lowering a refined-RETURN guard, a tuple return's component guards, or an ensures(...) predicate was registered and never lifted — the table stayed empty, its call_indirect was orphaned, and the #1185 propagation dropped the function and every caller: a check-green, verify-clean program compiling to ZERO exports. The param-position twin (lowered before the lift, so it always worked) is carried as the control that makes it an ORDERING defect, the ensures-clause twin shows the same bug with no refinement in sight, and a violating return asserts the lifted guard ENFORCES rather than merely existing. #1234: the lift worklist fed itself — a refinement whose predicate holds a closure refined by a type whose chain leads back to it (type SelfRef = { @Int | ... fn(@SelfRef -> @Int) ... }, and equally a mutual A -> B -> A or a three-type cycle) had each lift's own boundary guard queue an AnonFn for ever, and vera compile never returned. All three cycle lengths are asserted on a daemon thread with a wall-clock budget, so a regression fails fast instead of hanging the suite, and each on the [E602] naming the closure it refused (a guard that never fired cannot produce it). Two controls carry the other half — the guard is keyed on the lift CHAIN, not on everything already lifted, so fn f(@R, @R -> @Int) and a diamond, which each legitimately lift one predicate's closure twice, must still run; mutation-measured, they are the only two tests a seen-set spelling reddens. #1235: a Tuple<PosInt, Int> formal crossing into a closure was unguarded where the named path traps — both spellings of the same boundary are run against each other, violating and passing
test_byte_literal_joins_1212.py	25	759	#1212 — a @Byte literal inside a value-position join lowers at the i32 Byte width. @Byte is i32 (spec §11) while an int literal defaults to i64.const, and the #865 / #1092 coercions each tested for a TOP-LEVEL IntLit — which the checker's bidirectional coercion is equally happy to type inside an if or match branch. Ten write boundaries are parametrized with the literal in a branch (let, handler state-init, clause-dispatched put, bare put, get-clause resume — verbatim the form the E602 clause-lowerability skip message recommends — a clause with update, a @Byte call argument, a generic constructor field at Box<Byte>, a lifted closure's own RETURN whose named twin had been coerced since #865 while the closure path had no such step, and a HETEROGENEOUS join at a @Byte return, where the arm the result-type decider reads is already i32 and a sibling is a bare literal — arm ORDER decided which way that one failed, so both orders and both paths are pinned). The module docstring states what that list is and is not: measured coverage, since the checker's single Byte coercion makes the true enumeration "every position propagating a Byte expectation", which nothing enumerates in one place, each a check-green program that failed WASM validation with type mismatch: expected i32, found i64 before the fix. Every case carries a VALUE oracle (200, distinguishable from every other constant in its fixture) rather than merely asserting the module runs, and a separate test drives the OTHER branch so a fix that marked only the arm the result type is read off would still fail. The controls are the load-bearing half: a plain @Int join must stay i64 — pinned on 5,000,000,000, which an i32 store cannot represent, so a spreading mark is a wrong VALUE and not just a validation failure — a Byte join with no literal arm must be untouched, and a Byte-RETURNING literal join must keep its own #865 return coercion. The constructor-field case runs through the real pipeline (checker artifacts threaded), because the #1092 width keys on the checker-recorded target type
test_closure_boundary_widths_1255_1256_1269.py	52	973	Widths and pointer-ness at a closure or effect boundary — three burndown defects of one seam, each a boundary answering "what is this declared type" from something other than that type. #1255: GC pointer-ness was read off the SYNTACTIC head, so type SmallByte = { @Byte | ... } was rooted on the shadow stack at the closure parameter, return and capture and at the two named-function twins. The oracle is a DIFFERENTIAL against the @Byte spelling of the same program rather than an absolute push count — these bodies must allocate or no prologue is emitted at all, so they legitimately root their own intermediates — with the base spelling's own count PINNED beside it, because equality alone also holds when both spellings root the scalar, which is the pre-fix state and what a mutation deleting the exclusion outright would produce. A genuine pointer at each of the four boundaries is the control (rooting nothing anywhere satisfies the differential too), and every shape runs under VERA_EAGER_GC=1 — a collection at each $alloc, where removing a load-bearing push reads back as a wrong value rather than as a passing test. The heap-layout invariant the defect was inert behind is executable here: a module with no string pool at all — the exposure the issue named — still starts its heap above the inline scalar range, and shrinking the two constants that create that margin fires the build guard. #1256: the apply_fn call_indirect signature took each parameter's width from the ARGUMENT, so a @Byte formal fed a literal registered two incompatible $closure_sig types and trapped; asserted by run AND by the emitted signature list, since a value oracle alone would also pass if both sides converged on the wrong shared width. The join spelling, the refined formal, the function-type-alias arm of the formal recovery, a directly-called named twin and an i64 control (pinned above $2^{32}$, which an i32 parameter cannot carry) surround it. #1269: throw's payload was not a @Byte write boundary, so throw(5) into Exn<{ @Byte | @Byte.0 < 10 }> put an i64.const under an i32 tag and failed WASM validation at load. Both halves of the width agreement are pinned — a fix that widened the TAG would also run, and would put a Byte cell at eight bytes everywhere else — across the bare, aliased, refined, branch-literal, qualified-Exn.throw and thrown-inside-the-handled-body spellings, the last two reaching registration paths the others do not
test_nested_handler_clause_ops.py	27	971	#1211 — a handler clause body's bare get/put belongs to the handler's DECLARATION scope, not to the body it refines. Eight nested shapes, each asserted on all three components (checker accepts, verifier discharges clean, compiled program returns the checker-derived value): put in a put clause and in a get clause, a bare get in a with state-update expression, depth-3 nesting proving the IMMEDIATELY enclosing handler wins, the qualified State.put spelling, a nested handle expression inside a clause body (its registries must be restored to the declaration's, not the intervening handler's), and the two op-result-type mirrors — a bare get(()) in match-scrutinee (_effect_op_result_wt) and array-element (_effect_op_result_vera) position, both of which emitted invalid WASM for a check-green program before the alignment. Every oracle is derived from the checker's story, never from what codegen emits, and a meta-test asserts each shape still SEPARATES enclosing-cell from inner-cell routing (the pre-fix value is recorded per case) so none can go vacuous. Round two adds the two dispositions of an EMPTY enclosing handler stack — the declared effect row (the only route that reads the restored _effect_ops, which every handler-enclosed case bypasses) and the outermost handler in a pure function (E122 at check) — the enclosing handler's own clause running on the outward-routed op (a transforming with one level out: 300100, where the intrinsic reading gives 300050), IO.print inside a clause body, the #1233 same-family refusals (nested handler, with expression, declared row) with their different-family control, and the outward-re-entry depth cap (below it, at it with a WAT-size bound, and past it as a loud E602)
test_handler_op_ownership_1284.py	15	419	#1284 — whose declaration a bare get/put call site denotes. The checker resolves user-fn-first (pinned directly: an over-applied get under a handle[State<Int>] reports the USER signature's arity), and codegen used to answer that question twice more and differently — the declared-effect row withheld the op when a function owned the name, the handler expression overwrote unconditionally. Four shapes from check-green source, each asserted on the CHECKER's value and on the dispatch target in the emitted WAT: a handled body returning the cell instead of the function's answer (silently 5 for 4), a @Bool-returning user get whose module WASM validation rejected, same-family nesting refused outright with a spurious [E602] naming a State operation the source never contained, and different-family nesting emitting the enclosing cell's getter at the wrong width. A parametrized differential runs all five shapes (the four plus a user put) as one table with each case's pre-fix behaviour recorded, so a case that stops distinguishing the two answers is visible rather than vacuous; the controls — an unshadowed handler and an unshadowed declared row, both of which must still reach the intrinsics — are what a fix that simply stopped installing the ops would fail, and new(State<Int>) under a shadowed op name pins that the #1285 family registry composes with this
test_new_state_family_1285.py	9	323	#1285 — which cell new(State<T>) reads under a multi-State effect row. old() has been family-keyed since #1205/#1209 while new() read the name-keyed op registry, so the two sides of one ensures clause read different cells: effects(<State<Int>, State<Bool>>) with ensures(new(State<Bool>) == …) was check-green and verify-green, put state_get_Int's i64 into the Bool comparison's i32.eq, and died at load. Three multi-row cases — the width-mismatched shape that could not load, an Int/Nat pair that loaded and answered about the wrong cell, and old() beside new() of one family, whose unchanged-cell claim the runtime refuted on a contract the verifier had discharged — plus the single-State and alias-spelled controls the whole existing corpus exercises. Each cell is seeded from a caller's handler at a value the other cell is not holding, so a wrong-cell read cannot coincide with the right answer, and a deliberately false postcondition asserts the Tier 3 runtime check really traps, without which every "the program runs" assertion here would prove nothing
test_adt_membership_scope_1253.py	5	334	#1253 — a checker↔codegen DIFFERENTIAL over one module's slot table. _adt_layouts is one map across every absorbed namespace, so a sibling module's ADTs were members of a module that never imported them while the checker kept the name opaque: ['Array<?>', 'Array<Int>'] against ['Array<Float>', 'Array<Int>'] for the same signature. Each case renders the module's parameters through vera.naming twice — once against the environment the checker binds that module's declarations in (built by the production _modules_visible_to + check_program path, not a rebuild of it) and once against codegen's _alias_env inside _module_alias_scope — and asserts both the agreement and the checker's own value, so an alignment on the WRONG name still fails. Three membership cases (an unimported public sibling, a private sibling, and the imported positive control that is green before and after — what separates scoping the membership from erasing cross-module ADTs) plus the entry program's own view, which must keep seeing the ADT it imports by name
test_prelude_decl_stamp_1287.py	4	240	#1287 — the prelude's declaration-index block is a fact about the prelude. _stamp_decl_order guarded the PRELUDE write on _decl_order, the active (main-file) namespace, so a main-file type Option = Int — accepted under §8.4.1, and not a data, so it does not suppress the prelude's own Option — made the guard fire and left Option out of _prelude_decl_order entirely, with every later prelude declaration shifted one place earlier because the counter never advanced. That map is the base layer under every module's index space ({**prelude, **module_own}), so the wrong index reached AliasEnv.data_types as _BUILTIN_DECL_INDEX. Stated as an INVARIANCE — the same program with and without the shadowing alias must stamp an identical prelude block — plus the module-namespace index it feeds, and a control that the main file's own stamp still wins its own namespace (which a fix stamping _decl_order unconditionally would break)
test_prelude_adt_namespace_1277.py	61	1034	#1277 — one file's data Json must not evict the prelude's from another namespace, and a module declaration contending with a prelude one must be loud. Three halves, pinned by disjoint cases so a regression in any is attributable. Acceptance battery: all eight prelude ADT names × {module declares it alone, entry also uses the prelude's}, asserting that no cell reports [E602]/[E620] and that a cell which does not report [E621] emits every public function the entry declares — the silent-drop check, and the guard against the rail's original four-of-eight coverage returning (the layout harvest skips a built-in name, so a layout-keyed rail saw data Json and never data Option). That battery accepts either answer per cell by design, so the §8.4.1 injection split is pinned separately: an entry that never names the type must still report [E621] for the four every program compiles (Option, Result, Ordering, UrlParts) and must stay clean for the four injected on demand, with a partition cell holding the two halves to the battery's own name list. Plus two-declaring-module cells in both import orders — the entry's import order is derived from the parametrization, and the both-differ cell asserts the two reports arrive in that order, so the pair cannot quietly become one program compiled twice — covering restate+differ, both-differ, both-restate, and a non-prelude control that must stay E609's, because the rail asks every declarer and a first-wins lookup made it order-dependent. Plus the restatement control for all eight: a module that restates the prelude's shape shares the one layout, compiles and runs, and must not be refused — measured legal at the branch point, and refused by the rail's first form for four of them. Rail detail: severity, the module's own file and line, the description naming the type and the module, the empty exports, and cmd_compile returning 1 over a cmd_check-green program. Floor: the checker registers the prelude ADTs in every TypeEnv unconditionally, so codegen's membership must too; asserted as a differential against the checker's own data_types in a module namespace, and on the entry namespace's member set for the issue's measured shape. prelude_adt_names() is compared against inject_prelude itself, and data_decl_shape is pinned on the directions that matter — a renamed type parameter is the same layout, a reordered constructor is not, an alias-spelled restatement keys EQUAL to the prelude's, and a type parameter shadows an alias of its own name. Each declaration is resolved through the aliases of the namespace it was written in, one side only: the two whole-program cells pin both directions of that — a module restating the prelude through type Payload = String; must compile, and a module hiding a mismatch behind type Array<T> = Int; must not
test_import_visibility_entry_point_1244.py	6	269	#1244 — vera check reports the same diagnostics whether it was given a module or a file that imports it. Registration alone says what a module DECLARES; the importer never checked its bodies, so a name a module never imported was rejected standalone (E200, §8.5.1) and accepted in silence through an importer. Written as EQUALITY between the two entry points rather than as "the importer warns", because the property is agreement — a future change making the standalone verdict lenient would satisfy a one-sided assertion and must fail here on the standalone leg. Six cases: the leaked unimported name, the honest control that imports what it uses (green before and after, so the new body check is the visibility rule rather than a blanket rejection of cross-module programs), the issue's type-error-through-importer shape (an @Int call bound to a @Bool slot: check-clean, Tier-1, failing at compile), a diamond proving each module is reported ONCE (the body check is memoised by path across nested checkers), and both entry points into an import cycle proving the memo terminates it
test_clone_body_declaring_module_1241_1243.py	5	344	#1241 + #1243 — an imported generic's clone body resolves its bare calls in the DECLARING module, on both sides. The verifier's lexical lookup fell through to the importer's registry (_declaring_module_scope swapped the naming env, source and file but not the function registry) and codegen's clone-emission door was the one door that did not thread the module's intra-rename map, so glib's gen called the importer's need. The two halves are one routing rule, and the tests are written so neither passes alone: each case asserts the vera verify verdict AND the vera run value together, so the verifier half alone (which makes verify clean while the compiled program still traps on the postcondition it just proved — the measured false Tier-1) fails the same test the codegen half alone (right value, verify still refusing) fails. Every expected value comes from the module verified and run STANDALONE, never from what the importer produces. Shapes: a private direct callee, a two-hop private chain, the type-discriminating pair (@Int vs @Bool — check-green source that emitted invalid WASM), and the unshadowed-callee control that was correct before and after, which is what pins the defect to the SHADOWED name rather than to cross-module calls in general
test_module_generic_namespace_1274.py	24	1,015	#1274 — a module generic that does not own the importer's bare name is reached under mod$<path>$name. Pre-fix only PRIVATE module generics were routed that way (#1000), so a PUBLIC one collided with the importer's same-named generic in the clone-name space: both files' gen2 mangled to one gen2$Bool, one overwrote the other, and the module's own body ran the importer's — a false Tier-1 (check/verify clean, the module's proved ensures violated at run: 999 where the declaring module answers 111). The full visibility matrix (module generic × importer generic), the import-filter dimension (out-of-filter, in-filter, wildcard), the unshadowed-out-of-filter cell that assembled to unknown func $gen2, and a type-discriminating shape whose two clones have different WAT result types. Each cell asserts the verify VERDICT and the runtime VALUE together in one test — a clean verify beside a violated postcondition IS the bug, so splitting them across sibling tests would let it hide — against the standalone library as oracle, and re-checks that the importer's own generic still answers its own value. The per-module both-sides differential lives in test_monomorphize_differential.py. Two further families joined after the adversarial round: the module→module hop — a module's bare call to a DIFFERENT module's qualified-only generic, which the per-module classification never rerouted, in both a LOUD spelling (a contract pins the answer, so a captured call traps) and a SILENT one (every contract admits both answers, so only the value distinguishes them) plus the two-hop shape where the entry never imports the declaring module at all; and the shared-input pair, which pins that the two sides compute the importer's occupied bare names identically — codegen reads them after Pass 0's helper renames, the verifier from the pre-transform AST, and a non-generic where-helper named gen2 made the same imported generic bare-name-owning on one side and qualified-only on the other. The idempotence of that derivation is asserted directly across BOTH Pass-0 transforms and their composition — over a fixture carrying every helper shape it distinguishes (non-generic under non-generic, under a generic parent, under a generic helper, and a generic helper), since a fixture missing one would let a partial assertion look total — with each shape's membership pinned individually beside it, because idempotence alone would hold for a derivation that answered the same WRONG set every time. Two more families close the visibility dimension: the transitive one, driven through the production ModuleResolver (a hand-built ResolvedModule defaults direct=True and would never reach the path), asserting that a module reached only transitively has ALL its generics qualified-only — the entry's namespace does not hold them at all; and the user-written qualified call (deep::gen(true) where the importer declares its own gen), which must key its instantiation to the module's declaration rather than to whoever owns the bare name
test_module_shadowed_generic_effect_op_1310.py	4	410	#1310: a qualified-only (shadowed) module generic's instantiation discovery had no effect-operation registry at all, unlike #1207's unshadowed discovery walk. idg(get(())) inside handle[State<Int>], where idg is a forall<T> generic declared in an imported module, checked and verified clean and then compiled with [E602]/[E620] notes and no main in the emitted module: the WASM call-rewrite correctly named mod$mlib5$idg$Int, but _collect_shadowed_qualified_calls (codegen) and its mirror walk_seed (the verifier's _collect_shadowed_qualified_instances, #732) fell through to the phantom-var Bool default for the effect-op argument, so mod$mlib5$idg$Bool was the clone actually emitted and verified. The issue's own repro is pinned end to end (no E602/E620, the checker's own clone name in the WAT, and the runtime value), plus a nested-distinct-state cell (mirroring #1207's own) that would still pass a fix stopping the Bool default without preserving HandleExpr's merge-over-the-enclosing-scope semantics, now also asserting the outer cell's clone is absent, matching the first cell's shape. Two more cells run the #732 differential directly on both fixtures: codegen's _emitted_instances and the verifier's _instances must name the identical instantiation, red if either side's HandleExpr merge is reverted alone
test_ambiguous_import_refusal_1304.py	40	1,202	#1304 — two imports supplying one bare name are refused, in every namespace. Spec §8.5 ordered a local declaration against an import and gave the qualified form for a clash it hides, but defined no order between two IMPORTS of one name, and neither did the implementation: a module importing two dependencies that each export forall<T> fn gen — one @Int-returning, one @Bool — bound its bare call to whichever supplier a set of module paths yielded first, so one unchanged file was check-green on one run and [E121] body has type Bool on the next (at the branch point: accepted on hash seeds 0, 2 and 3, rejected on 1, 4, 5, 6 and 7). The load-bearing cells are the DETERMINISM ones — each import order checked in four fresh subprocesses under four PYTHONHASHSEED values, asserting one byte-identical verdict including message and location, which the base tree cannot satisfy and which a merely deterministic PICK would also fail (the refusal is what removes the choice). Around them: the refusal is definition-gated like the E608 rail it generalises, so an unused clash is still refused and swapping a bare call for the qualified form does not lift it; the two escape hatches — a local declaration (§8.5.2) and a selective import — are asserted to their RUNTIME VALUE, since a disambiguation resolving to the wrong supplier is silent at check and wrong at run; four non-ambiguous controls (one supplier, disjoint names, a private namesake, an out-of-filter namesake) hold the refusal to bare-name ambiguity; and the emitted code is held to a typecheck-phase range, because reusing a codegen code would carry #1304's own complaint — a scope question enforced at the wrong layer — into the fix. A subprocess canary pins that every fresh interpreter measures this checkout
test_module_generic_collision_1281.py	20	809	#1281 — E608 must not refuse two modules' PROVABLY DISTINCT generics. A generic emits nothing under its bare name, and since #1274 its clones live in a namespace chosen per OWNER, so the diamond (base public, mid1 private, both named gen) cannot overwrite anything — and was refused outright, with vera verify returning rc=0 beside the refusal. Each door now answers its own module's generic (555 + 111) against the standalone oracles, and the emitted module carries mod$…$mid1$gen$Bool and mod$…$base$gen$Bool with nothing in the entry's bare clone namespace. The relaxation is gated on three conditions, each with its own cell: both declarations are top-level generics (a generic beside a non-generic keeps the refusal), at most one owns the bare name (asked of the predicate directly, since end to end the ambiguity gate catches that shape first), and no namespace can name both — a module importing two dependencies that each export gen would resolve its own bare call to one of them, and spec §8.5 refuses the name outright rather than ordering the two imports (issue 1304). The CHECKER reports that (E155) and this rail is its backstop, so both cells drive the shape through build_multi_module_past_check and assert both layers: a rail no test can reach is one that can rot into a relaxation nobody measures. A namespace that declares its own gen is not ambiguous however many dependencies export one (§8.5.2). The registration half — a qualified-only generic contributing no bare _fn_sigs or _fn_ret_type_exprs entry — is pinned by two STRUCTURAL cells, one per table, and its docstring says why: with #1299's scope narrowing in place both withholdings are defence in depth, reverting them leaves every suite and the whole conformance corpus green, and they are kept only because four consumers read those tables per NAME and nothing but their current internals stops each from picking one
test_lexical_fn_scope_1299.py	56	1,554	#1299 — codegen's bare-call ownership table must be the CALL SITE's lexical scope. The #1284 predicate is one rule over two tables, and codegen's was set(_fn_sigs): every symbol the whole compilation absorbed, including names the compiling body cannot see, so a bare get(()) the checker resolved to a State operation was lowered as a call to some other declaration. Four routes, all check-green — an imported module's private get, a public one a selective import excludes, a where helper of a forall<T> parent (which keeps a bare key beside its clone-qualified one where a non-generic parent's does not), and the ability operation show, which E151 does not reserve and which reaches the same table through the INTRINSIC gate rather than the op one. Where the widths agreed the module loaded and answered the invisible declaration's value (7007 for the cell's 42007); where they differed it failed to load; the generic-where route is always loud (unknown func $get). Every expected value is the checker's, PROVEN by a type oracle rather than assumed — the invisible get returns @Bool while the caller returns @Int from it and checks green — and each route carries a rename control. The visibility matrix (public/private × in-filter/excluded/wildcard × shadowed/unshadowed × direct/transitive) asserts the verify verdict and the runtime value together per cell. The two directions are pinned at once: the sibling loses the name, the generic TEMPLATE keeps it (asserted on the emitted instruction stream, since monomorphization supersedes the template and a value assertion would be green either way), and a lifted closure — compiled through its own WasmContext — inherits its parent's scope. Four table invariants sit beside them: the scoped set is a subset of the registry, every $-bearing key stays in it, prelude names stay in it, and every emission door supplies a declaration its own helpers
test_phantom_generic_instances_1271.py	14	358	#1271 — discovery inside a still-generic scope must not instantiate a callee at an ENCLOSING scope's type VARIABLE. pick(@U.1, @U.0) inside forall<U> fn helper bound pick's variable to the NAME U, so a pick$U clone was emitted whose parameter has no WASM type and which the compilability pass then skipped with a loud [E604] — the noise that kept #1223's shapes out of the conformance suite. Drives the four #1223 fixtures plus a mutual-recursion shape (two sibling generic helpers under a generic parent, whose phantoms include one arriving through a callee's declared RETURN type, leaf$W), asserting on ONE compile that no clone is keyed by a type variable, that no E602/E604/E605 skip is emitted, AND that the genuinely concrete clone is still there — the third assertion being what separates the filter from an over-filter that would take the real instantiation with it. Plus the primitive-spelled binder matrix (forall<Int>, <Bool>, <String>, <Float64>), each row instantiating a sibling at exactly the type its binder is spelled like — a shared idw(5) would have let every row but Int pass for free — asserted on the clone set AND on the program still running; with the Q-binder control that keeps a genuine type variable filtered, so the fix cannot degenerate into "never filter". That control CREATES a live phantom candidate — a generic helper under a generic parent, handing its callee an argument typed by its own binder — because a control that merely fails to create one holds under any filter including none; mutation-checked by disabling the filter, which turns it red
test_handle_exn_divergent_result_1276.py	10	391	#1276 — a handle[Exn] whose clause body AND handled body both diverge emitted a result-LESS block into a result-expecting context: check-green, verify-green, rejected at load with type mismatch: expected i64 but nothing on stack. Four divergent shapes (the issue's Int rethrow, the Byte payload spelling #1269 unmasked, a three-deep rethrow chain, and a clause diverging through both arms of an if), each asserted on valid WASM AND on the observable — the OUTER handler's clause value, 1000. Paired with the Unit TWIN, which infers None for the same reason but DOES complete: it must keep running and its WAT must contain no unreachable at all. The pairing is the point — result_wt is None means two things wanting opposite lowerings, and a fix that terminated both would trap a program that runs. The MIRROR family covers a clause that throws on one path and COMPLETES on the other (if and match spellings), where the inference read only the then branch / arm 0, answered None, and left the completing path's value stranded in a result-less block; the if case appears twice with different thrown values so both the throwing and the completing path are exercised from one inference
test_infer_vera_type_join_1286.py	26	577	#1286 — the VERA-level siblings of #1276's WAT join. InferenceMixin._infer_vera_type (the WASM call-rewrite consultor) read then_branch only and arms[0] only, and Monomorphizer._infer_vera_type_name (the instantiation-discovery consultor) read then_branch only and had no MatchExpr arm at all — so a branch that throws, naming no type, decided the answer for the whole expression. Two symptoms from check-green (and, with contracts, verify-green) source: as an array-literal ELEMENT the None raised CodegenSkip and the declared main simply left the exports with a loud [E602] note, and as a GENERIC ARGUMENT it left the type variable unbound, so idg$Bool — the phantom-var default, an i32 clone — was emitted for an i64 Int argument and the module failed to load. Seven witnesses (array literal in the if, match and pair-representation String spellings; generic argument in the if and match spellings; the constructor FIELD behind the same conditional), each asserted on the value, on main surviving into the exports, and on the absence of the skip note — the drop is quiet at the value level once the function is gone. The seventh witness is the consultor-AGREEMENT case, where every arm completes and nothing diverges: the rewrite named idg$Int from arm 0 while discovery named the phantom default, and the caller was dropped on a dangling target — which is why the repair lands on both consultors together, the clone-name agreement contract (#772) making the pair the unit. Each witness carries its ARM-SWAPPED twin and the pair must agree, so the join property under test is order-invariance rather than a remembered value; a WAT assertion pins WHICH clone the module carries, since a value can be right for the wrong reason. The PR review round found the same divergence one shape over and the sweep it prompted found a third, both closed here: discovery had no Block arm, and the transformer leaves a braced match-arm body AS a Block, so Some(@Int) -> { let … } named nothing there while the rewrite named the concrete clone — idg$Int emitted and never registered, main dropped from a check-green program. It only reaches a wrong answer when no later arm yields either, so the witness pairs the block-bodied arm with a throwing one; the braced-if variant needs the branch TAIL to be a block in its own right, a let inside the branch being a statement. The third is a handle in argument position, a presence cell since it has no branches to exchange. An IndexExpr argument dangles the same way and is deliberately NOT closed here, tracked as #1327 — the rewrite's arm resolves chained indexing, aliases and Future payloads against codegen tables the monomorphizer lacks, so a partial mirror would trade "both say unknown" for "the two disagree". WAT membership is tested through wat_fn_names / wat_calls, not in wat: the substring form is a prefix test that a longer mangled symbol satisfies, which is exactly how one clone impersonates another. Mutation-checked one edit at a time: reverting the rewrite-side if fails 13, its match 8, the discovery-side if 8, match 9, Block 6 and HandleExpr 2, and all six at once fails all 26
test_generic_under_generic_callees_1223.py	8	298	#1223 — a generic where-helper under a GENERIC parent instantiates its own generic callees. The helper is monomorphized only during clone hoisting, outside the worklist that rescans every clone it emits, so a top-level generic called from the helper body was discovered only in its still-generic spelling (pick$U, binding the enclosing type variable's NAME) while the rewrite called pick$Bool — E602 skip, E620 drop of the parent and of main, "No exported functions" from a check-clean, verify-clean program. Four shapes — a user generic, the prelude twin (option_unwrap_or), two levels of generic nesting where the INNER helper is the caller, and the non-generic-parent control that compiled before the fix and must keep compiling (it is what proves the trigger is the generic ancestor rather than the nested helper) — each asserted on no E602/E620, the checker's run value (the helper's argument order is non-commutative, so a miswiring gives 7 instead of 3), and a REGISTERED-vs-RESOLVED differential. That differential captures the emitted mono-decl names rather than _emitted_instances (whose generic-under-generic entries are keyed by the concrete-free lexical chain, not by the per-clone emission name the rewrite calls) and captures the rewrite side on _resolve_generic_call rather than from the WAT, because a desync skips the calling function and removes the dangling call along with it. The verifier's half of the pair is pinned in test_monomorphize_differential.py's inline corpus, not here
test_mono_effect_op_naming_1207.py	9	339	#1207 — monomorphization discovery and the WASM call-rewrite name ONE clone when an effect operation fixes a generic's type argument. A differential over the two consultors, not a unit test on either: the compiler's own E602 ("call target not registered in this module") IS the two sides disagreeing, so each case asserts no E602/E620, and additionally pins WHICH name they agreed on — an alignment on the wrong one still fails. Four instantiation-driving shapes (get(()) as an array-literal element under a plain State<Nat> cell, under a type Count = Nat alias cell whose clone must be pick$Count, in a function whose operation comes from the DECLARED effect row rather than an enclosing handle, and in direct argument position), plus the array_append builtin-argument control and a shadowed-name control — a user get(@Unit -> @Bool) is NOT an effect op in a declared row, so the clone must be pick$Bool and not the cell's; that case is green before the fix as well as after, which is what makes it a guard against the alignment over-reaching rather than a second copy of the repro
test_effect_op_determinism.py	9	504	#1215 — bare effect-op resolution order: the built-in State and Http both declare get, so effects(<State<Int>, Http>) is a two-candidate row with no user effect declaration needed. The two candidate bindings are made to produce DIFFERENT observables (the source-order program runs to 70; the reversed row is a loud E217 naming Http.get), swept across six PYTHONHASHSEED values in child interpreters so a frozenset-order flip cannot pass — plus the innermost-handler-beats-declared-row precedence case, a signature-level assertion that the resolved OpInfo follows the recorded order both ways (including the deterministic name tiebreak for a row member no order tuple mentions), and the qualified-lookup control. The type-ARGUMENT sibling rides here too: effects(<State<Int>, State<Bool>>) (two independent cells, spec §7.3.3) had the identical frozenset dependence in _effect_type_mapping, and codegen took the LAST instantiation in the row where the checker takes the first — both now source-order-first, swept the same way. A sixth sweep covers the public ordered_effect_row() fallback for a row member no order tuple mentions: its two members share the effect NAME and differ only in type ARGUMENT, so a name-only sort key ties them and hands back frozenset order — the order AND the _effect_type_mapping selection it drives are both asserted stable across the same seeds. Two further sweeps take that structural key down a level: a type argument may itself be a FUNCTION type, whose own effect row was rendered by pretty_effect — so two outer instances differing only INSIDE a nested row (by a refinement's predicate, or by a type variable's built-in marker) tied again, and both legs are asserted single-outcome across the same seeds, separately, so a regression names the elision that came back
test_db_effect.py	9	136	#229 — the built-in <DB> effect: DB.query / DB.execute type-check under effects(<DB>) (E122 without it; E204 on a non-String SQL argument), plus is_db_sql_op — the predicate the #309 gate keys on — gating any DB.query/DB.execute by parent_effect == "DB" + op name (the same axis codegen routes to the host on), so a user effect DB shadow's op IS gated (it would still reach the host) while an unrelated effect's query is not — the shadow is itself rejected at its declaration since #1149 (E152), so this predicate is defence in depth; a checker↔codegen differential pins the gated set to the built-in DB ops
test_db_marshalling.py	35	234	#229 — the <DB> marshalling helpers: Array<Option<String>> params (inbound reader), Array<Array<Option<String>>> query grids (_alloc_result_ok_rows) and Result<Int> row-counts, round-tripped through an InstanceCaller over a real compiled module — each case run normally AND under VERA_EAGER_GC=1 (every $alloc fires $gc_collect), the large-grid case forcing free-block reuse; mutation-validated (dropping a shadow-stack root corrupts the read-back / SIGBUSes the swept-pointer read)
test_db_runtime.py	21	301	#229 — the <DB> host binding (vera/runtime/db.py) on stdlib sqlite3: create/insert/select round-trips against :memory:, NULL cells → None, the affected-row count (incl. the -1 DDL sentinel), a BLOB cell UTF-8-decoded with replacement, the Err-not-crash error path, an unopenable VERA_DB_URL deferred to an Err (not a host crash), and injection-safety (a malicious param binds as a literal, table intact); plus _open_connection's VERA_DB_URL surface (memory + file URLs, in-memory default) and register_db's bind/no-op paths
test_sql_provenance_309.py	79	780	#309 — the SQL literal-provenance gate (SQL injection as a compile-time error): non-literal SQL rejected E207 (bare param slot, function result, \(expr) interpolation, string_concat with a runtime operand, let-bound runtime value, if-expression), literal / concat-of-literals / let-chain-with-shadowing / empty-string accepted, placeholder/param arity E208 with quote- and comment-aware counting (named/numbered placeholders are rejected outright, E209), the count_placeholders↔sqlite3 differential (exact count accepted, one too many rejected), and gate scoping — a user effect DB shadow is rejected at its declaration (E152, #1149) and its runtime SQL still draws E207 alongside it (defence in depth), an unrelated effect's query is not gated, and no E207 cascade onto a mistyped SQL arg
test_checker_modules.py	242	2,632	Module-call diagnostics, cross-module typing, visibility enforcement, builtin redefinition (function E151 and effect E152 surfaced from a module into its importer), reserved function names (E153 — the contract state forms old / new and the keyword class assert/assume/forall/exists/match/if/let/fn/true/false, each top-level, where-helper, and module-surfaced, plus the handle host-invoked carve-out and the probe record behind both halves; the twenty-one contextual keywords then/else/data/type/module/import/public/private/requires/ensures/invariant/decreases/effect/with/in/where/pure/ability/effects/op/result, derived from grammar.lark rather than hand-listed and reachable rather than traps — each declared, was called and answered its value before the fix — over five parametrized batteries (declaration, visibility, where-helper, a rationale free of the keyword branch's false unreachability claim, and a usable per-name fix suggestion) with handle and fifteen keyword-containing names as controls; and resume, reserved on separate grounds — not a keyword, so the declaration parses and outside a handler a bare call reaches it, but it collides with the resumption binding every clause body carries, and the pins cover the rejection, the where-helper depth, that the rationale carries none of the other two branches' false claims, that handler-clause resume(...) still checks AND that a wrongly-typed one is still E202 — the pair, since a binding that accepted anything would satisfy the first alone — and that the rejected declaration draws no second error out of the correct clause bodies it used to shadow, at both top level and where-helper depth), parsed module calls (#420 split)
test_checker_errors.py	73	1,196	Error codes, resolution-coverage diagnostics, contracts, error accumulation (#420 split); cyclic type aliases incl. #1059 self-reference through a type argument (Future<F>, mutual Future<B>/Future<A>, Array<L>) rejected E132
test_checker_builtins_collections.py	97	848	Map / Set / Decimal / Json / Html / Http / Inference built-in type-checking (#420 split)
test_checker_builtins_strings.py	122	945	String / numeric / type-conversion / float-predicate / string-search / markdown / regex built-in type-checking, removed-legacy-name regression (#420 split)
test_obligations.py	775	1,741	Reified proof obligations + warm VerificationSession (#222 Phase A): full-corpus differential oracle (warm session == cold verify() on diagnostics, summary, and obligation stream, plus warm-twice determinism, across all 43 examples and every verify/run-level conformance program), summary↔obligation tier-bookkeeping consistency (including the #967 total == tier1_verified + tier3_runtime leg, plus a focused self-consistency pin on the three call-demotion examples), the #1242 stream partition — over a corpus widened to every conformance program that type-checks, at any level, len(obligations) == total + violated + tier3_unguarded and every status is one of the documented five, with the vocabulary read from the ObligationStatus Literal so a sixth member fails rather than vanishing from the counts — per-kind unit tests (requires / ensures / decreases / nat_sub / call_pre statuses, counterexamples, error codes), content-key stability + same-text-two-sites span disambiguation, session solver reuse, type-error short-circuit, ADT-registry resync between programs; plus the Phase B incremental suite — identical-source full replay, callee-body-edit replays callers while callee-contract-edit invalidates them, span-shift and ADT-edit conservative invalidation, cross-program isolation, timeout-status never cached (monkeypatched solver), FIFO eviction bound; plus the #727 dedup pin — a violating call in a let RHS records exactly one E501 diagnostic and one call_pre obligation; plus the #1208 call-site rendering pin — a PARAMETERISED callee slot substitutes into the E501 message and its fix instead of falling back to the generic wording
test_verifier_contracts.py	96	898	Z3 verification over the example corpus, trivial/ensures/if-else/let/multi-clause contracts, counterexamples, tier classification, arithmetic, verification summaries, Diverge effect, edge cases, string-length + string-predicate verification (#839 split)
test_verifier_nat_obligations.py	82	1,743	@Nat subtraction underflow obligation (#520 — Path-A discharge via requires/path-conditions/path-aware Z3 refutation, pure-literal exclusion, Int-Int and Nat-Int exemptions) and @Nat binding-site narrowing obligation (#552/#747/#749 — Tier-1 value >= 0 at let/call-arg/effect-op-arg/ctor-field/match-bind/destructure narrowing — a concrete site classifies tier3_runtime (codegen-guarded) while the effect-op argument and generic-instantiated constructor field classify E504 (obligated but unguarded, #754/#757) whose rationale names its actual cause — an untranslatable value — rather than the untranslatable-or-timeout conflation #1251 removed, walker-recursion pins, _narrows_into_nat verifier/codegen soundness parity; PR #972 clone-instantiated side-table substitution — a Some(@T) bind in an Option<Nat>-instantiated clone is no narrowing, genuine clone-path narrowings still obligated); #1201 — a builtin Tuple<Nat, Nat> parameter's match-bound components carry their declared component facts (a valid ensures over one proves instead of falsely violating) and an Int component bound as @Nat fires one loud E503 per component, both mutation-caught (#839 split)
test_verifier_primitive_ops.py	39	662	Primitive-operation safety obligations (#680) — division/modulo by-zero E526 and array-index-bounds E527, the in-bounds/out-of-bounds two-check with float-exemption, honest Tier-3 for opaque lengths, off-by-one and lower-bound pins, De Bruijn-correct fix hints (#839 split)
test_verifier_calls_modules.py	81	2,199	Call-site preconditions (incl. branch-aware), pipe-operator verification, cross-module contracts (#839 split); #764 — block translation continues through a let-destructure (E501 fires at/after it, De Bruijn component order pinned with a mutation-caught reversed-order check, ensures over the block result proves Tier 1, the #730 statement-position product case, and the pre-fix before-destructure guard); #1199 — an untranslatable let value binds a span-keyed opaque constant (violating call after it fires E501, assert repairs the proof via #804, two effect-op lets are never provably equal, an ensures depending on the opaque value demotes E522 rather than falsely violating — the taint gate, mutation-caught; a registered user data Tuple routes through the registry constructor path, pinned by an isomorphic-rename differential and an uncached-instantiation demotion check, both mutation-caught); #1236 — a GENERIC callee's call-site precondition demotes loudly (E532 Tier-3) instead of vanishing, in the violating direction with the runtime oracle that makes the old all-Tier-1 verdict a FALSE one, in the satisfied direction (conservative until #732 translates the contract per instantiation), and from the ensures-clause drain as well as the body's, against a non-generic twin that is still discharged statically and a requires(true) generic that stays silent
test_verifier_fresh_scope.py	46	1,106	Fresh-scope obligation walking (#779/#985): primitive ops and binding sites inside closure bodies, quantifier predicates, and handler clauses are obligated Tier-3 under the empty fresh-scope slot environment — with scope-honesty soundness pins for BOTH walkers (a closure param or clause payload never proves against the outer requires; mutation-derived, each killing a full-suite-surviving mutant) — quantifier domains, handler state-inits, and handler bodies walk at enclosing-scope full precision (Tier-1 from requires), manifest violations in closures stay loud (E526/E527/E507/E503), a refined closure narrowing discloses tier3_unguarded + E506, assert/assume conditions are descended by the nat-binding walker, ensures-position quantifier predicates record Tier-3, a nested closure's return widening/narrowing is reported matching codegen's lifted-closure guards, the #1203 boundary obligations fire through a scalar State<T> alias exactly as their codegen guards do (loud E503 init/put through type Count = Nat, Tier-1 from requires — #1205 obligation↔guard parity), and the E533 per-instantiation state-declaration recheck is pinned both ways (a concrete (@Nat = ...) on handle[State<T>] at T=Int is loud with the failing instantiation named; the honest @T control is clean with zero state_decl obligations)
test_verifier_budget.py	36	285	#1350 — the configurable Z3 budget. Resolution order (explicit argument > VERA_Z3_TIMEOUT_MS > 10 s default), malformed values raising rather than silently reverting, the seams that construct a solver honouring it, and the CLI surface (--timeout-ms, the effective budget echoed in verify --json, refusal by name on every command that cannot honour it — including the no-file ones that dispatch early, lsp worst of all — and compile unaffected by a stray env value). The budget's arrival is checked by SPYING on z3.Solver.set rather than by timing anything: explicit argument, environment and default each reach the solver, cold and warm, and a warm session and a cold verify() given the same budget hand the solver the same number — the differential oracle's property at the plumbing level. Deliberately no wall-clock assertions live here; the categorical control that separates "needed more time" from "cannot see through it" is test_examples_ephemeris.py::test_transcendentals_stay_tier_3_at_any_budget, which re-verifies at three budgets instead of measuring elapsed time.
test_verifier_adt_decreases.py	22	822	Match/ADT verification, decreases measures (incl. ADT decreases), mutual recursion (#839 split)
test_mutual_recursive_sorts_881.py	15	317	#881 mutually-recursive data declarations — Z3 sort construction for a mutual group (issue repro, 3-cycle, one-base-case pair, Float64-field pair) declared together via z3.CreateDatatypes rather than recursing unboundedly into fresh sort creation (which otherwise raises a raw RecursionError on a check-green program); plus the Tuple-mediated cases (self-recursion MkC(Tuple<C, Int>) and a well-founded mutual pair through a Tuple field), where a fresh Tuple sort build re-entered the same RecursionError; pins non-FP mutual equality (direct and Tuple-mediated) as Tier-1 and recursive-FP mutual equality as a loud Tier-3 (#871 interaction), with a mutation-kill that re-raises RecursionError when the direct or Tuple-mediated group construction is reverted
test_adt_float64_eq_871.py	9	306	ADT equality over Float64 fields: per-field fpEQ soundness differentials (NaN, signed zero), multi-constructor recognizer guards, recursive-ADT Tier-3 demotion (#871)
test_adt_ord_reject_921.py	40	676	#921 compare/ordering on a user ADT is rejected (E242) rather than returning a silent wrong result — the Ord ability op's bare type variable is now constrained to the §4.5/§9.8.1 orderable primitives (Int/Nat/Float64/Byte/String); covers simple/recursive/enum ADT rejection, constrained-generic accept vs ADT-instantiation reject, the diagnostic naming the offending type, the ensures-position no-traceback pin, primitive compare still checks + runs, structural ADT == untouched, and a Tier-1 verify + false-ensures rejection differential
test_adt_eq_reject_928.py	23	447	#928 ==/!=/eq on a non-Eq-derivable type is rejected (E243) rather than a silent pointer-identity comparison — the equality sibling of #921; covers function-typed ==/!=/eq(), State<Rec>/composite-with-Map-field, direct Map/Array-field ADT reject (upgraded from a late E613); positive controls (Int/String/Bool, Box, List<Int>, Option, Result, nested-generic List<List<Int>>) still check + compile + run to the correct structural-equality result; plus the checker↔codegen Eq-derivability differential (both real predicates over a shared corpus) and codegen ground-truth pins, mutation-validated
test_verifier_refinements.py	92	2,480	Refined Bool/String/Float64 param sorts, refinement-predicate translation + verification (#746 — Tier-1 discharge at narrowing/return positions, E505 with counterexample, E506 Tier-3 for untranslatable predicates, the R3 already-refined exemption, refined-ADT-sub-pattern arm-fact carry into @Nat narrowings and call preconditions, alias-base refined returns, refined returns from match arms) (#839 split); plus the #1214 zero-size-argument differential — mk(()) and mk(1) must record the same refine_bind/violated/E505 obligation and the same summary, a satisfying call-site precondition must discharge under both spellings, and a zero-size formal sitting BEFORE an informative one must not shift which argument the callee's precondition is checked against, an ERASED argument that is itself a call keeps its own nested precondition obligation (the walk happens, only the result is discarded), and Future<Unit> — direct and behind an alias — is masked as the second zero-size type; plus the #1251 disclosure-honesty set — an E506 over an UNMODELLED base names the base rather than blaming Z3's decidable fragment, a modelled base with a deferred predicate still names the predicate (the over-correction guard), and a SYMBOLIC narrowing keeps its obligation, status and code once the concrete gate lands; plus the #1251(b) concrete-decision set — a LITERAL narrowing over an unmodelled base is decided rather than disclosed (@Small = 200 is a rejection naming the value, @Small = 5 a Tier-1 proof, the alias spelling of the cell the same), a predicate the fold cannot settle stays disclosed so the gate is shown to DECIDE rather than widen the base, and ch02_byte_refinement is pinned whole — verdict, counts and per-obligation status in order, since counts alone would net out a rejection here against a new proof there; plus the non-verdict split — check_valid's opaque (#1199) and unknown outcomes get different reasons, driven directly by injecting the outcome since no whole program is known to reach those branches, with two structural pins over vera/verifier.py's AST, both ranging over all three Tier-3 recorders (refinement, nat_bind, nat_to_int_coerce) and checking that roster against the source so a rename cannot make them vacuous: no demotion site fixes a solver reason at the call site instead of deriving it from result.status, and no call that is not literally guarded=True omits the reason its disclosure has to state — closed against the two measured escapes (an f-string parses as JoinedStr, a shared module constant as Name), failing on any reason= shape it cannot classify, and reading the module through inspect.getsourcefile so it is neither cwd-dependent nor able to inspect a different file than the tests import
test_verifier_shadow_audits.py	71	1,395	Per-monomorphization generic verification (#732 — per-instantiation body verification, collapsed-type-var De Bruijn reindex soundness, one-diagnostic dedup, decreases-only discovery, Tier-3 E520 residual) and the #680 shadow/projection audit battery — 57 differential tests pinning the safe→verified / opaque→Tier-3 / unsafe→loud trichotomy across compound shadows, destructure De Bruijn alignment, opaque match scrutinees, and intra-block scoping; mutation-validated (every test flips RED when its target machinery is broken) (#839 split)
test_verifier_mutation_obligations.py	38	888	#387 mutation-hardening: obligation-record completeness and projection-helper pins (#839 split)
test_verifier_mutation_gates_smt.py	52	1,317	#387 mutation-hardening: the verifier's soundness-gate predicates, generic-instantiation aggregation/meet logic, and SMT translation pins (#839 split)
test_soundness_392.py	36	584	#392 audit batches 1–2 — verifier soundness/completeness fixes: signed div/mod truncate toward zero (#799), body assert(P) carries a Tier-1 obligation (#800), divisions in contract predicates carry a div_zero obligation (#801), and the #804 assume-half of #800's assert rule — a prior assert/assume discharges later obligations (including a later call's precondition) + the postcondition at Tier 1, removing false E501/E503/E500/E505
test_int_overflow.py	6	143	#798 — @Int/@Nat arithmetic-overflow obligations (part of the #392 smt.py soundness audit): +/-/* on @Int/@Nat now emit an int_overflow obligation (the analog of nat_sub/div_zero) rather than modelling the operands as Z3's unbounded integers, so a ensures(@Int.result > @Int.0) over @Int.0 + 1 no longer proves a contract the i64/u64 runtime violates under two's-complement wraparound. Unbounded operands leave the obligation undischarged (Tier-3, runtime-guarded); operand bounds that prove the result stays in range discharge it at Tier 1
test_int_overflow_codegen.py	62	718	#798 Stage 3 — runtime overflow-trap codegen: the codegen emits a guard at exactly the @Int/@Nat +/-/* sites the verifier obligates, so vera run/vera compile programs trap on overflow instead of silently wrapping at the i64/u64 boundary. #808 wired the guard to the vera.overflow_trap host import, so the trap now classifies kind="overflow" (carrying the overflow Fix paragraph) rather than the generic unreachable; TestOverflowTrapKind808 pins that, with controls proving the #520 nat_sub underflow and #813 @Nat→@Int widen guards still classify unreachable
test_int_overflow_differential.py	259	398	#798 Stage 3 verifier↔codegen classification differential (cross-component soundness rule): the codegen overflow guard must fire at exactly the sites the verifier obligates and classify each site's operand type (@Int i64 vs @Nat u64) identically — else a Tier-1-clean program traps spuriously or a wrapping op slips through unguarded. Over a corpus exercising all five operand combos plus the literal-left ambiguity (a naive codegen mis-classifies it as @Nat), asserts the verifier's per-site gated classification equals the codegen's site for site, both sides driven by the same ast.span_key
test_nat_int_widening.py	36	602	#813 — @Nat -> @Int widening coercion obligation (dual of #552 nat_bind, part of the #392 soundness audit): a @Nat in (i64.MAX, u64.MAX] reinterprets when widened (u64.MAX → -1), so a nat_to_int_coerce obligation that the value is <= i64.MAX now fires at the return position — provably-in-range → Tier-1, provably-out-of-range (@Nat.0 >= 2**63) → loud E530, unbounded → honest Tier-3 (runtime-guarded), with an @Int -> @Int control that must not fire; the unguarded generic-@Int-field case also has its E531 rationale read for WHAT IT SAYS — a value bounded on neither side, not the untranslatable-or-timeout conflation #1251 removed. The #813 follow-up adds the explicit nat_to_int built-in and heterogeneous if/match arms with a non-negative-literal alternative; #820 adds the heterogeneous-@Int-slot arm, closure argument, and closure return/capture obligations (each per-arm / per-site, with @Int-arm and @Nat-formal controls that must not fire)
test_int_widening_codegen.py	52	535	#813 Stage 3 — runtime @Nat -> @Int widening-trap codegen: the codegen emits a guard at exactly the @Nat -> @Int coercion sites the verifier obligates (return, let, call argument, and — since #820 — array element, tuple construction/destructure, heterogeneous if/match arm, closure argument/return), so vera run/vera compile programs trap when a @Nat above i64.MAX would reinterpret to a negative @Int instead of silently returning the wrong value. The trap is a bare unreachable (shares _emit_negative_i64_guard with the #552 nat-bind guard), classified kind="unreachable" today (a dedicated widening trap kind is a follow-up)
test_int_widening_differential.py	26	320	#813 verifier↔codegen behavioural differential (cross-component soundness rule): at every @Nat -> @Int coercion site the verifier's nat_to_int_coerce classification must AGREE with the runtime — a tier3 (codegen-guarded) site MUST trap on a @Nat above i64.MAX (return / let / call-arg / constructor field / ADT sub-pattern / match-bind, and the #820 array-element / tuple-component / heterogeneous-arm / closure argument-return sites), while a tier3_unguarded (E531) site must NOT trap (the generic-instantiated @Int-field coercion codegen cannot guard). Runs BOTH sides on one corpus so the "runtime-guarded" claim is checked against the actual trap — catching a verifier deferral codegen never guards (unsound silent -1) or a spurious trap
test_nat_narrowing_return_differential.py	136	2,897	#758 verifier↔codegen behavioural differential (cross-component soundness rule): at the function-return @Int -> @Nat coercion slot the verifier's nat_bind verdict must AGREE with the runtime — an unproven narrowing leaves the return obligation undischarged (loud E503, or an honest tier3 for an opaque value) and codegen's return guard TRAPS on a negative input, while a proven narrowing (requires / path condition) discharges at Tier 1 and the guard is dead (vera run returns the value, no trap). Runs BOTH sides on one corpus so "the verifier obligates this return" is checked against the actual guard — the return-position dual of test_int_widening_differential. #983 review adds the tier3 quadrant (opaque float_to_int, verify + compile in one run), let_before_tail / nested_if_join join shapes, a type Count = Nat alias case, and threads file= + resolved_modules= through the verify side for CLI-pipeline fidelity. #1017 adds the apply_fn ARGUMENT-narrowing quadrant (the @Int -> @Nat dual of the #820 argument widening): a provably-negative arg is E503, a runtime arg is obligated + call_indirect-guarded (run traps), a requires-bounded arg proves Tier 1, a @Nat -> @Nat arg is unobligated, and an opaque float_to_int arg records tier3 with the codegen i64.lt_s/unreachable guard emitted (verify + compile cross-checked in one pipeline run). #1024 adds the REFINED apply_fn-argument quadrant (refine_bind, the refinement dual of #1017): an argument narrowing into a {@Nat | @Nat.0 > 0} closure formal discharges the FULL predicate refined-first — a constant 0 is E505 (clears the @Nat base's >= 0 but violates > 0), a runtime arg is obligated + guarded at the lifted closure's prologue (run(0) traps with a contract_violation Refinement-violation message), a constant 5 / requires-bounded arg proves Tier 1, and a @Pos -> @Pos arg is unobligated. #1032 adds the REFINED closure-RETURN quadrant (the return-side dual of #1024): fn(@Int -> @Pos) { @Int.0 } records exactly one tier3 refine_bind (opaque body — never a false Tier 1), run(-5) AND run(0) trap at the lifted body's return guard with the "return value" refinement message, a satisfying value passes, and the always-satisfying body stays an honest tier3 with no spurious trap — plus the re-derived single-guard pin (exactly one contract_fail refinement check in the lifted body, zero i64.lt_s narrowing checks). PR #1202 adds the #1203 handler-boundary quadrants (init/put/with/resume × trap/pass/zero, bare-put and clause-body-put dispatch shapes, widen duals at U64_MAX with i64.MAX boundary controls) and the #1205 scalar-alias family quadrants: alias and refined-alias State<T> cells compile and run, every #1203 guard keys through the alias (init/put trap on negatives, widen dual at U64_MAX), the alias-equal annotation binds clause slots under its SOURCE name, a stateless handler's clause @T.0 reaches the op ARGUMENT (the pre-fix capture skew read the cell — pinned in both directions), Exn<Code> compiles with the payload bound under the clause pattern's name, old(State<Count>) snapshots through the collapsed family, and the retired lying-annotation fixture is pinned as check-rejected E336. The second adversarial round adds the clause-scope checker-parity battery (mixed-spelling State and Exn shapes bind under the checker's canonicalized argument names, both patternless twins bind nothing, the declaration-scope shadow probe), the parameterised-alias family differentials (State<Id<Nat>>, alias-of-generic-alias, Exn<Id<Int>>), and the State<Byte> write-boundary battery (init/clause-put/bare-put/with/resume literals at i32)
test_nat_bind_construction_soundness_1332.py	42	713	#1332 — a @Nat tuple component narrowed at CONSTRUCTION is obligated, never assumed (part of the #392 false-Tier-1 audit; the construction-position counterpart to test_nat_narrowing_return_differential.py's return-position half). let @Tuple<Nat, Int> = Tuple(@Int.0, N) destructured by an irrefutable single-arm match verified as proved while vera run trapped on a negative: _translate_match asserted the arm's @Nat sub-pattern source fact UNCONDITIONALLY at the solver's base level, where the datatype accessor axiom reduced it to the construction obligation's own goal — the obligation discharged itself. The anti-circularity test existed but was SYNTACTIC (is the scrutinee AST a ConstructorCall?) where a let-bound tuple arrives as a slot reference whose TERM is one. Every cell pins the verdict against a control that must not move, because a verdict alone cannot separate the repair from over-rejection: the precondition-discharged form still proves and still runs, the return-position form is unchanged in both directions, and the two construction spellings — with and without the destructure — must agree with each other, which is the internal inconsistency the bug consisted of. The soundness differential asserts the verdict and the run in ONE test (verify-clean beside a trapping run IS the bug, so siblings would each pass alone), with its requires(@Int.0 >= 0) parametrisation verify-clean so the implication is exercised with a true antecedent. The REFINED sibling is here too, repaired by the same change and worse in kind — a refined tuple component carries no runtime guard, so pre-fix it returned -7 for a PosInt from a verify-clean build rather than trapping. Two over-rejection controls straddle the guard: one where it FIRES (a tuple built from an already-@Nat parameter, whose postcondition still proves from the parameter's own declaration) and one where it does NOT (an opaque @Tuple<Nat, Int> parameter, whose declared source facts must survive). The suite is then parametrised over how the scrutinee is PRODUCED, because a guard asking "is this term literally C(args)" is defeated by anything that wraps the construction — an if producing the tuple laundered past the first version, verifying both narrowings while the program trapped, and a match-produced spelling did the same. Bare constructor, if with both arms constructed, if with one constructed and one call-produced, match-produced and let-of-let are each required to keep the narrowing obligated, in the @Nat and refined families alike, beside call-produced and opaque-parameter controls that must keep their facts — the boundary being PROVENANCE: a call- or parameter-produced value's component facts were established in the callee's context, a locally constructed one's are still outstanding
test_nested_ctor_sort_1360.py	30	680	#1360 — a Tuple nested inside a constructor translates, and verify --json always envelopes. let @Option<Tuple<Nat, Int>> = Some(Tuple(@Nat.0, 1234)); was check-green and killed vera verify with a raw z3.z3types.Z3Exception: Sort mismatch, emitting NO --json envelope at all. Two sorts derived by different routes disagreed: a nested Tuple argument is built by the variadic-tuple branch keyed on the arguments' Z3 sorts (Nat reads back as Int, so always the Int spelling), while the enclosing ctor's sort comes from _resolve_pinned_sort, which prefers a cached instantiation equal to the pin MODULO Nat/Int — sound at a scalar position where both spell one IntSort, unsound at a datatype position where #884 made the two injective sorts. The Nat appears even in an all-Int program because a positive literal types as Nat on the declared side, which is why the trigger is the NESTING and not Nat; same-ADT nesting (Some(Some(...))) is carried as a control, measured passing before the fix, so the repair is pinned to the disagreeing sorts rather than to nesting in general. The envelope half is asserted INDEPENDENTLY of that crash — a translation function is monkeypatched to raise and the cell asserts stdout is a parseable E699 envelope rather than empty, so the machine-readable contract holds for the next translator bug too — and the pair mutation-validates apart: reverting the sort fix reddens the four translation cells while the controls stay green, breaking the backstop reddens exactly the two envelope cells. A fourth group covers the guard PREDICATE itself: _ctor_accepts exists to intercept Z3's raise-instead-of-error behaviour, so a predicate that can itself raise defeats its own purpose — hostile stand-ins whose arity(), domain() and sort() raise must be ANSWERED False (the conservative "does not accept", which routes to the decline path) rather than propagate, beside a discrimination cell over real Z3 terms so the group cannot be satisfied by a predicate that swallowed its body and declined everything
test_hetero_widen_tailcall.py	21	312	The heterogeneous per-arm widen guard vs tail calls (#986) and targets: an arm whose @Nat value is a tail call must lower to a plain call so the appended guard stays live (return_call would skip it — the widening dual of the #983 per-leaf narrowing), the genuine @Int arm's recursive return_call keeps TCO (100k-depth run), the gate is target-aware (_is_hetero_int_widen_join: a hetero join in a @Nat-returning context must NOT widen-guard its legal @Nat arm — the target-blind gate false-trapped $2^{63}$), and a user data Tuple must not take the builtin variadic carrier's target-table path (verifier emits no obligation there; guarding it was an opposite-direction desync)
test_xmod_span_collision.py	4	156	#987 — the span-keyed target-type table is single-module (keyed by bare span, no file identity): an imported body's expression span can coincide with a main-file entry. #987 threads each module's OWN table into codegen (CheckArtifacts.module_artifacts → _compile_fn(module_tables=...)), so the engineered line-for-line collision pair now proves the legal all-@Nat imported function is not falsely widen-guarded by CORRECTNESS (its own table targets Tuple<Nat, Nat>), not merely suppression — with a thread_modules=False control pinning the #986 suppression fallback still holds when no module tables are threaded, and a same-file control proving top-level guards unaffected
test_xmod_widening_differential.py	18	293	#987 verifier↔codegen widening differential run THROUGH THE IMPORT DOOR (the same-file test_int_widening_differential was green while this door was open): for each cross-module shape (array-element, tuple-construction, tuple-destructure control, transitive 3-level, and shadowed-import) the library's standalone verify must classify the @Nat -> @Int coercion Tier-3, AND the importing program compiled the way vera run/vera compile compile it (per-module tables threaded) must TRAP at u64.MAX — never the silent -1 — while passing 2^63-1 and 42 unchanged. Pins that the #820 array/tuple-construction guards, recovered from the span-keyed target table, now fire for imported bodies. Also pins the import-door trap is the guard's bare unreachable net (not some other trap), and a two-independent-libraries-both-widen scenario asserting BOTH imported bodies trap at u64.MAX (kills a first-module-only partial-collection mutant)
test_xmod_artifact_collection.py	5	205	The per-module CheckArtifacts.module_artifacts pass is OPT-IN (collect_module_artifacts=, default off) because only the codegen-bound callers consume it and it is O(N²) sub-checks in the module count. Pins that typecheck_with_artifacts WITHOUT the flag leaves module_artifacts empty (the vera verify / warm-session path pays nothing) and WITH it collects each resolved module's own table; plus the GAP-1 artifact-level pin — in a transitive fixture (main -> alib -> blib) the middle module alib's target table has 2 entries only because its direct flags are re-derived from its OWN imports (a first-module-only / top-level-flags mutant drops it to 1)
test_xmod_generic_widen_gap.py	15	413	#998 guarded differential: an imported generic function's mono clones carry their origin module and compile against ITS span tables, so the #820 widen guards fire at every instantiation through the import door. For the array-element and tuple-construction sites × T=Bool/T=Int instantiations, the standalone library verify must promise Tier-3 AND the importer must trap with the guard's bare unreachable at u64.MAX (never the silent -1) while in-range values round-trip — through both the bare-call and shadowed (lib::wrap → mod$…) doors, plus a hoisted-where-helper-widen scenario (the per-clone hoisted copy inherits the clone's origin) and a local-generic control (local clones keep the main-file tables)
test_xmod_ability_ops_992.py	5	156	#992 imported-body ability-op rewrite: eq in an imported top-level fn, its where-helper, and a nested grandchild; compare (the other AST-rewritten ability op); and the shadowed (mod$…, Pass 2.6) door — each runs end-to-end through the import door (a raw call would drop the body and dangle the importer's call)
test_xmod_where_helper_import_991.py	3	190	A non-generic where-helper's name (#991) no longer suppresses a same-named IMPORT's bare emission — the shadow set is collected from the POST-hoist program, so the import wins outside the parent (spec §5 helper locality) while the parent's body call reaches its own hoisted helper (go(0) == 701, both doors observed; a stale bare-name shadow would dangle unknown func or silently capture the import-bound call). Controls: a TOP-LEVEL local sharing an import's name still shadows it (§8.5.2), and an UNINSTANTIATED T-unused generic helper's name still shadows (its template still emits bare; dropping it would duplicate the import's bare emission)
test_generic_where_helper_990.py	10	339	#990 nested-generic monomorphization: a forall<T> where-helper under a NON-generic parent is a mono base — the issue repro (direct instantiation), the grandchild variant (all-non-generic ancestor chain), two instantiations (T=Int + T=Bool) both emitted, and WAT-level single-emission pins (exactly one gid$Int clone, no bare @T template); plus the #904 control (helper under a GENERIC parent stays hoisted per-clone, no standalone duplicate) and the own-where-child shape (the generic's T-dependent and T-independent children are hoisted per-clone only — the Pass-2 where-fn sweep stops at the generic template)
test_codegen_where_helper_mangling_991.py	13	553	#991 non-generic where-helper name collisions: parent-qualified mangling (compute$where$branchA$where$leaf) so two siblings' same-named nested helpers, and a helper named like a top-level function, compile and run each their OWN body (RUN-value assertions — sibling leafs summing to a value only distinct bodies yield, nested-helper vs top-level both reachable) instead of crashing WAT assembly with duplicate func identifier; plus WAT name-scheme pins (top-level names stay bare, nested helpers mangled), full lexical resolution (a grandchild calling an ancestor-scope "aunt", and an inner helper shadowing an outer same-named one), a collision coexisting with a nested generic (gid$Int still emitted), the generic-subtree capture battery — a generic helper's call to its OWN nested shared must not be captured onto an ancestor's hoisted name (silent-wrong-value shape, the false-Tier-1 verify+run differential, the unshadowed-ancestor-call no-regression guard, and a generic child's name shadowing an ancestor's) — and the CHECKER leg: a differing-signature diamond (@Int -> @Int vs @Int -> @String leaves) that the flat last-wins lookup falsely E121'd must check clean AND run to the three-subsystem-agreement value
test_monomorphize_differential.py	62	2,191	#732 differential soundness: the verifier's per-monomorphization instantiation discovery covers every instantiation codegen emits (name coverage + per-generic count), over real generic programs (conformance ch02/ch09, examples/generics.vera) plus inline cases for the soundness-critical scenarios — collapsed type vars, prelude combinator emission (option_map), transitive generics, a generic whose type arg is fixed only by a where-helper's return (a Float64-returning helper, so the unresolved-var "Bool" phantom default cannot mask a miss), a generic whose type arg is fixed only by an imported constructor (id2(MkBox(7)) — the verifier's mono-context must include _module_constructors, else it phantom-defaults and misses codegen's id2<Box>), a generic whose type arg is fixed only by an imported function's return (id_g(make_int(...)) — the verifier's mono-context must seed fn_ret_types from imported functions, else it phantom-defaults and misses codegen's id_g<Int>, plus a private-shadow case pinning the imported-fn seeding stays unfiltered like codegen since filtering would diverge into a false Tier-1), and a generic reached only through a contract clause or where helper (codegen must seed Pass 1.5 from the shared node-level walk, not just decl.body, or it skips the clone → CodegenSkip at run time) — so a missed instantiation (a false Tier-1) is caught. Guards against a vacuous pass when codegen emits nothing, plus a determinism guard (vera compile --wat is byte-stable across PYTHONHASHSEED — the mono worklist sorts its instantiation sets); plus the #899 call-rewrite↔emitted-clone differential (test_call_rewrite_matches_emitted_clones) — the THIRD consultor the verifier⊇codegen check never exercised: captures every mangled target the WASM call-rewriter (_resolve_generic_call) resolves and asserts each is an actually-emitted clone, over user-fn-return-into-generic-arg shapes (a non-generic user fn returning Option<Decimal>/Result<Decimal, String> in Option<T>/Result<T, _> position; a scalar-resolving alias type Age = Int and a named refinement in bare @T position; and a non-generic user fn returning a LITERAL parameterized type Option<…>/Result<…>/Box<…> bound to a bare @T, where discovery keys the clone by base name pick_last$Option — the base-name key is sound because a bare-@T body is representation-polymorphic) — a dangling target is the check-green-then-run-drops-main desync. All three consultors (discovery, verifier, call-rewrite) route the user-fn-return clone key through ONE shared declared_return_clone_key, so they cannot desync by construction. The #898 cross-argument merge (eq2(MkErr(5), MkOk("x")) — one argument fixes each of a sparse Res<A, B>'s two parameters) is in BOTH corpora: a symmetric collapse of the merge trips the inline differential's vacuous-emission guard (codegen emits nothing once the type under-determines), and an asymmetric one-sided merge surfaces in the call-rewrite differential as a dangling bare eq2$Res clone. The #1274 per-module half lives here too: every QUALIFIED-ONLY module generic (private, out-of-filter, or locally shadowed) must be emitted AND discovered under the same mod$<path>$name base, with the complement pinned beside it — a public in-filter unshadowed generic must keep the bare name, or #774's bare-call routing would break in silence
test_codegen_expressions.py	89	787	Int/Bool/Float64 literals, slot refs, arithmetic, comparison, boolean logic, unary ops, if/let, function calls, recursion, pipe operator, CompileResult surface (#419 split)
test_codegen_calls.py	32	1,402	Statement-position unit calls (#556), WASM tail-call optimization (#517 — return_call emission, 50K- and 1M-iteration stress, structural return_call/plain-call boundary assertions, GC-aware TCO for allocating fns (#549 — $gc_sp restore before each return_call), postcondition-fallback regression, analyzer unit tests over tail-transparent constructs), pair-typed closure params + captures (#535) (#419 split)
test_codegen_infrastructure.py	24	455	Module assembly import/memory conditionals, execute error paths, unsupported-construct skips + node-level E602 reasons (#626), built-in shadowing (#154), typed holes, example round-trips (#419 split)
test_codegen_interpolation.py	35	1,321	String interpolation, the E615 loud inference-fallthrough channel (#630) (#419 split)
test_codegen_effects.py	117	2,665	State<T> host imports, effect handlers, Exn<E> handlers (incl. expression-bodied, #475), Async/Future<T>, Random effect (#419 split); plus the #841 concurrent-Async battery (TestConcurrentAsync841) — fused async_http_get/async_http_post/async_await import pins, sync-import suppression, pure-shape eager pin (no task imports), kind-4 register_wrapper structural pin, a generic-fn-with-concrete-Future-return await classification pin, the behavioural two-gets-overlap test (local ThreadingHTTPServer, server-side request-log ordering, no wall-clock), and the #843 indirect-closure Ok-path pin (payload byte-exact through await(apply_fn(...))); plus the #1109 alias-Future battery (TestConcurrentAsyncAlias1109) — alias-typed let, alias-declared fn return, two-hop alias chain, and payload-alias (Future<R>) shapes classify for the fused-handle check (import pins + byte-exact Ok payloads), plus the aliased two-gets-overlap behavioural pin
test_state_clause_semantics.py	27	696	#976 intrinsic-hybrid State clause semantics: clause bodies execute (get-transform 105/30), with overrides the intrinsic store (10), the pre-store capture makes with @T = @T.0 keep-old (7 — the corpus-migration canary); composite (heap) state transform + a captured-pointer-read-after-alloc shape; non-tail resume skips loudly; canonical clauses pinned as exact identity (99, and the spec §7.5.3 counter anchor 10); #1006 effect ops as array-literal elements (identity + transforming get clause, and the declared-effects(<State<Int>>) helper covering the second op-injection site)
test_codegen_data_types.py	93	1,864	ADT metadata + constructors, match expressions (incl. nested patterns), tuples (incl. the #902 zero-size Unit component in a by-value Tuple / user-ADT layout — construct, match-extract, multi-Unit, Unit in any position, and a side-effecting Unit-returning call field Tuple(IO.print(...), n) all compile + run; the #1031 transparent Future<Unit> component erasing like bare Unit through both let-destructure and match, incl. an alias to the compound and an alias-of-alias chain; and the #1037 alias to a representable compound type FI = Future<Int> binding a real local through destructure, match, an alias chain, and a standalone let), ADT string fields, generic-monomorphization regressions (#604, #767) (#419 split)
test_codegen_structural_eq.py	58	1371	Structural Eq auto-derivation (#773): String-field ADTs compared by content (distinct string_concat allocations), nested-ADT fields compared by value not pointer, 2-level recursion, a recursive generic ADT (List<Int> — the self-calling $eq_ function + deep List<T> param substitution), a mutually-recursive ADT pair, P<String> wrapping Box<T>, Box<String> under an Eq-constrained generic, type-alias fields (alias-to-Int/String/ADT/refinement + 2-hop chains resolve before Eq dispatch), NaN-field runtime consistency with primitive ==, Byte fields, loud E613 for Map/Array/Set-field ADTs on the generic path AND for direct == (Map-field, Md-builtin, ctor-inferred bare generic, and the always-true Tuple placeholder), the checker↔codegen derivability differential, the #772 constructor-path lockstep probe, and the #898 sparse-multi-type-parameter probe (a fully-determined Res<Int, Int> derives + compares by value on the ctor path; the under-determined id1(MkErr(5)) — A free — reports the clearer E619 not the misleading E613; the determined-but-non-Eq Res<Array, Int> soundness gate stays E613; the cross-argument merge eq2(MkErr(5), MkOk("x")) compiles + runs the Res<String, Int> clone; a determined-non-Eq cross-arg type is E613; the E619-accuracy split — a recovered non-Eq component Res<A, Array<Int>> or a structural non-Eq field W<A,B>{K(Array<A>,B)} is E613, an all-known-Eq free-param case stays E619); and the #923 nested-generic direct-== probe (a List<List<Int>> / 3-level List<List<List<Int>>> / Chain<Pair<Int>> operand inferred from constructor calls derives + compares by value where a one-level type-arg recovery would spuriously E613; the eq(...) builtin form matches; a non-Eq nested component List<List<Array<Int>>> stays E613); and the #932 generic-call sibling (the same List<List<Int>> / 3-level / Chain<Pair<Int>> nesting reached THROUGH an Eq-constrained generic call eq2(@T, @T -> @Bool) derives + runs where a one-level clone-path recovery would spuriously E613; a non-Eq nested leaf stays E613 — the fix recurses the derivability-name recovery without changing the mangled clone name)
test_codegen_zero_size_fields_1043.py	22	463	Registered constructor layouts erase zero-size fields (#1043): the layout differential — registered field_offsets/field_types for a bare Unit, Future<Unit>, or alias/alias-chain field (erased first, last, and multi-erased) match construction's "unit" (size 0 / align 1) convention — plus every consumer end-to-end: a wildcard-over-erased nested match extracts the real value (not zeroed fresh-alloc memory), structural Eq over an erased field first / multi (equal compares equal, distinct stays false), show renders the field as unit, hash is payload-sensitive (not garbage), no-erased-field controls stay green, and the builtin variadic Tuple wildcard-over-erased still LOUD-skips (E602, not silent); a dedicated Future<Unit> end-to-end block (construct via async(()) + wildcard-match + Eq + show, exact values) pins that async(()) construction is not blocked by any skip; mutation-validated (each edit site reverted independently flips its consumer's tests RED)
test_codegen_orphan_call_indirect_1185.py	9	433	No call_indirect reaches the output without a table to dispatch on (#1185), the unclosed half of the #1100 class: an [E602] skip swallowing a module's ONLY closure rolled the lift back, suppressing the (table)/(elem) sections while every surviving carrier kept its indirect call — an uninstantiable module emitted with zero error diagnostics, raw unknown table 0 on the first call to ANY export. Both carrier shapes are pinned (the apply_fn special form on a closure-typed parameter, and a monomorphized clone of prelude option_map — the clone's drop attributed to <prelude>, not to whatever the user's file holds at that line), plus the no-closure-anywhere shape that previously produced NO diagnostic at all; each asserts the [E620] chain names the [E602] root with its location and that the unrelated victim export RUNS (41). Over-correction controls, green before and after: a surviving closure keeps the table so the apply_fn carrier is NOT dropped and still computes (107), the array_map/array_fold emission site likewise (63), and a closure-free program has neither. Mutation-validated — neutering the carrier seeding flips exactly the three orphan tests RED with the controls green, and un-hardening #1100's acceptance helper on the same broken module makes it pass again. The exception-path lift skip (a raise ESCAPING _lift_pending_closures, unreachable from a check-green program today) is pinned by a stubbed-lift regression asserting the carrier's [E620] names the root rather than claiming the program creates no closure
test_codegen_skip_propagation_1100.py	8	325	A codegen skip propagates to (transitive) callers before module assembly (#1100): the repro (helper skipped, main calls it — clean [E620] warning naming caller + root, no raw wasmtime unknown func text, module still assembles), depth-2 transitive drops in BOTH declaration-order permutations (caller-first needs a second fixed-point round, so a single-sweep propagation goes RED), root-cause naming with the skip's line embedded and the E620 located at the caller's declaration, an untouched public sibling that keeps its export and RUNS (41 — no fallback coincides), mutual-recursion termination (ping/pong cycle + skipped callee drops all three callers, sibling still runs), the closure shape (the dangling call lives in the lifted closure's WAT; the parent drops via the construction edge and the stub keeps table indices valid), and a no-callers control (root E602 only, no E620, everything else untouched); mutations — single sweep, dropped closure edge, dropped stubbing, hop-instead-of-root threading — each killed by a named test
test_dropped_entry_1183_1186.py	21	561	A dropped entry function is refused, never silently replaced (#1183), and an imported body's skip locates in its own module (#1186). #1183: the repro — declared main dropped, one public sibling surviving — exits nonzero with main and the root [E602]/[E620] named, and the sibling's 4243 sentinel (a value no fallback, default, or error path produces) never appears on stdout; the same for an explicit --fn, for the --json envelope (ok: false), and at the execute() library boundary; CompileResult.dropped_fns is pinned as the reified source of the refusal; the Compilation notes: block appears when a sibling survives (the ungating); auto-selection survives for the never-declared case and prints a one-line stderr note naming its choice; zero-export compile exits nonzero in both text and JSON; and the browser bundle refuses a dropped main using the SURVIVING-sibling fixture, so a non-empty export list rules out the zero-export check as the cause. #1186: the root E602 carries the MODULE's path with module-local line/column and quotes the module's source line, the [E620] cross-file prefix fires with its exact wording derived from the root's own location, a same-file control keeps the bare at line N, column M form, and vera test names the [E602] root instead of calling a public-but-dropped function private. Mutations — api.py refusal, CLI refusal, the E620 drop record, the module source scope, the tester reason, the notes ungating, the auto-select note, the zero-export gate, the browser refusal — each killed by a named test
test_imported_trap_source_map_1189.py	8	342	An imported function's runtime trap frame names ITS module's file (#1189), the source-map sibling of #1186's diagnostic fix. Fixtures split the basenames (chinchilla.vera module, stargazer.vera importer) so a frame's attribution is decidable from the string alone, and every trap is a precondition violation so WasmTrapError.kind is pinned. Covers the three doors: an imported non-generic fn (pre-fix <unknown> — never registered on the main generator), a monomorphized clone of an imported generic (pre-fix the IMPORTER's path with the module's line range, which in the fixture names a real-but-unrelated importer function), and the mod$… emission of a locally-shadowed import (whose rightmost-$ strip yields nobody's entry). Asserted at the cmd_run text backtrace (per-frame line, never the whole stderr blob — main legitimately names the importer), the --json frames array, fn_source_map itself, and execute()'s WasmTrapError.frames. Over-correction control: a wholly main-file trap keeps the main file, green before and after. Mutations — the module file on the Pass-0.5 registrar, the bare-name harvest, the mangled-name mirror, the Pass-1.5 module source scope — each killed by a distinct named test
test_codegen_typeparam_unit_wildcard_1060.py	31	959	Wildcard over a type-parameter field instantiated to Unit (#1060), the type-parameter sibling of #1043's declared-Unit field: a WILDCARD over Box<T> field T used to advance the match offset walk by the generic i32 width, so on Box<Unit> (field erased to 0 bytes) every later field read four bytes high — silently check-green. Bug-manifesting shapes go end-to-end (Box<Unit> trailing-Int, Named<Unit> String read-back, Entry<Unit> nested-ctor tag, Bool-following, second-type-parameter, and a nested-generic Outer<Unit> wrapping Inner<Unit> that exercises the deeper-recursion type substitution); controls stay green (before-erased field, trailing wildcards, Option/Result<Unit> builtins, Box<String>/Box<Int>/Tagged<Unit> alignment-coincidence, structural Eq/show recompute path); the direct-call boundary is pinned (#1065) — a match mk() { … } scrutinee recovers its concrete instantiation from the callee's declared return type, so a wildcard followed by a read now compiles and reads the real value (Box<Unit> trailing-Int, Entry<Unit> nested-ctor, Named<Unit> String read-back) instead of the sound #1060 interim LOUD-skip, while a trailing direct-call wildcard still compiles; the generic-call sibling (#1072) resolves the declared return's type variables from the call site (P2<T, Unit> at T=Int, the var-typed field at String i32_pair width, a fully concrete parameterized return on a generic fn, nested-ctor and String-read-back variants, plus a trailing-wildcard control), and the module-call door (#1073) routes boxlib::mk() — and the imported-generic #1072 x #1073 compound — through the shared resolver into the same recovery; mutation-validated per arm (reverting the #1060 instantiation-awareness flips exactly the #1060 bug-manifesting shapes RED with declared-Unit #1043 tests green; reverting the #1065 declared-return threading flips exactly the three direct-call value shapes RED; neutralizing the #1072 generic arm flips exactly the five generic value shapes + the imported-generic compound RED; neutralizing the #1073 module arm flips exactly the two module tests RED)
test_codegen_alias_adt_name_width_1309.py	112	423	A type alias whose name is also a registered ADT's must emit the ALIAS TARGET's width (#1309). Codegen's _type_expr_to_wasm_type tested _adt_layouts — and Array/Map/Set/Decimal, none of them primitives — before the alias table, where the checker's _resolve_named resolves primitive, then alias, then declared ADT; so type Option = Int; emitted the ADT's i32 pointer for an i64 slot on a check-green, verify-green program. Three dispositions are pinned separately because they fail differently: LOUD scalar targets (Int/Nat i64, Float64 f64) died at load; PAIR targets are the SILENT ones the issue's "matching widths" prediction missed — an i32_pair is two words and the single i32 dropped the length, so string_concat("ab", "ab") returned junk bytes and array_length over three elements returned 0, both at exit 0; and matching-width targets (Bool/Byte/Map/Set/Decimal, all i32) are INERT, kept as green-both-sides guards that the reorder leaves them alone. The battery is the differential that makes width-luck unreintroducible: every name in the LIVE built-in ADT registry (read off a real CodeGenerator, so a new built-in joins without anyone widening a list) crossed with every representation class, comparing the emitted twice body in full — header widths and the instructions under them — against the identical program under a fresh alias name, plus the two unit duals — under an alias the derivation answers the target's width, without one it still answers the ADT pointer, so "the alias wins" cannot be satisfied by breaking every ordinary ADT parameter. Primitives are asserted to still shadow a same-named alias — the one branch that must NOT move — across all seven spellings by asking the derivation directly, which is the only way to reach every one of them since two are checker-refused (@Bool.0 + @Bool.0 is E140, type Int = Int; is E132); a run-level program carries the behavioural half, because type Bool = Int; used AS a Bool is check-green, runs, and distinguishes the hoist mutant. An earlier draft claimed the checker refuses every program that would exercise this, which is measured false. A separate block covers the THIRD consumer of the same disease (CR on PR #1323): _return_type_is_string tested the Future<T> transparency strip before the alias table, so under type Future<T> = Array<T>; a @Future<String> return was classified a string and execute() decoded the array's backing bytes as UTF-8 — two NULs where the fresh-name control printed the pointer, measured identically at the branch point and so pre-existing. String stays ahead of the alias branch there too, being the one primitive involved, and three over-correction controls hold the #841/#1047 transparent-Future decode and PR #1041's alias-to-Future shape. Json and HtmlNode are deliberately outside the prelude-ADT row: their prelude combinator bodies render against the flat alias map a main-file shadow pollutes, which is an alias-env SCOPING defect (#1316) the reorder does not reach — though it does MOVE that failure (17 prelude json_* signatures flip width, the loader's complaint reverses direction, html_attr loses a push), so "fails identically" — an earlier draft's wording — is measured false
test_codegen_pair_scrutinee_1305.py	32	685	A match whose SCRUTINEE is pair-represented (String / Array<T>) took one local at the internal i32_pair pseudo-type, so the module carried (local $l1 i32_pair) and never assembled (#1305). The issue reached it through json_keys and framed it as an Option<Array<String>> payload binder; the docstring records why measurement does not support that — json_keys returns Array<String>, and array_length(json_keys(j)) compiled and ran at the branch point — so the tests are built on the shapes that actually trigger it: match @String.0 { @String -> … } and match @Array<Int>.0 { @Array<Int> -> … }, both legal and check-green, plus the slot, call-result and builtin-result scrutinee forms. One test returns the BOUND STRING rather than its length, because a fix that allocated two locals and copied only the pointer passes every length-free assertion. The issue's own repro matches Some/None against that array; a pair carries no tag, so the assertion is that the module assembles and the refusal is a located E602 — not that the nonsense compiles (the checker accepting it is #1315). The guard is a WHITELIST (wildcard and binding only) and these cells are why: as a blacklist naming the two constructor kinds it let true -> and 1 -> fall through into the arm-condition emitter, turning a loud WAT failure into a check-green program that exits 0 printing 100 from the scrutinee's heap POINTER read as a truth value, and its integer twin into a shipped .wasm that died at instantiation with no diagnostic — so five unlowerable-arm cells (bool/int/string literals over both pair spellings) and a nullary-arm-FIRST program pin each half, the last because both original repros led with Some and left the nullary half droppable green. The two shadow pushes are pinned as EMISSION by a WAT differential against the match-free twin (exactly two more push idioms) plus a position assertion that no length half is rooted: deleting both pushes leaves the whole suite, the GC rooting and reclamation suites, and four allocate-in-the-arm probes under VERA_EAGER_GC=1 green, so a behavioural claim would be one no probe supports. The two controls the issue listed as already-compiling are kept as regression guards, and an Option/Result binder battery over Array<String>/Array<Int>/Array<Json>/Map/Set/String/Int payloads plus a nested Option<Option<Array<String>>> pins the boundary: the scrutinee change left pair-typed constructor FIELDS alone
test_codegen_erased_alias_typeargs_1070.py	15	398	Non-literal erases-to-Unit type ARGUMENTS (#1070): Box<U> (type U = Unit;), Box<Future<Unit>>, Box<FU>, and alias chains — the #1060 width recomputation's zero-size test was the literal name Unit, so these spellings got 4 bytes and every later field read a shifted offset (silent 22→0, nested 314→0); the same literal-test disease made structural Eq over the same spellings fall back to the scalar POINTER compare (pre-existing — equal structs compared unequal, silently) and show/hash loud-skip. Pins every spelling end-to-end: wildcard reads (trailing Int, nested ctor), Eq equal/distinct + Future<Unit> arg, show renders unit + the real fields, hash payload-sensitive + deterministic, literal-Unit controls; the rider — a zero-size @Unit BINDING after an unrecoverable wildcard is not a read (compiles), while a genuine read beyond it still LOUD-skips (E602); mutation-validated per site (width fn, field-name canonicalisation, both dispatch gates, derivability gate, rider — each flips exactly its own test subset)
test_codegen_alias_typeargs_eq_1076.py	34	499	The Eq-dispatch ground-spelling cluster (#1076/#1077/#1078). #1076: structural == over NON-Unit alias type args (Box<MyInt>/MyStr/MyBool/Future<Int>/chains) silently pointer-compared (equal structs → 0, check-green) — equal AND distinct pairs per spelling, i64-width pins with >$2^{32}$ payloads whose low 32 bits collide, MyStr content-vs-pointer compare, plus the #1060-walk width shapes (Bool follows the type-param field, so an i32-sized MyInt/MyStr/Future<Int> manifests); a genuine free T (dead base-generic clone, #912) still compiles via its scalar fallback. #1077: show/hash of Tuple<U, Int> (raw-args Tuple plan branch) and of bare aliased-Unit values (literal-name top-level arms) loud-skipped — all four now compute (exact renders, payload-sensitive hash), literal controls pinned. #1078: element-wise == on arrays of parameterized ADTs (Array<Box<Int>>, literal included) pointer-compared (the IndexExpr operand's element head drops its type args) — equal/distinct/>$2^{3}$2/aliased-element shapes, non-generic-array + direct-compare controls; mutation-validated per site (canonicalization helper, width fn, both dispatch gates, derivability gate, Tuple plan branch, top-level Unit arms, IndexExpr recovery arm — each flips exactly its own subset)
test_codegen_alias_of_adt_eq_show_1085.py	49	1,140	The alias-of-ADT / forall-Eq / bare-Future dispatch cluster (#1085/#1086/#1087 + the PR #1090 review round: #1091/#1092), siblings of #1076/#1077 at entry points the ground-spelling pass never reached. #1085: structural == over an alias of a WHOLE ADT (type MyBox = Box<Int>;, @MyBox.0 == @MyBox.1) silently pointer-compared (equal structs → 0, check-green) — the operand reaches the dispatch as the bare alias name, absent from _adt_type_names; equal AND distinct pairs, i64-width >$2^{3}$2 low-bits-collide pins, String-content, non-generic-ADT and alias-chain shapes, direct-compare control, plus the refinement-over-whole-ADT == (type NB = { @Box<Int> | true }; — the same silent pointer compare, equal + distinct pins). #1086: a forall<T where Eq<T>> instantiated at an Eq alias (@Box<MyInt>) wrong-loud E613'd (the top-level constraint gate misses alias / Future spellings) — equal / distinct / i64 pins for MyInt and Future<Int>, an alias-of-whole-ADT positive, plus a non-Eq alias (Array<Int>) differential (still E613, never the codegen E699 — gate↔codegen lockstep, #732). #1087: show / hash of a bare or aliased Future value loud-skipped (E602) — the inferred type reaches the top-level dispatch un-peeled; aliased + bare Future<Int> / Future<Bool> renders, payload-sensitive i64 hash, plain-Int + aliased-primitive + refinement controls. #1091 + composite-Future (PR #1090 review): the composite path's _parameterized_arg_type recovery UNDID the grounding — bare/aliased Future<Option<Int>> show+hash, alias-of-whole-ADT show/hash (type MyBox = Box;, type MB = Box<Int>;), @Array<FI> slot + array-literal element grounding, with Tuple-component and ctor-argument GREEN pins (grounded at plan consumption, #1076/#1077). #1092: an in-range int literal coerced into a @Byte-instantiated generic ctor field was stored i64 while every reader sizes i32 — MkB(0) == MkB(255) silently equal, extraction read 0 for a stored 255; distinct + equal + extraction + aliased-forall-Eq shapes through the full checked pipeline (_run_checked threads the checker's target-type table exactly as the CLI does), passthrough + Int-instantiation controls; mutation-validated per site (operand grounding, gate fallback, show + hash grounding, recovery grounding, Array-arm element grounding, Byte width coercion — each flips exactly its own subset)
test_composite_postcondition_eq_912.py	16	492	Composite (Box/Option/nested-ADT) == in an ensures postcondition lowers its runtime check to STRUCTURAL equality, not a pointer compare (#912): true @T.result == ctor postconditions run without a spurious Postcondition violation trap in both operand orders, the E500+runtime-trap negative controls prove a false composite postcondition is still rejected by vera verify AND traps, and a Tier-1 verify pin; a function generic over the parameterized ADT itself (fn id2(@Box<T> -> @Box<T>)) with a slot-vs-slot postcondition compiles + runs — the free-type-var scalar fallback affects only the DEAD base generic clone, while the reachable monomorphized clone lowers the == structurally (pinned by a rebox test where a FRESHLY-constructed, structurally-equal, DIFFERENT-pointer result is Tier-1-verified AND runs without trapping, plus a WAT assertion that the reachable mono clone's postcondition uses call $eq_ not i32.eq); a genuinely non-Eq contract composite (Box<Array<Int>>, Tuple) is a clean E613 not an uncaught crash — mutation-validated (neuter the ResultRef arm → left-@T.result run tests AND the rebox/structural-WAT pins flip RED; neuter the free-type-var routing → the Box<T> run tests flip RED via the dead-base-clone E613; remove the postcondition backstop → the clean-E613 tests raise an uncaught exception)
test_contract_predicate_degradation_922.py	9	250	A non-Eq composite == / unsupported hash/show in a CONTRACT-PREDICATE position degrades to a clean diagnostic, never an uncaught Python traceback (#922): a Tuple == Tuple in a requires or a { @T | P } refinement guard is a clean E613, a hash(recursiveADT) in a requires/ensures is a clean E602 (the #912 postcondition backstop caught only AdtEqNotDerivableError, not CodegenSkip); regression pins that valid contracts (primitive ==, derivable-ADT ==, refinements over primitives, primitive postconditions) still compile + run, plus a cross-check that the #912 concrete-Tuple postcondition still degrades to E613 — mutation-validated (neuter each new catch → its repro re-crashes with an uncaught traceback)
test_codegen_arrays.py	242	4,467	Byte type, array literals / bounds checking / length / range / concat, direct indexing of builtin call results (#1048, #1051, alias-canonicalized #1055), array_flatten of inline nested literals + type-variable builtins nested as call arguments + alias-spelled / user-fn call-emission arguments incl. the Map/Set host-import tag inference (#1052, #1053, #1063), nested-alias element classification (#1067), generic-alias container returns (#1068), bare-alias returns + Block args (#1071), Future<alias> element sizing (#1074), map/mapi/fold closure-return Future<T> sizing incl. the fold SlotRef-init fallback (#1079), the post-#1041 Future<Bool> map stride-desync regression (#1081), collection-alias Array<Future<Alias>> payload canonicalization (#1082), construction builtins (#209), compound element types (#132), array utilities (#419 split)
test_array_map_slot_closure_1056.py	10	227	#1056 — a fn-typed slot (@Mapper.0 where type Mapper = fn(A -> B)) as the closure argument to array_map / array_mapi / the array_fold accumulator: let-bound and parameter slots, type-changing Int -> String mappers (map and mapi), chained two-slot maps, order-pinned mapi and fold (non-commutative, non-literal initializer), an apply_fn-parity pin, and the inline-AnonFn control
test_codegen_refinements.py	72	1,208	Assert/assume, forall/exists quantifiers (incl. WAT inspection), refinement type aliases, refinement-predicate runtime guards (#746 — primitive- and @Array-base boundary guards, @Byte-base i32-width guards incl. @Byte-returning fn-call operands + 0..255 range conjoin (#766), tuple-component decomposition at the FFI boundary, generic tuple aliases, infinite-alias E617 fail-closed, refinement-over-tuple unwrapping, zero-size base guard-skip for @Unit and @Future<Unit> (#943)), head-over-refinement shape (#655) (#419 split)
test_codegen_strings.py	113	1,266	String literals + IO host bindings, WAT string escaping (unit + end-to-end), String/Array signatures, format expressions, core string ops (length/concat/slice/char codes/repeat), char classification, string utilities (#419 split)
test_codegen_string_builtins.py	153	1,341	parse_nat/float/int/bool (Result-returning), base64, URL encode/decode/parse/join, search/transform builtins (#198), universal to-string (#106) (#419 split)
test_codegen_numeric.py	86	1,104	Math builtins (#199), numeric type conversions (#208), Float64 predicates + constants (#212), int64-min / float-carry to-string regressions (#475) (#419 split)
test_codegen_io.py	42	821	IO operations (#135: read_line, read_file, write_file, args, exit, get_env, sleep, time, stderr), Markdown + Regex host bindings (#419 split)
test_codegen_collections.py	69	1,141	Map + Set collections (#62), wrapper-handle bit-31 tagging (#578) (#419 split)
test_codegen_json.py	116	1,112	Json collection, typed accessors (#419 split), canonical serialization (#1293 — format_json_number's ECMAScript boundaries and dumps_canonical's shape, insertion-ordered keys, non-finite refusal, and rejection of values outside read_json's domain)
test_json_accept_domain_1306_1308.py	97	720	json_parse's accepted domain on the reference host (#1306, #1308): spec §9.7.1 states it as RFC 8259-valid text that decodes to finite numbers and strings of Unicode scalar values, and all three exclusions are pinned end-to-end through a compiled program that reports which arm it took plus the whole Err message — the JavaScript constants at the top level and nested in containers, with the first of two naming the refusal; a number that OVERFLOWS to an infinity (1e999, -1e999, [1e999], {"a":1e309}, 1E999, [[1e999]]), the second entry route to a non-finite JNumber and the one both host parsers accepted, so it diverged from the stated domain on both hosts at once rather than between them; the same overflow in its INTEGER spelling (1 followed by 309, 310 and 400 zeros, signed and nested), which was reference-host-only because json.loads returns an int there and a float-only range check never saw it, with the bound pinned as the double ROUNDING boundary against float() as oracle and int(sys.float_info.max) + 1 as the control that separates it from the obvious-but-wrong bound; and a lone surrogate parameterised over position (value, key, array element, nested, top-level string) and escape casing. The controls carry the weight the refusals cannot: matched surrogate pairs (single, adjacent, at end of string, literal astral) still parse, 1e308 / -1e308 / the largest representable double still parse so the overflow refusal is a boundary and not a wall, underflow is decided rather than assumed (1e-999 decodes to 0, finite and in the domain, so it is accepted — the plausible wrong answer is symmetry with overflow), "NaN" as a string value and as a key is ordinary JSON, and text malformed for any other reason keeps its host-native syntax message — the constant-lookalike shapes ([Infinity_x], {Infinity:1}) that a raise-on-sight parse_constant hook would have misreported, which is why the hook records and the refusal is decided after the parse, and the sign/case shapes (-NaN, [-NaN], +Infinity, infinity, nan, -Infinityx) that a token scan without a value-start constraint would have claimed. Unit tests on first_domain_violation — the ONE document-order walk both value-level exclusions share, so "whichever comes first names the refusal" needs no precedence table — pin the traversal directly (key before its own value, earlier entry before later, D800/DFFF inclusive at both ends, an int and a bool never read as a non-finite number, and the NaN arm that no JSON text can reach) where the end-to-end probe can only observe the first refusal. The cross-host half is TestBrowserJsonAcceptDomainParity1306_1308 in test_browser.py
test_codegen_decimal.py	57	779	Decimal collection, Decimal monomorphization (#419 split)
test_codegen_host_effects.py	71	1,135	Html/Http/Inference host effects, provider dispatch, postcondition host-import propagation (#823) (#419 split)
test_inference_response_shapes_1333.py	164	2,131	#1333 — Inference.complete parses a provider response by SHAPE, not by position. The Anthropic Messages API returns content as a list of TYPED blocks and a reasoning-capable flagship leads with a thinking block, so content[0]["text"] raised KeyError('text') and the host boundary published the bare key 'text' as the whole Result::Err payload. Three properties, one per defect: selection by type across both response families — the OpenAI-style message.content is a string, a list of typed parts, or null on a reasoning turn, where the old str(...) returned the literal completion "None" — with a selected entry's text itself required to BE a string, the review having found the same coercion one level deeper, where text: null became that completion and an object became a Python repr; every shape failure and HTTP rejection naming the provider AND the model that answered, with the error body read under a 64 KiB cap so the message bound is a memory bound too, every interpolated field routed through the same 200-character limit, and the configured key plus any credential-shaped token redacted before it can reach a Vera value — on every route, a table of twelve parametrized rows standing in for the invariant after a review pass found the non-JSON-body path unredacted, a sweep found six more, and a second pass found four render sites whose api_key could be dropped with nothing red; two structural tripwires now hold it — the count of api_key-carrying render sites, read by an AST walk rather than a regex (which undercounted the same source by one and could not see a positional key in a multi-line call), and the row count itself, since deleting a row was invisible to the first and left the suite green one cell lighter. An empty or whitespace-only completion is an error only when the provider explained it — stop_reason refusal or max_tokens, message.refusal, finish_reason length — with the reason matched case-insensitively and the token carried verbatim into the diagnostic, and a response with no block or part of the selected type at all reported as an error naming the types that were present, and the blank test is .strip() on both the string and list paths, which is what round 9 claimed and delivered only for the exactly-empty fragment, which is what makes the sweep's own misattribution impossible to repeat — with VERA_INFERENCE_PROVIDER unset, auto-detect takes the first key set to a non-empty value in registry order, so a still-exported Anthropic key won the "xAI run"; and a boundary that labels any exception this module did not itself write. The verbatim channel belongs to a dedicated InferenceError and nothing else: the original rule named plain RuntimeError / ValueError by exact type, which the PR review refuted — those are the types an unforeseen transport failure raises too, so RuntimeError("boom") from below claimed the channel and surfaced as the bare boom. The headline cells run END TO END through execute() over a mocked urlopen — the product path the report came from — with the six-provider sweep parametrized in registry order, its rows pinned against _PROVIDERS so a new provider cannot silently leave the sweep. Mutation-checked, every count re-measured on the tree as it stands: the by-position read 45, the boundary's plain-type rule 18, the shared redaction helper 28, the boundary label 8, the str() coercion 8, the missing-text-key skip 7, the reason clause 21 (the same whether its function body is emptied or all four call sites are neutralised — an earlier note claimed the two forms differed), the output_text preference 6, the empty-completion rule 10, the blank test's truthiness revert 4, the reason's case fold 3, the xai credential prefix 3, the strict .decode("utf-8") 3, and the narrower one-to-three-cell guards (redact-before-truncate, the exact-key rule, the output_text preference, the truncation window's start, the "(no keys)" honesty rule, the credential pattern's eight-character floor, and the three bounded-read guards). Every pytest.raises in the file names InferenceError rather than RuntimeError: the class is a RuntimeError subclass, so the looser assertion accepted a site regressing to a plain one — making that regression fails 15 cells now against 2 before. The plain-type figure had read 5 with the drop blamed on cells bypassing the boundary; that was wrong. Threading the model into the boundary label made it a prefix of itself, so eleven startswith cells matched the wrapped message they existed to reject and lost discrimination silently — they now assert the label's absence too, via one shared helper, and the figure went back to 16, rising with each _assert_deliberate cell added since
test_codegen_nat_guards.py	61	1,435	@Nat runtime guards: subtraction underflow (#520) and binding-site narrowing (#552 let site; #747 tuple-destructure / match-bind / ADT sub-pattern / ctor-field / call-arg sites; #758 per-leaf function-return guards incl. type-alias returns and TCO preservation on mixed-arm tails — i64.lt_s; unreachable net, @Int targets exempt) (#419 split); #758 @Int -> @Nat return-position guard; #983 review adds alias-aware return gates (type Count = Nat narrow, type MyInt = Int widen), the alias-to-refinement single-guard exclusion, and the per-narrowing-leaf emission that keeps a non-narrowing @Nat -> @Nat recursive tail call's return_call (TCO) intact. #1256 extends both alias-aware gates to a parameterised alias APPLICATION (type Ident<T> = T; type Count = Ident<Nat>;), which the name-only chase resolved to the bare head Ident — so neither gate fired and f(0 - 5) returned -5 through the @Nat slot, #983's silent negative one spelling over. Each parameterised case carries its unparameterised twin as the oracle (the claim is that the two spellings compile to the SAME guard, which a bare presence assertion would not catch losing), plus the run-trap on the violating value, the pass on a satisfying one, and the refinement-over-application control that pins the _refinement_guard_parts conjunct still keeps a refined return single-guarded
test_codegen_translator_fixes.py	27	528	WASM call-translator regression fixes (#475): string/array slice clamps, char-code bounds, URL/base64/parse edge cases, map-array-value rejection (#419 split)
test_codegen_gc_alloc.py	39	892	Layout helpers, bump allocator, GC core (#515), shadow-stack overflow, multi-page grow (#487), worklist overflow (#348) (#419 split)
test_codegen_gc_rooting.py	38	1,560	Opaque-handle param rooting (#347, #490), host-walker GC rooting (#692), Map host-store reachability (#695), ADT-builder rooting (#743) (#419 split); plus the #841 Future-handle battery (TestFutureHandleGCRooting841) — eager-GC survival across an intervening alloc, the operand-stack window (both(async(A), async(B)) with get/post-distinguished Err text), Phase-2c reclamation of fire-and-forget futures via host_store_sizes["future"], and repeated-await memoization; host-import pair-let rooting (TestHostImportPairLetRooting846) — IO.args / IO.read_line pairs surviving an intervening alloc under eager GC, with IO.read_file / IO.get_env ADT-path confirmation; and the _ShadowGuard.push slot-complete bound (TestShadowGuardPushBound791) — partial-headroom / full-window / negative-sp rejection and the exact-final-slot accept boundary, constructed directly on a hand-rolled module
test_codegen_gc_reclamation.py	21	706	Transient Map/Set/Decimal reclamation (#573; scale trio marked stress, #738), bucket occupancy (#706), SameValueZero keys (#743) (#419 split)
test_codegen_contracts.py	33	601	Runtime pre/postconditions, contract fail messages, old/new state postconditions, the #958 tier-agnostic always-emit pin
test_codegen_decreases_guard.py	24	859	The #1172 runtime termination guard: non-terminating measures trap through the contract channel instead of hanging (the issue's ADT repro, constant/growing/negative-floor scalars, a lexicographic violation, mutual where recursion), terminating programs run clean with the guard emitted (Tier-1 countdown, the corrected spec Ackermann, sequential siblings pinning the exit restore, a concrete ADT measure), the tier3-obligation ⇒ emitted-guard differential, E127 rejection of non-well-founded measures (Float64/String/Bool and a lex component) plus acceptance of the well-founded family, and the parameterized-ADT-measure no-guard pin (#1177)
test_codegen_monomorphize.py	258	5,102	Generic instantiation, type inference, monomorphization edge cases, ability constraint satisfaction (Eq/Ord/Hash/Show), operation rewriting (eq/compare), show/hash dispatch (incl. structural show/hash for composites, same-base finite nesting, and _split_param_type — #911; recursive-ADT show/hash via a generated self-calling helper, deep-list termination + GC-frame $gc_sp restore, non-generic mutual recursion — #924), ADT auto-derivation, array operations (slice/map/filter/fold), nested where-helper emission on the non-generic path (#978/#989 — a grandchild helper using eq/compare in its body or contracts must have its ability op rewritten so its body is emitted, and a node with two nested helpers emits both)
test_codegen_nested_nullary_ctor_994.py	7	229	#994 F2 nested payload-less constructor in a forall<T> ==/!= — the #979/#981 checker adoption newly accepts ensures(Some(None) == @Option<Option<T>>.result) under forall<T>; check+verify passed but compile raised a spurious E613 because the structural-Eq derivation erased the type argument (the inner None renders bare Option, so Some(None) recovers as Option<Option>; the dead base clone's slot renders Option<Option<T>> with a nested free T the top-level-only free-var check missed). The fix recovers the fully-concrete name from whichever operand carries it (both share a type by E142) and routes to the scalar dead-code lowering only when NEITHER resolves. Pins: both operand orders + != + a body-position == compile + RUN to their sentinels (55/77), with concrete and payload-carrying controls that must keep compiling — mutation-validated (remove the sibling recovery → the reachable clone TRAPS on a scalar pointer compare; remove the concreteness gate → the base clone flips back to E613)
test_codegen_closures.py	63	2,024	Closure lifting, captured variables, higher-order functions, iterative-builder shadow-stack regressions (#570), closure return-value shadow-push balance for both i32-pair and i32-ADT branches across array_map and array_mapi, plus VERA_EAGER_GC injection self-test (#593), IndexExpr-of-FnCall element-type inference (#614), non-contiguous capture and walker-order miscompiles (#615), Future<T> free-variable capture width (#1044)
test_codegen_invariant_e699.py	5	266	CodegenInvariantError raised in a translator surfaces as a structured [E699] "internal compiler error" at the _compile_fn boundary, not a raw traceback (#657 Track 2), across all four contract-lowering paths — body, closure, precondition, and postcondition (#939 completes the precondition + postcondition nets)
test_codegen_modules.py	186	3,835	Cross-module guard rail, cross-module codegen, module-qualified call resolution bypassing a local shadow incl. intra-module siblings, where-fn helpers both directions, unit- and pair-returning calls in statement position, and the @Nat-parameter guard mirrored onto shadowed targets (#814 §8.5.3), name collision detection (E608/E609/E610), fused-async await of a cross-module future (#841/#842) and of an indirectly-called closure (#843 — await(apply_fn(closure, …)) classified by declared return type incl. generic-alias type-arg substitution; unresolvable shapes fail loud via E616 or the #867 WASM-validation trap), transitive module imports (#890 — a main -> mid -> base chain and a main -> {left, right} -> base diamond compile and run via the real on-disk resolver, while a transitive symbol stays invisible to the top-level importer per §8.6.4), a non-void ModuleCall used directly as a constructor argument or array-literal element (#905 — its return type is resolved at the field/element site via the shared _resolve_module_call_wasm_name, closing a check-green→codegen-crash gap; the non-void sibling of #902's Unit-field fix), a user-defined function named show/hash used in a constructor field or array element (#908 — the ability-op width special-case must defer to the user fn's declared return width when the name resolves to a user fn, matching codegen's not in known_fns dispatch gate; a genuine unshadowed ability op still uses the special-case width), and an imported function's nested where-helper at any depth (#989 — the registration walk must reach grandchildren via _flatten_where_fns, so an imported libfn -> child -> grandchild chain that checks + verifies green also emits every helper and no call dangles)
test_codegen_coverage.py	5	244	Defensive error paths: E600, E601, E605, E606, unknown module calls
test_execute_characterization.py	24	510	Characterization harness pinning execute()'s observable contract ahead of the #421 runtime decomposition (#734): every ExecuteResult field (value int/float/str — including a transparent Future<String> return decoded for display (#1047) — heap-pointer/None, stdout, state, exit_code, stderr) crossed with the three completion modes — normal return, WASM trap (raises WasmTrapError with a classified kind, output-before-trap preserved), and interrupt/exit (IO.exit(n) → exit_code n with value None, Ctrl-C → 130) — plus the positional-constructor compatibility shape and capture_stderr True-vs-default. Mutation-validated: every cell confirmed to flip RED when its target return path in api.py is deliberately broken (9 mutations, 0 green-for-the-wrong-reason tests)
test_walker_defensive_branches_597.py	34	855	Synthetic-AST tests for the 11 defensive isinstance branches added by #597 (_scan_io_ops / _scan_expr_for_handlers / _infer_expr_wasm_type / _infer_vera_type) plus the 5 pr-review fixes (#2/#3/#8 — ModuleCall/AnonFn/QualifiedCall return None; dead is not None guards on Block/HandleExpr removed). Also hosts the two compilability pre-scans' field-coverage gate (#1210 rounds 5, 7 and 9): it derives the obligations from the dataclass fields of vera/ast.py — one per (class, field) PAIR — and a pair is discharged only by the conjunction (the class isinstance-branched AND the field name read inside that branch) or by a justified-ignore entry naming the route its expressions ARE reached by. Stronger than scripts/check_walker_coverage.py, whose set is the Expr subclasses and whose verdict is "the class is NAMED"; and stronger than the class-keyed obligation it replaced, which discharged the moment a class had ANY branch, leaving a new field on an already-dispatched class to a second, weaker screen (the mutation is pinned: fabricating one must fail the OBLIGATION). The ignore table takes either key shape, and a class-level entry is permitted only while its class has a single field — otherwise it would exempt whatever field the class grows next, the same hole one table down. The name-based limit of the dispatch route is stated on the gate. Round seven adds the boundary-guard derivation gate: the emitter, the return-epilogue predicate and the import pre-scan must all read one tuple decomposition and none may reclassify behind it, which is the structure that makes their agreement a property of one function rather than of three. Plus contract_exprs's explicit dispatch, including the raise on an unknown ast.Contract subclass
test_check_walker_coverage_597.py	15	311	Unit tests for scripts/check_walker_coverage.py parsing logic — Expr subclass extraction, isinstance flattening (incl. tuple form), checklist-block anchoring (incl. CR-3 regression test: # Foo → bar outside WALKER_COVERAGE block not counted), section-header tolerance, auto-discovery invariants, end-to-end main exit code
test_diagnostic_fields.py	90	1438	Unit tests for scripts/check_diagnostic_fields.py (#682) — required-field detection, the warning severity rule (no fix), spec_ref validity, the codegen structural-exemption registry, the # diag-fields-exempt per-call opt-out, the error_code-registration check (#828), a live-tree integration check that all of vera/ is fully tagged, and the narrowed plumbing-skip (#827: the skip now requires a genuine self-receiver helper method — a direct class member, not a @staticmethod, module-level or nested look-alike — whose sole own-scope Diagnostic it is, where own-scope means the body and excludes decorators / parameter defaults / annotations; a stray second ctor, or one in a nested def, is inspected by all three passes: field presence, spec_ref validity, error_code registration; each guard and each pass's use of the skip is mutation-pinned separately; #956: the skip also requires that sole ctor be reachable as the helper's result — return-ed, appended, or bound to a local later return-ed/appended — not merely constructed and handed to something else, a name rebound by any binding form — counted generically: every Store-context name (assignment/unpack of any shape, for/with targets, walrus), import ... as, except ... as, match captures, parameters, and nonlocal declarations in nested functions; a bare annotation is not a rebind, and the return/append name-match is order-sensitive — after that binding is treated as unreliable rather than reachable, and only a self.<attr>.append(...) call counts as a diagnostic sink, not an append to an unrelated throwaway local; #955: the # diag-fields-exempt opt-out is honoured for an unresolvable non-literal severity/spec_ref — marker found anywhere across the call's span — but never for a spec_ref/error_code that resolves yet is factually wrong, and the error_code pass skips non-literal codes entirely)
test_stress.py	16	553	Scale-dependent regression tests (#596) — @pytest.mark.stress, skipped by default. 9 logical tests × eager-GC lane parametrisation = 16 test instances. 10K array_map, 5K nested-array array_map$, 1\text{K}-\text{deep} \text{tail} \text{recursion} \text{with} \text{allocating} \text{arg}, 1\text{M}-\text{deep} \text{tail} \text{recursion} \text{with} \text{allocating} \text{arg} (#549 \text{GC}-\text{aware} \text{TCO}), 20 \times 20 \text{nested} \text{array}-\text{fold}-\text{of}-\text{array}-\text{fold}, 100\text{K} $array_fold, 10K String allocations, 1K State<Int> get/put cycles, 10K IO.print calls. Pins #570 / #515 / #593 / #549 / #487 / #348 / #573 regression coverage
test_string_length_soundness.py	15	278	#802 — string_length code-point vs UTF-8 byte soundness: a non-literal string_length defers to Tier 3 (the issue's "é" probe no longer proves == 1 at Tier 1), a string-literal length is modeled at its exact UTF-8 byte count (== 2 for "é"), and the boolean predicates string_contains / string_starts_with / string_ends_with stay Tier 1 (sound under UTF-8 self-synchronization), while a predicate over an astral (> U+2FFFF) or lone-surrogate literal defers to Tier 3 (z3.StringVal cannot model those code points)
test_errors.py	62	657	Error code registry, diagnostic formatting, serialisation, SourceLocation, and error display sync — the canonical E001 diagnostic must match each of its mirrors: README.md, docs/index.html, spec/00-introduction.md, AGENTS.md's example --json block, and the hardcoded example in scripts/build_site.py that generates docs/index.md (#829; AGENTS.md's ellipsis-truncated description/rationale are prefix-compared, its error_code/spec_ref/fix exactly)
test_eq_contract_874.py	13	430	eq/compare ability ops in contract position: codegen canonicalization + verifier Tier-1 discharge/counterexample, where-fn contracts, compare Ordering-sort materialization, shadowing guard (#874)
test_formatter.py	542	3,638	Comment extraction, interior comment positioning, expression/declaration formatting, match arm block bodies, §1.8 rule 2 in value position (a let-bound match/if expands exactly as one in statement position, and a comment above an arm inside a statement's value stays on that arm), blank-line preservation (§1.8 rule 13 — gaps between statements, before a block result and around a comment, collapsed to one and never invented), idempotency, parenthesization, spec rules, ability declarations
test_cli.py	273	4,612	CLI commands (check, verify, compile, run, serve, test, fmt, version, quiet), subprocess integration, JSON error paths (including the verify --json obligations array and its summary-reproducibility pin, #967, and the #1242 partition pin — the array is emitted unfiltered, a refuted obligation is counted by no summary field, and it still joins its E500 on the location key), runtime traps, arg validation, multi-file resolution, IO exit codes, --explain-slots (including the #1208 naming pins — an alias in type-argument position is tabled resolved, and a forall variable shadowing a module alias keeps the two parameter stacks apart — and the #1217 where-helper tables: the helper prints indented under its parent, appears in the JSON qualified as parent.helper, and inherits the enclosing forall variables so the shadowing holds inside it too), builtins/effects/errors introspection dispatch, and a USAGE-completeness guard (every dispatched cmd_<name> handler has a help row)
test_introspect.py	39	221	vera builtins/effects/errors --json registry introspection (#539): the {schema, items} envelope, count-equals-registry differential per registry, error-phase derivation, effect/ability kind tagging, the parameterised Exn<E> effect, and best-effort since attribution with full-coverage guards
test_resolver.py	20	602	Module resolution, path lookup, parse caching, circular import detection, the E011/E012/E013 diagnostic contract, internal-error isolation (a compiler bug is not masked as E013), and the transitive-closure return of resolve_imports (#890 — a diamond yields each reachable module once, direct imports tagged direct, the transitive one not)
test_types.py	82	443	Type operations: subtyping, effect subtyping, equality, substitution, pretty-printing (including leaked-placeholder rendering to ?, #1069), canonical names
test_wasm.py	29	502	WASM internals: StringPool, WasmSlotEnv, translation edge cases via full pipeline; plus the fused-await payload-alias canonicalizer cycle-guard pins (TestCanonicalizeTypeExprAliases)
test_verifier_coverage.py	92	1,651	Verifier/SMT coverage gaps: SMT encoding paths, verifier edge cases, defensive branches, #667 SMT translator coverage for FloatLit / IndexExpr / ArrayLit (Tier 1 verification of float/array literal/index contract predicates)
test_verifier_sort_name_collision_884.py	5	203	#884 Z3 sort-name collision — regression pins that lossy type-name mangling can no longer collide two distinct ADT/tuple sorts onto one Z3 datatype (_get_or_create_adt_sort / _get_or_create_tuple_sort routed through the injective mangle_type_name), plus the Array-element reverse-lookup fix (_get_element_sort_for_array)
test_verifier_nested_ctor_sort_918.py	14	441	#918 same-ADT self-nested constructor sort selection — a Some(Some(x)) body (or nested same-ADT ctor literal in a contract) once resolved the outer ctor to whichever Option<...> instantiation was cached (base-name-wins), feeding sort.constructor(idx) a wrongly-sorted DatatypeRef and crashing Z3 with an uncaught traceback on a vera check-green program; the fix translates the ctor call's arguments, recovers each argument's Vera type from its Z3 sort, and unifies against the ctor's declared field types to pin the owning ADT's FULL instantiation. Pins: nested-body + nested-contract verify without crash, a TRUE nested postcondition PROVED at Tier 1 (not blanket-demoted), a FALSE one still disproved (E500 soundness), the #887-trap single-level call-arg staying opaque/clean (on-demand materialisation gate), a different-ADT nesting staying clean, and no Z3-internal exception text leaking as a diagnostic
test_verifier_nullary_ctor_sort_994.py	11	228	#994 F1 bare nullary-constructor sort selection in ==/!= — the #979/#981 checker adoption newly accepts Some(None) : Option<Option<Int>> compared against None/Some(None) in a contract; a bare None carries no payload, so the base-name scan picked the wrong live Option<...> sort and _datatype_value_eq's left == right raised an uncaught Z3 sort mismatch on a vera check-green program. The fix hints the nullary-ctor sort from the checker's recorded (instance-substituted) semantic type via the gated #918 pinning, and degrades a residual sort mismatch to Tier-3 rather than crash. Pins: true != None / == Some(None) PROVE at Tier 1 (both operand orders, concrete + forall), false == None disproved (E500) against a match-based oracle, verify --json always emits JSON, and a direct _datatype_value_eq degradation backstop — mutation-validated (disable the hint → the false-disproof tests flip RED; disable the guard → the direct mismatch backstop raises)
test_verifier_where_helper_scope_991.py	5	235	#991 lexically-scoped where-helper resolution — the flat, last-wins env.functions lookup assumed the WRONG same-named helper's ensures at a call site, a false E500 in a diamond of two siblings each carrying a nested leaf with a different postcondition. The scoped lookup resolves a bare helper call to the nearest same-named helper in the enclosing where-tree (own children, then ancestors), then the top-level function, then the flat registry. Pins: the diamond verifies (each parent proves against its OWN leaf), the wrong-helper counterexample does not arise, and a genuine postcondition violation against a helper's own body is still caught — mutation-validated (revert the scoped lookup → the diamond flips RED). Plus the clone-scope shape: _verify_generic_instances threads the enclosing ancestor chain into each clone's verification, so a nested generic helper's unshadowed ancestor-helper call cannot be captured by a same-named decoy helper under another function (false E500) — verified AND run (verifier↔codegen agreement) with a non-trivial decoy postcondition, per-function Tier-1 ensures-obligation checks (present and verified, never skipped), and both doors executed (host and decoy run values)
test_wasm_coverage.py	226	3,976	WASM coverage gaps: helpers unit tests, inference branches, closure free-var walking, operator/data/context edge cases
test_tester.py	17	445	Contract-driven testing: tier classification, input generation, test execution, skip message content
test_tester_artifacts.py	1	89	vera test compiles through the same artifact tables as the other CLI doors: the tester-compiled WAT for a tuple-component widening carries the widen guard (without the shared artifact tables, cmd_test emits no guard while the verifier claims Tier-3 runtime-guarded — a verifier↔codegen divergence)
test_tester_coverage.py	49	1,395	Tester coverage gaps: String/Float64/ADT parameter input generation, Bool/Byte parameters, unsatisfiable preconditions, type expression edge cases, FP model-value extraction (NaN/Inf/signed-zero, #797), the #1208 naming pin (the threaded alias environment canonicalizes a type-argument alias), and the #1216 resolution set — an alias-typed parameter is trialed rather than skipped, its alias-spelled requires constrains the generated inputs, a refined alias reaches Z3 with its predicate so no trial violates codegen's entry guard, a forall variable shadowing a same-named module alias still resolves to an unsupported type variable, and a parameter that resolves to a non-encodable type still skips with that type named; plus the #1229 set — an UNTRANSLATABLE input constraint skips the function naming the blocking conjunct instead of scoring the resulting entry-guard trap as a contract failure, on the reported string_length repro, on a mixed clause (only the untranslatable conjunct is named), on a quantified precondition and on a refined parameter's predicate, with a Tier-3 control that must still be tested so a skip taxonomy firing on everything cannot pass
test_markdown.py	94	610	Markdown parser: block/inline parsing, rendering, round-trips, edge cases
test_lsp.py	146	2470	LSP transport + coordinate layer (#222 Phase C) and language features (#222 Phase D): parametrized code-point↔UTF-16 goldens incl. astral-plane fixtures and surrogate-pair snapping, Span (1-based, exclusive-end) and SourceLocation (0-based col) → LSP Range conversions, point→token-range widening, DocumentStore open/change/close + index invalidation, an in-process handler-drive test, and one stdio end-to-end round-trip against the real vera lsp subprocess (initialize → didOpen → shutdown → exit) pinning serverInfo + textDocumentSync capabilities; plus the Phase D feature suite — parse-error single-diagnostic path, type-error verification short-circuit, tier=3 in E520 diagnostic data, per-function tier Hint synthesis (and its suppression for functions with violated obligations), smallest-enclosing-span hover, De Bruijn slot goto (most-recent-parameter jump, out-of-range None, off-slot None, and the #1208 keying pins: a parameterised reference resolves, an alias-spelled parameter is reachable from a canonically-spelled reference, and a forall variable shadowing a module alias lands on the right parameter), and typed-hole completion (inside/after hole, away-from-hole None); plus the Phase E speculativeEdit suite — identical-text all-unchanged, breaking edit surfaces newly_undischarged (violated nat_sub) with canonical state untouched, strengthening edit surfaces newly_discharged, parse/type errors report ok:false, deleted functions report removed, proof_delta purity; plus the Phase F1 proposeEdit suite — the apply gate (clean and strengthening edits apply, breaking and non-compiling edits refuse), force overriding both gates with the delta still reported, wiring against a structural fake server (apply round-trip with exact full-document replacement range, refuse touches no canonical state, unopened-URI clamp sentinel), and full-document-range goldens (trailing-newline virtual line, UTF-16 end column); plus the Phase F2 strengthenContract suite — splice goldens (first-clause-only replacement with byte-identical remainder, ensures variant, unknown-fn None), the call-site audit pin (tightened precondition refused with newly_undischarged call_pre items, canonical state untouched), provable-ensures strengthening applies, and the three splice-target refusal paths (no analysis, unparseable document, unknown function); plus the Phase F3 addEffect suite — transitive-caller closure goldens (diamond in declaration order, leaf, unknown-fn None, recursion appears once), handler bounding (#725: a caller discharging the effect around its only call site drops out of the closure and is not rewritten, while a second unhandled path, a call in a handler clause, a handler for another effect, a handler naming a different instance of the same effect (handle[State<Nat>] against a State<Int> propagation, which the checker does not discharge — end-to-end that caller must still be rewritten and the candidate must still apply, with the matching State<Nat> propagation against the same fixture as the positive control that this handler key does prune something), and a bare where-helper call all keep it in, as does a refinement type argument at either depth (Exn<{ @Int | p }> and Exn<Array<{ @Int | p }>> render as their bare base type but discharge nothing of Exn<Int> — also pinned end-to-end), while an unparameterised handle[IO] does bound an IO propagation, a whitespace-spelled State< Int > request still bounds, and nesting bounds in either order (a matching handler inside a foreign one, a foreign one inside a matching one) — plus a key-level pin that handle[Mod.IO] keeps its module, and the effect-less query pinned handler-unaware; plus the two boundary pins the review added — a call in the handler's STATE INITIALISER keeps its edge, since the initialiser is evaluated in the enclosing scope before the handler is installed (pinned beside the E125 the checker raises there against a pure caller, with the identical call in the handler body clean as the contrast), and an alias-spelled handler does not bound a State<Int> propagation though the checker discharges it (handle[State<MyAlias>] with type MyAlias = Int — the spelling comparison's under-prune, #1292, with the alias-spelled request as the control that does prune)), effect-row rewrite goldens (pure to singleton set, source-preserving append, already-present None, base-name identity blocking State next to State), diamond propagation applying one multi-site candidate with the bystander untouched, mixed append/replace rows with already-satisfied callers skipped, the fully-satisfied no-op shape, and the two refusal paths; plus the #728 instruction-contract suite — the LSP message carries description, rationale, and the Fix: paragraph (also pinning single E501 emission at the LSP surface), and a bare diagnostic maps to the description alone
test_browser.py	413	5,094	Browser parity: Python/wasmtime vs Node.js/JS-runtime output equivalence across IO, State, contracts, Markdown, Regex, and the examples the browser target can execute (two explicit lists in the file, not the whole examples/ directory — interactive stdin, file IO, DB and the non-standalone modules example are excluded with their reasons recorded); plus the #349 runtime.mjs coverage battery — per-value-type and per-key-type Map variants, per-element-type Set variants, cold Decimal branches (exact-zero sign, negative-shift division, decRoundPlaces special cases, non-finite storage), readJson/json_stringify across every Json ADT tag, the Regex/Json Result.Err arms, and nested-Markdown walks. Two operations carry a canonical form the specification states rather than merely agreeing across the hosts, so their batteries assert more than equality: json_stringify (spec §9.7.1) pins the expected string on every Json ADT tag and on the number-rendering boundaries, checks three-pass idempotence, checks that a non-finite JNumber fails on both hosts and prints nothing, pins the object key orders an ordinary JS object cannot carry (array-index keys, which ES enumeration hoists to the front in ascending numeric order, and a __proto__ key, whose assignment writes a prototype instead of a field) on both a parsed and a program-built object, and checks the reference host's own number rendering differentially against a real JSON.stringify over doubles drawn from raw bit patterns; md_render (§9.7.3) pins the expected render, re-renders it to prove the fixed point, runs the round-trip property over a corpus carrying the container and multi-line shapes a flat corpus misses, and renders MdBlock values the test builds directly, since several renderer rules — a container's child separator, an empty container, a code span wider than one backtick — are unreachable through md_parse. plus the #1306/#1308 accept-domain battery (TestBrowserJsonAcceptDomainParity1306_1308), which runs one .wasm under both runtimes and compares the WHOLE stdout — arm taken and Err message together — over the JavaScript constants, over numbers that overflow to an infinity in both their exponent and integer spellings, and over lone surrogates at every position a string can occupy, with the expected sentences imported from vera/wasm/json_serde.py so runtime.mjs's hand-copied duplicates are held against the originals, beside acceptance controls (matched pairs, finite boundary values, underflow to 0, "NaN" as a string value), a ten-case host-native-message battery pinning that neither the substitute-and-re-parse probe nor the value-start constraint hijacks an unrelated syntax error (-NaN is the case needing both rules — the substitution alone turns it into -0 and manufactures a refusal the reference host never makes), a precedence case fixing that a non-finite constant outranks a lone surrogate on both hosts though each reaches that answer by a different route, and a document-order case fixing that overflow and lone surrogate are resolved by one walk rather than by two per-host precedence rules that would agree on every single-violation document; md_parse itself is not yet at parity and its remaining divergence classes are a tracked bug (#1301); the suite pins the shapes the two implementations agree on
test_conformance.py	1220	154	Parametrized conformance suite: parse, check, verify, run, format idempotency across 244 programs; a negative entry fails at the stage expected_error_stage names (check, the default, or compile — which also asserts the program type-checks cleanly first)
test_prelude.py	29	585	Prelude injection: Option/Result/array operation detection, combinator shadowing, type aliases, the reserved namespace every injected alias declaration lives in — checked against the checker's own E154 regex rather than a second spelling of the rule, since an alias the prelude injects outside it is one codegen resolves and the checker leaves opaque (#1184/#1221) — end-to-end compilation
test_checker_apply_fn.py	18	455	#854 — apply_fn as a checker special form: zero-warning pins (API + CLI --json + closures.vera), E201 arity / E202 type / non-function-first-arg errors, E122/E125 effect-row enforcement for applied fn values, E151 redefinition rejection, variadic two-param application, prelude combinator regression pins
test_prelude_diagnostics.py	8	271	#851 — prelude combinator skip-warnings: unreferenced-prelude E602/E604 suppression (zero-warning minimal compile, API + CLI --json), <prelude> origin attribution for referenced-but-skipped combinators (text + to_dict), transitive reference scan, and user-fn warning locations pinned unchanged
test_readme.py	2	79	README code sample parsing
test_html.py	4	167	HTML landing page code samples: parse, check, verify (vera:skip-annotation aware, #538)
test_float64_fp.py	10	260	#797 — @Float64 contracts via Z3's IEEE-754 FloatingPoint sort: unsound relational / reflexive contracts (rounding at $2^{53}$, NaN, Inf) flip from proved to violated/Tier-3, NaN-guarded contracts still verify at Tier 1, ==/!= use IEEE fpEQ/fpNEQ (incl. +0.0 == -0.0), % matches codegen truncated remainder (not fp.rem; NaN-by-zero + large-magnitude edges), and float_is_nan / float_is_infinite / nan() / infinity() translate to FP predicates / constants. Also guards mixed @Float64/@Int ordering as a clean E142 (not a Z3 crash)
test_float64_builtins_807.py	81	491	#807 — Tier-1 modeling of the modelable @Float64 builtins. float_clamp modeled unconditionally as faithful WASM f64.min(f64.max(v,lo),hi) (the NaN-propagation soundness guard distinguishes it from a naive z3.fpMin/fpMax); int_to_float / float_to_int concrete-gated (symbolic args defer to Tier 3 — Z3's symbolic FP↔Real reasoning returns spurious counterexamples); float_to_int domain obligation (E529) for concrete NaN/Inf/out-of-range args. Verify-vs-run differentials confirm each model agrees with wasmtime bit-for-bit (±0, ±inf, NaN, ties, lo>hi, the $2^{53}$ rounding boundary, i64 max, and the trap cases)
test_examples_ephemeris.py	11	351	#143 — the tree's only floating-point example. Pins the rendered stdout byte-exact and both geocentric distances, then re-derives the angles from that output and checks them against an INDEPENDENT reference (ERFA's analytic model via astropy) to 30″ — the tolerance is the JPL element set's arcminute accuracy, not the code's. Per-function tier pins (wrap_deg at Tier 1, kepler_solve's termination proved, and the two eccentricity refinement binds verified in earth_elements and mars_elements — the bound-at-construction story) deliberately stand in for a corpus-wide tier count, which moves legitimately whenever obligations are added elsewhere. The transcendental contracts are pinned at EXACTLY tier3 across three solver budgets, which is the categorical claim the example's header makes: verified at 60 s would falsify it and timeout would mean the demotion had become merely slow. The fixture fails on any type error before verifying, so no tier is ever asserted about a program that does not compile.
test_build_site.py	54	847	Site-asset tooling — _abs_links rewriting (relative links, fenced-block immunity incl. inline backticks and tilde fences, http/https/fragment pass-through, Vera effect syntax not mis-parsed), build_site <lastmod> stability (preserve/refresh keyed on URL-structure change), check_site_assets sitemap staleness (missing / date-only-clean / structural-stale), and the #538 leak guard (vera:skip fence annotations stripped from generated docs/SKILL.md / docs/llms-full.txt, with a non-vacuous precondition that the source carries annotations); plus the #1154 check_fact_coherence() suite — index.html↔index.md fact extraction and divergence detection; plus the #1341 implementation-status appendix — Status: callout extraction in both spellings (blockquote and bare paragraph), nearest-heading attribution, generated-file header, idempotence, POSIX-form chapter paths, and count parity against an independent live scan of spec/
test_builtin_typevar_collision_970.py	61	811	#970 a user forall type-var name colliding with a built-in generic's internal name (T/E/A/B/K/U/V): focused check/verify pins for the compound-argument shapes (@Array<Option<T>>, @Result<Int, Option<E>>, @Map<K, Option<V>>) plus a collide-vs-control differential battery over every generic-builtin family and contract/where-helper position. Also pins marker-strip (the #b namespacing marker must never reach an E205/E202 diagnostic), a registry-consistency pin (every built-in ability-constraint type_var stays a member of its forall_vars), the dual completeness-gap pinned in both argument orders, a tier-split equality pin, and the #1069 leaked-placeholder message-rendering sweep (a stripped built-in var renders as ?, not a bare letter, at every reachable actual-type slot: the mismatch sites plus the operator/index/interpolation family, assert/assume, if condition and branches, and the contract/refinement predicates — one parametrized row per converted render slot, with the provably-unreachable sites documented in the class docstring)
test_check_changelog_updated.py	68	712	check_changelog_updated.py unit + end-to-end tests: file classification (incl. file-style exact-match vs directory-style prefix-match), CHANGELOG diff parsing with [Unreleased] section tracking, bare-heading rejection, and full-file context (regression test for bullets far below the heading), Skip-changelog: trailer detection, temp-repo integration covering substantive/exempt/label/trailer paths, and GIT_*-env hermeticity of the temp-repo fixtures (regression for the pre-commit-hook env leak)
test_release.py	62	798	Release policy and registry verification (#481): strict project-name and version parsing/comparison, version-bump/TestPyPI/recovery planning, exact confirmation and immutable-tag guards, first-parent version-introduction discovery, package-change recovery refusal, non-empty CHANGELOG extraction, one-wheel/one-sdist SHA-256 manifests, malformed registry-response handling, missing/filename/hash propagation retries, exact filename/hash verification, and CLI dispatch/GitHub-output wiring. An autouse fixture scrubs hook-exported GIT_* variables so the tmp-repo git calls (fixture helpers and release.py's own) never resolve to the developer's repository when the suite runs inside a pre-commit hook.
test_check_doc_counts.py	103	1,151	check_doc_counts.py's pure per-document checks: KNOWN_ISSUES refactoring line counts (±10% tolerance band incl. the exact-boundary case, drift detection, empty-file citation, hyphenated paths, missing file/section/rows, the #419 empty-section sentinel + its cannot-mask-a-malformed-table dual), HISTORY version-row format (issue-link limit, — separator rejection, dateless-row and prose exemption, line-number reporting), the TESTING.md tests breakdown (parts summing to the collected total, a self-consistent-but-stale row, and the reworded-row error), and vera/README.md's Test Suite counts (all four checked independently — mutation-validated by dropping each citation in turn — plus the reworded-paragraph error, a thousands-separator case pinning that every one of the four counts is read comma-tolerantly, and the two section-anchoring cases — a reworded paragraph with decoy counts in a later section, and a renamed heading, both of which must fail loud rather than match across the section boundary). The reworded case is a test in its own right for both new checks: a pattern that matches nothing must be an error, or rewording the sentence silently switches the gate off. Also the release count (README's status line and HISTORY's total against each other and against git tag: the matching case, the one-ahead release cut that release.yml has not tagged yet, that +1 being the ONLY slack once the version is tagged, the two-behind drift that actually shipped, per-document reporting, and a tagless checkout standing the oracle down without standing down the cross-check), plus the tag reader itself against real repositories built in tmp_path — release tags read, nightly/-rc1 not counted as releases, and both no-evidence answers (None rather than [], since an empty list would read as zero releases and make every documented count wrong) for a tagless checkout and a directory that is not a repository at all. CONTRIBUTING.md's pre-commit hook count is checked the same way, reworded-sentence case included; and the CI-pipeline lint row against ci.yml's lint job — a matching row, a step present in CI but absent from the row (the drift that shipped), a row entry CI no longer runs, the same set in a different order, a reworded row and a renamed job (both errors, not skips), that only the lint job is read rather than the whole workflow, and the shipped pair both clean and red with one entry dropped). Also check_faq_example_count (#1346), which reads FAQ.md's by-the-numbers example bullet: the page's conformance bullet was pinned first and its test bullet only after that one had drifted through two releases, so the example bullet is pinned rather than left as the third instance of one lesson. Its cells are all about ANCHORING, because an unanchored search reads whichever occurrence comes first and reports the page consistent while the bullet itself is stale — a decoy phrase carrying the right count in prose above the list, a duplicate bullet (two answers, and the check cannot say which one a reader believes), an inline mention, and an indented sub-bullet; each reddens if the anchor is dropped, and a reworded bullet is an error rather than a skip for the same reason as the checks above
test_grammar_alignment.py	91	753	check_grammar_alignment.py gate (#683): both extractors (Lark headers with the ?/!/_ markers stripped, template parameters and rule priorities tolerated, and -> alias names deliberately not collected; spec headers from ```ebnf fences only), the allowlist arithmetic in all three directions — unwaived drift, a spent entry both files now have, and an entry whose premise broke — one case per waiver proving the fact it rests on is actually checked, the name-deleted-from-both-files case that must not read as agreement, a mutation restoring the spec's old assert_stmt name, non-vacuous extraction, and the false positive the issue itself rested on: qualified_call and module_call are spec headers Lark expresses as aliases, and must never be reported as drift. Three pin the premise checks against ways they used to pass vacuously: an alias surviving only inside a // comment must not hold its waiver up, an alias that moved to another rule must fail the waiver naming fn_call, and a spent waiver whose premise also broke must yield one instruction rather than two opposite ones
test_check_examples_run.py	79	1,315	check_examples_run.py, the harness gate that RUNS the examples. Five separable parts, each in both directions. The coverage rule — the shipped tables cover the shipped corpus exactly, and an unclassified example, a stale RUN_SPECS or SKIPS key whose file is gone, a name in both tables, and a skip citing an undocumented property are each an error; the empty corpus is an error too, since a glob that stops matching would otherwise report success over zero programs. Plus the specs' own well-formedness: every named entry point is public in its example, every no-main example pins one (or vera run would fall back to an arbitrary first export), and no skip property is unused. The runner — a seeded tmp_path corpus proves it goes red on a program that type-checks and compiles but traps at run time, green on one that does not, and reports only the broken member of a mixed pair; a fixture whose first export is clean and whose named one traps proves spec.fn is actually honoured rather than ignored; a writer program proves each run gets a scratch working directory, so a gate run leaves nothing beside the examples. The TESTING.md cross-check — missing row, extra row, rename (reported naming both sides), wrong disposition and wrong skip property are errors, the parse stops at the next heading so a row-shaped line in a later section is not swept in, and both a reworded heading and a heading whose table has vanished fail loud rather than finding nothing to compare. The output signal -- the second half of the two-signal discipline check_examples.py established: the fallback note that vera run prints when it cannot use the named entry point is a failure even at exit 0, an absent expect sentinel is a failure even at exit 0, and a spec without one asserts nothing about output; end to end, a privatised main and a program that completed down a graceful arm each go red, and the same program passes once its own output is the sentinel, so the check reads the output rather than always failing. Which specs must carry a sentinel is derived from what each example declares — a resource effect in a function's effect row, or a call to a resource operation, both validated against the live effect registry so a renamed effect or op fails loudly — and asserted equal to the specs that have one, in both directions; the previous hard-coded triple could not see a fourth such example arriving without one. The runner's use of BOTH streams is pinned structurally -- vera run writes the note to stderr and nothing there on a clean exit, so no fixture can distinguish reading both streams from reading stdout alone, and a tripwire wired to the wrong stream is no tripwire. Also the hermetic-environment property: an ambient VERA_DB_URL or provider key is stripped so a gate run cannot be pointed at a real database or turned into a billed API call, a fixture spec puts its own URL back, and every neutralised name is checked to be one vera/runtime/ actually reads
test_check_corpus_differential.py	52	895	check_corpus_differential.py, the burndown instrument that compiles the corpus at two revisions. The pure pieces only — the real two-revision run costs minutes and is not a test. Classification, all four verdicts: identical, WAT differs, and each one-sided compile failure as its own kind, since a compilability reversal reported as a text difference is the mis-description the instrument exists to avoid; failing at both revisions is not a mover and is counted separately, so a green run states how much of it was vacuous. Enumeration — recursive, keyed by repo-relative POSIX path, and an empty corpus is an error rather than a clean run over nothing. The canary — each side must import the compiler it was pointed at, so a side silently resolving to the venv's editable install cannot compare a revision against itself; an import failure and a foreign compiler are different messages. Reporting — every mover named with its reason, the exit code, the --json shape, and a program missing from one side reported rather than dropped. One test asserts the instrument is absent from .pre-commit-config.yaml, so the docstring's claim cannot rot
test_check_editor_grammars.py	20	249	check_editor_grammars.py gate (#1156): the registry read (every effect in, every ability out, and the four names the grammars actually drifted on present so the set checked is non-vacuous), the word-boundary presence test across all three grammar formats (JSON, plist XML, Vim keyword list) including the prefix pair Http/HttpServer in both directions, the deliberate comment-mention false pass, a metacharacter pair that only passes when the name is matched literally (A.B present, A0B not), and the empty registry; the gate's primary path end to end — a listed grammar with an effect stripped out, and a listed README with one stripped out of its prose bullet, each red against an otherwise-clean mirrored tree; the completeness guard — a grammar discovered under editors/ but absent from GRAMMARS fails that same tree, over three discovery routes (.el outside a syntax directory, a tree-sitter .scm query set, a .tmLanguage.json filed anywhere but syntaxes/); and the registry's provenance, run as a subprocess against a throwaway checkout whose vera package names an effect the grammars do not, which is the only way to see that the list comes from the tree being checked rather than from site-packages. The shipped grammars and READMEs are currently clean
test_check_explicit_encoding.py	54	254	check_explicit_encoding.py gate (#645): flags text-mode open() / read_text() / write_text() and subprocess.run/Popen/check_output(..., text=True) captures missing an encoding="utf-8" literal (rejects non-literal / non-UTF-8 values), skips binary/bytes-mode calls, honours the # encoding-exempt opt-out, and asserts the shipped repo is clean
test_check_limitations_sync.py	13	233	check_limitations_sync.py section extraction: table-rows-only issue harvesting, prose-link exemption, bounding at the next second-level heading, None for absent or sub-level headings so renamed sections fail loudly; plus the #852 fail-loud rule: an UNKNOWN issue state under --check-states (gh missing / auth failure / timeout) is an error, never a silent pass
test_doc_annotations.py	23	340	scripts/doc_annotations.py — the inline vera:skip-<stage> fence-annotation reader and shared run_parse_only_gate used by the doc-block gates (#538): markdown/HTML scanning (annotation attached to the following fence / <pre>, stacked directives), hard problems (malformed, dangling incl. EOF, duplicate-stage, unknown-stage, unterminated fence / unclosed <pre>; prose mentions without comment syntax are fine), the gate round-trip semantics via evaluate_block (unannotated failure fails, annotated failure skips, annotated PASS is a stale annotation, skip-check still runs parse first and stops the pipeline), unsupported-stage detection for parse-only gates, and strip_annotations (annotation lines removed, other HTML comments survive)
test_doc_builtin_shadowing.py	8	107	check_doc_builtin_shadowing.py gate (#819): reject-set membership (opaque built-ins in, overridable combinators out), top-level + where-block fn <builtin> definitions flagged, non-built-in / overridable / prose-mention ignored, and the shipped docs are currently clean
test_runtime_traps.py	98	3,255	Runtime trap categorisation (#516 Stage 1), out-of-bounds host-read bounds check (#1145), stdout/stderr-on-trap preservation (#522), IO.print live tee (#543), and trap source backtrace (#516 Stage 2): _classify_trap per-kind mapping (divide_by_zero/out_of_bounds/stack_exhausted/unreachable/overflow/contract_violation/unknown), plus host_error from _classify_host_error on execute()'s non-Trap branch, WasmTrapError shape + RuntimeError substitutability, end-to-end cmd_run text + JSON envelopes including trap_kind, captured stdout, captured stderr, JSON-mode "no stderr leak" invariant, cross-stream code-order regression using merged redirect_stdout/redirect_stderr, the v0.0.123 tee suite (live streaming, write-count + order preservation, JSON-mode tee suppression, trap preservation invariant under tee, per-write flush count, default-execute silence), and the v0.0.124 source-mapping suite — _resolve_trap_frames unit tests covering user-fn / built-in / built-in-prefix / monomorphized base-name fallback / unknown-name / no-frames-attribute / leaf-first ordering preservation; end-to-end cmd_run text-mode + JSON-mode backtrace including the leaf-first ordering invariant; contract-violation backtrace in both text and JSON modes; direct execute() WasmTrapError.frames attachment; suppression marker for collapsed leading runtime-helper frames (mocked vera.codegen.execute with synthetic is_builtin=True leaf frames so the collapse logic is testable deterministically); source-map population for top-level fns + lifted closures (with span-value assertion against the closure literal's exact line range); and the no-builtin-leakage regression that pins built-in helpers (alloc / gc_collect / contract_fail) NOT being registered in fn_source_map; plus the v0.0.125 Stage 3 suite (#547) — text-mode Fix: block surfacing with position-ordering invariant (Fix appears after the source backtrace), text-mode block suppression for contract_violation (no empty header noise), JSON-mode fix field always-present (schema stability) including the empty-string case, _TRAP_FIX_PARAGRAPHS table-completeness assertion (every kind in the taxonomy has a Fix paragraph entry), and the column-wrap invariant (~76 chars max per line, two-space indent under the Fix: heading); plus the UTF-8 hardening suite TestHostPrintInvalidUtf8589 (#589 / #592) — after #592 centralised the errors="replace" invariant into the single vera.runtime.text.safe_utf8_decode helper — reached only through a shared _slice_and_decode helper (vera/runtime/heap.py) that the three WASM-memory string readers (_read_wasm_string and _read_string_export there, and vera/wasm/markdown.py::_read_string) delegate to, with the host_print / host_stderr / host_contract_fail host imports and the String-return extractor in execute() routing through those readers rather than decoding inline: one helper unit test pinning the invariant once (invalid bytes → U+FFFD, valid + empty pass through), three wire-real end-to-end tests that drive the production readers (_read_wasm_string / markdown _read_string behind a synthetic-WAT probe host import; _read_string_export against a real exported memory, also covering its out-of-bounds → None pointer-fallback) over a region seeded with invalid UTF-8 — so a strict-decode regression surfaces as a UnicodeDecodeError escaping wasmtime's trampoline, and the host imports / extractor are transitively covered — and one synthetic-WAT end-to-end test that imports vera.print and calls it with raw invalid UTF-8 bytes to pin the wasmtime-trampoline fact independently (a Python UnicodeDecodeError inside a host import escapes as a "python exception" cause iff the host decode is strict); the six pre-#592 structural source-grep assertions were retired by the centralisation; plus the Ctrl-C-during-host-import suite TestHostSleepKeyboardInterrupt (#595 / #599) — after the v0.0.160 relocation to a single except KeyboardInterrupt handler in execute() (enabled by wasmtime>=45.0.0's except BaseException trampoline fix): one structural assertion that the four per-host-import raise _VeraExit(130) guards are gone and the centralized handler maps to exit_code=130, plus four end-to-end tests that compile real Vera programs calling IO.sleep(...), IO.read_char(()), a mocked fused await (#841 — Future.result() patched to interrupt), and a live in-flight fused await (no mocking — _thread.interrupt_main() fired only once the server confirms the request arrived, handler then released so the executor teardown has a real worker to wait out; post-#848 the progress print precedes the async(...), so program order makes its stdout assertion deterministic), raise KeyboardInterrupt from inside the blocking call, and assert the program exits with ExecuteResult.exit_code == 130 (pre-interrupt stdout preserved) instead of a raw Python traceback escaping wasmtime's trampoline; plus the host-callback surface suite TestHostCallbackErrorSurface1302 / TestClassifyHostError1302 (#1302) — execute() classified on the exception's TYPE NAME (Trap / WasmtimeError), so a host import raising an ordinary Python exception skipped the conversion and escaped as a 63-line interpreter traceback with the captured streams dropped, and in --json mode with no envelope emitted at all. The conversion is now keyed on the BOUNDARY (everything escaping the guest invocation), and the suite drives a real json_stringify(JNumber(nan())) program through all three surfaces: execute() raising a WasmTrapError of kind="host_error" carrying the host's sentence, the pre-failure stdout and the original exception as __cause__; text-mode cmd_run asserted on the ABSENCE of Traceback / File " / wasmtime and a sub-ten-line diagnostic, since asserting only that the sentence appears would still pass on the pre-fix output where it was the traceback's last line; and JSON-mode cmd_run producing a parseable envelope with trap_kind, an always-present empty fix, frames, and the captured stdout. TestHostErrorDebugKnob1302 covers the escape hatch the conversion needs — VERA_DEBUG_HOST_ERRORS (ENVIRONMENT.md) re-raises the original exception so a binding bug stays diagnosable — as a deliberate pair, one test proving the knob does something and one proving its absence is what produces the one-liner, since neither alone distinguishes a working knob from unconditional behaviour, plus the truthiness table shared with VERA_EAGER_GC and an end-to-end cmd_run case
test_serve.py	8	189	#305 vera serve driver end-to-end: GET/POST echo round-trips (method/path/headers/body cross the host↔guest boundary via build_request_adt / decode_response_adt), handler status propagation, runtime contract violation → 500 with trap_kind JSON, State<Int> isolation across requests (instance-per-request pinned), and clean make_server validation errors (missing / wrong-signature handle), and an eager-GC round-trip pinning the Request builder's shadow-rooting; all on ephemeral ports
test_wasi_target.py	275	2,142	#237 WASI Preview 2 target (spec chapter 13): component emission validated live against the real wasmtime host — parse (Component(engine, wat)), instantiate (Linker.add_wasip2() + WasiConfig), and execute (stdout/stderr capture, env, argv incl. a 500-arg GC-pressure stress and a >64 KiB arena-cap trap, preopen file round-trips + errno mapping, stdin incl. UTF-8 multibyte, clocks, random bounds, exit, contract-violation text on WASI stderr, overflow); the family gate (clean diagnostic naming unsupported families, never a silent fallback); the core-emission pin (default --target wasm WAT untouched); cmd_compile/cmd_run --target wasi-p2 CLI integration (binary component artifact, --wat component text, JSON envelopes, trap-kind classification through the component boundary, exit-code 0/1 degradation, --fn rejection); the execute_wasi_p2 host runner (env passthrough, argv, stderr capture, String-main wasi:cli/run fallback); the dual-target conformance differential (all 174 run-level conformance programs driven under both targets, byte-identical stdout/stderr required — 122 are dual-tested and 52 skip loudly rather than passing silently: 45 whose compiled WAT imports a host family outside IO/Random (state, map, json, set, decimal, html, md, regex, db), 6 with no public zero-argument main, and 1 calling a nondeterministic op. The excluded set is defined by those three properties rather than by a filename list, so it stays accurate as programs are added); a stock-wasmtime-CLI smoke test (skips when the CLI is not installed); and the Stage-D server world (world="server"): incoming-handler emission pins (adapter lift, 32-slot dispatch table, @0.2.0 version pin, no wasi:cli/run), #305 handler validation + server family-gate diagnostics (rejected IO ops, non-String map instantiations, unsupported families), the cli-world pin (default emission carries no server machinery), Request/Response layout tripwires, and a stock-wasmtime serve smoke battery (host-vs-served differential over a method/path/header/body matrix incl. duplicate-header later-wins, in-guest map-op order parity, IO.print console routing, trap→500 with symbolized backtrace + violation text, graceful 500s for forbidden headers and out-of-range status, a 1 MiB GC-stress echo, and an eager-GC shadow-push mutation validation; skips when the CLI is not installed)

Conformance Suite

The conformance suite is a collection of 244 small, focused programs in tests/conformance/ that systematically validate every language feature against the spec. Most programs are self-contained; the module-focused Chapter 8 cases use import statements where needed, and ch07_cross_module_contracts.vera still depends on ch07_cross_module_contracts_lib.vera. Each program tests one feature or a small group of related features.

Simon Willison argues that conformance suites are a "huge unlock" for language projects — they transform development from trust-based to verification-based. The conformance suite serves as the definitive specification artifact that any implementation (or agent) can validate against.

Three-layer testing model

Vera has three distinct test layers, each serving a different purpose:

Layer	Location	Purpose	What it tests
Unit tests	tests/test_*.py	Test compiler internals	Error paths, edge cases, internal APIs
Conformance suite	tests/conformance/	Spec-anchored feature validation	Every language feature, one program per feature
Example programs	examples/	Showcase programs and demos	End-to-end usage, documentation

Unit tests verify that the compiler works correctly. Conformance programs verify that the language works correctly. Examples demonstrate how to use the language. All three run in CI and pre-commit hooks.

Test levels

Each conformance program declares the deepest pipeline stage it must pass:

Level	What it validates	Count
parse	Source text is syntactically valid	0
check	Parses and type-checks cleanly	50
verify	Type-checks and all contracts verified by Z3	20
run	Compiles to WASM and executes correctly	174

Almost all programs are at the run level — they compile and execute, producing correct results. Fifty programs (ch02_generic_over_unit_rejected, ch02_map_unit_value_rejected, ch03_typed_holes, ch04_let_unit_rejected, ch05_apply_fn_arity, ch05_decreases_float_rejected, ch05_reserved_fn_name_rejected, ch05_reserved_keyword_fn_rejected, ch05_reserved_contextual_keyword_fn_rejected, ch05_reserved_resume_fn_rejected, ch05_where_helper_outer_slot_rejected, ch07_cross_module_contracts_lib, ch07_handler_state_body_scope_rejected, ch07_old_outside_ensures_rejected, ch07_state_unit_op_param_read_rejected, ch07_bare_effect_op_rejected, ch08_ambiguous_import_adt_lib_bool, ch08_ambiguous_import_adt_lib_int, ch08_ambiguous_import_adt_rejected, ch08_ambiguous_import_adt_swapped_rejected, ch08_ambiguous_import_lib_bool, ch08_ambiguous_import_lib_int, ch08_ambiguous_import_rejected, ch08_ambiguous_import_swapped_rejected, ch08_circular_import, ch08_cross_module_generic_lib, ch08_module_generic_diamond_base, ch08_module_prelude_adt_contention_rejected, ch08_reserved_vera_prefix_rejected, ch08_reserved_vera_prefix_reference_rejected, ch08_reserved_vera_prefix_binder_rejected, ch08_reserved_vera_prefix_effect_rejected, ch08_reserved_vera_prefix_ability_rejected, ch08_reserved_vera_prefix_constructor_rejected, ch08_transitive_module_import_base, ch08_visibility_private, ch08_xmod_widen_lib, ch09_builtin_effect_redefinition_rejected, ch09_builtin_redefinition, ch09_eq_non_derivable_rejected, ch09_http, ch09_inference, ch09_ord_adt_rejected, ch09_sql_injection_rejected, ch09_sql_placeholder_mismatch_rejected, ch09_sql_placeholder_let_mismatch_rejected, ch09_sql_numbered_placeholder_rejected, ch06_quantifier_array_domain_rejected, ch07_handler_state_type_mismatch_rejected, ch02_alias_cycle_rejected) are at the check level. Thirty-seven of them — 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_reserved_contextual_keyword_fn_rejected, ch05_reserved_resume_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, ch07_bare_effect_op_rejected, ch08_ambiguous_import_adt_rejected, ch08_ambiguous_import_adt_swapped_rejected, ch08_ambiguous_import_rejected, ch08_ambiguous_import_swapped_rejected, ch08_circular_import, ch08_reserved_vera_prefix_rejected, ch08_reserved_vera_prefix_reference_rejected, ch08_reserved_vera_prefix_binder_rejected, ch08_reserved_vera_prefix_effect_rejected, ch08_reserved_vera_prefix_ability_rejected, ch08_reserved_vera_prefix_constructor_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, ch06_quantifier_array_domain_rejected, ch07_handler_state_type_mismatch_rejected, and ch02_alias_cycle_rejected — are negative tests that assert a specific diagnostic (E206, E135, E183, E201, E127, E153, E153, E153, E153, E130, E130, E174, E182, E217, E156, E156, E155, E155, E011, E154, E154, E154, E154, E154, E154, E150, E152, E151, E242, E243, E207, E208, E208, E209, E128, E336, and E132 respectively) via the manifest's expected_error field. One more — ch08_module_prelude_adt_contention_rejected — is a negative at the compile stage rather than at check: it carries expected_error_stage: "compile" beside expected_error: E621, so the harness asserts it type-checks CLEANLY and is then refused by vera compile with that code, which is the property a codegen-phase diagnostic exists for. ch09_http and ch09_inference are environment-gated (network / API key). Twenty programs (ch03_slot_let_chains, ch03_slot_noncommutative, ch04_nested_option_ctor, ch04_primitive_obligations, ch05_apply_fn_typing, ch06_adt_sort_disambiguation, ch07_cross_module_contracts, ch07_invisible_import_op_name_lib, ch07_io_read_char, ch07_io_sleep, ch07_random_effect, ch08_state_alias_module_table_lib, ch08_module_generic_diamond_mid1, ch08_module_generic_diamond_mid2, ch08_state_alias_per_module_lib, ch08_transitive_module_import_mid, ch09_http_server, ch09_invisible_import_ability_op_lib, ch09_math_builtins, ch09_nested_helper_family_op_name_lib) are at the verify level, using Z3-provable contracts — a library module is pinned at the deepest level it reaches, so the two per-module alias-table libraries are verified rather than only checked.

Skipped tests

pytest tests/ -v skips 120 conformance-stage tests, and every one of them is the level rule: a program declared at check skips its verify and run stages, one declared at verify skips its run — 50 × 2 + 20, which is what the suite reports. The two tables below split those 120 by why the program sits at its level, not by how it skipped: 116 are pinned there by the feature under test, and 4 by an environment CI does not have. Each skip is listed once; the tables do not overlap. (The suite's remaining skips are platform- or tool-gated and documented beside the tests that declare them.)

Level-limited skips — the conformance framework only runs tests up to the declared level; stages beyond that level are automatically skipped. These are expected and correct.

Test	Program	Declared level	Skipped stage	Reason
test_verify[ch02_alias_cycle_rejected]	ch02_alias_cycle_rejected.vera	check	verify	check-level negative test (expected_error: E132): verify stage not run
test_run[ch02_alias_cycle_rejected]	ch02_alias_cycle_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch02_generic_over_unit_rejected]	ch02_generic_over_unit_rejected.vera	check	verify	check-level negative test (expected_error: E206): verify stage not run
test_run[ch02_generic_over_unit_rejected]	ch02_generic_over_unit_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch02_map_unit_value_rejected]	ch02_map_unit_value_rejected.vera	check	verify	check-level negative test (expected_error: E135): verify stage not run
test_run[ch02_map_unit_value_rejected]	ch02_map_unit_value_rejected.vera	check	run	check-level negative test: no run stage
test_run[ch03_slot_let_chains]	ch03_slot_let_chains.vera	verify	run	verify-level programs don't get a run test
test_run[ch03_slot_noncommutative]	ch03_slot_noncommutative.vera	verify	run	verify-level programs don't get a run test
test_run[ch07_invisible_import_op_name_lib]	ch07_invisible_import_op_name_lib.vera	verify	run	verify-level programs don't get a run test
test_run[ch08_module_generic_diamond_mid1]	ch08_module_generic_diamond_mid1.vera	verify	run	verify-level programs don't get a run test
test_run[ch08_module_generic_diamond_mid2]	ch08_module_generic_diamond_mid2.vera	verify	run	verify-level programs don't get a run test
test_run[ch09_invisible_import_ability_op_lib]	ch09_invisible_import_ability_op_lib.vera	verify	run	verify-level programs don't get a run test
test_run[ch09_nested_helper_family_op_name_lib]	ch09_nested_helper_family_op_name_lib.vera	verify	run	verify-level programs don't get a run test
test_verify[ch03_typed_holes]	ch03_typed_holes.vera	check	verify	check-level program: verify stage not run
test_run[ch03_typed_holes]	ch03_typed_holes.vera	check	run	check-level program: no standalone main
test_verify[ch04_let_unit_rejected]	ch04_let_unit_rejected.vera	check	verify	check-level negative test (expected_error: E183): verify stage not run
test_run[ch04_let_unit_rejected]	ch04_let_unit_rejected.vera	check	run	check-level negative test: no run stage
test_run[ch04_nested_option_ctor]	ch04_nested_option_ctor.vera	verify	run	verify-level programs don't get a run test
test_run[ch04_primitive_obligations]	ch04_primitive_obligations.vera	verify	run	verify-level programs don't get a run test
test_verify[ch05_apply_fn_arity]	ch05_apply_fn_arity.vera	check	verify	check-level negative test (expected_error: E201): verify stage not run
test_run[ch05_apply_fn_arity]	ch05_apply_fn_arity.vera	check	run	check-level negative test: no run stage
test_run[ch05_apply_fn_typing]	ch05_apply_fn_typing.vera	verify	run	verify-level programs don't get a run test
test_verify[ch05_decreases_float_rejected]	ch05_decreases_float_rejected.vera	check	verify	check-level negative test (expected_error: E127): verify stage not run
test_run[ch05_decreases_float_rejected]	ch05_decreases_float_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch05_reserved_fn_name_rejected]	ch05_reserved_fn_name_rejected.vera	check	verify	check-level negative test (expected_error: E153): verify stage not run
test_run[ch05_reserved_fn_name_rejected]	ch05_reserved_fn_name_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch05_reserved_keyword_fn_rejected]	ch05_reserved_keyword_fn_rejected.vera	check	verify	check-level negative test (expected_error: E153): verify stage not run
test_run[ch05_reserved_keyword_fn_rejected]	ch05_reserved_keyword_fn_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch05_reserved_contextual_keyword_fn_rejected]	ch05_reserved_contextual_keyword_fn_rejected.vera	check	verify	check-level negative test (expected_error: E153): verify stage not run
test_run[ch05_reserved_contextual_keyword_fn_rejected]	ch05_reserved_contextual_keyword_fn_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch05_reserved_resume_fn_rejected]	ch05_reserved_resume_fn_rejected.vera	check	verify	check-level negative test (expected_error: E153): verify stage not run
test_run[ch05_reserved_resume_fn_rejected]	ch05_reserved_resume_fn_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch05_where_helper_outer_slot_rejected]	ch05_where_helper_outer_slot_rejected.vera	check	verify	check-level negative test (expected_error: E130): verify stage not run
test_run[ch05_where_helper_outer_slot_rejected]	ch05_where_helper_outer_slot_rejected.vera	check	run	check-level negative test: no run stage
test_run[ch06_adt_sort_disambiguation]	ch06_adt_sort_disambiguation.vera	verify	run	verify-level programs don't get a run test
test_run[ch07_cross_module_contracts]	ch07_cross_module_contracts.vera	verify	run	verify-level programs don't get a run test
test_verify[ch07_cross_module_contracts_lib]	ch07_cross_module_contracts_lib.vera	check	verify	check-level library module: verify stage not run
test_run[ch07_cross_module_contracts_lib]	ch07_cross_module_contracts_lib.vera	check	run	check-level library module: no standalone main
test_verify[ch07_handler_state_body_scope_rejected]	ch07_handler_state_body_scope_rejected.vera	check	verify	check-level negative test (expected_error: E130): verify stage not run
test_run[ch07_handler_state_body_scope_rejected]	ch07_handler_state_body_scope_rejected.vera	check	run	check-level negative test: no run stage
test_run[ch07_io_read_char]	ch07_io_read_char.vera	verify	run	verify-level programs don't get a run test
test_run[ch07_io_sleep]	ch07_io_sleep.vera	verify	run	verify-level programs don't get a run test
test_verify[ch07_old_outside_ensures_rejected]	ch07_old_outside_ensures_rejected.vera	check	verify	check-level negative test (expected_error: E174): verify stage not run
test_run[ch07_old_outside_ensures_rejected]	ch07_old_outside_ensures_rejected.vera	check	run	check-level negative test: no run stage
test_run[ch07_random_effect]	ch07_random_effect.vera	verify	run	verify-level programs don't get a run test
test_verify[ch07_state_unit_op_param_read_rejected]	ch07_state_unit_op_param_read_rejected.vera	check	verify	check-level negative test (expected_error: E182): verify stage not run
test_run[ch07_state_unit_op_param_read_rejected]	ch07_state_unit_op_param_read_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch07_bare_effect_op_rejected]	ch07_bare_effect_op_rejected.vera	check	verify	check-level negative test (expected_error: E217): verify stage not run
test_run[ch07_bare_effect_op_rejected]	ch07_bare_effect_op_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch06_quantifier_array_domain_rejected]	ch06_quantifier_array_domain_rejected.vera	check	verify	check-level negative test (expected_error: E128): verify stage not run
test_run[ch06_quantifier_array_domain_rejected]	ch06_quantifier_array_domain_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch07_handler_state_type_mismatch_rejected]	ch07_handler_state_type_mismatch_rejected.vera	check	verify	check-level negative test (expected_error: E336): verify stage not run
test_run[ch07_handler_state_type_mismatch_rejected]	ch07_handler_state_type_mismatch_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch08_circular_import]	ch08_circular_import.vera	check	verify	check-level negative test (expected_error: E011): verify stage not run
test_run[ch08_circular_import]	ch08_circular_import.vera	check	run	check-level negative test: no run stage
test_verify[ch08_module_prelude_adt_contention_rejected]	ch08_module_prelude_adt_contention_rejected.vera	check	verify	compile-stage negative test (expected_error: E621, expected_error_stage: compile): verify stage not run
test_run[ch08_module_prelude_adt_contention_rejected]	ch08_module_prelude_adt_contention_rejected.vera	check	run	compile-stage negative test: no run stage
test_verify[ch08_reserved_vera_prefix_rejected]	ch08_reserved_vera_prefix_rejected.vera	check	verify	check-level negative test (expected_error: E154): verify stage not run
test_run[ch08_reserved_vera_prefix_rejected]	ch08_reserved_vera_prefix_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch08_reserved_vera_prefix_reference_rejected]	ch08_reserved_vera_prefix_reference_rejected.vera	check	verify	check-level negative test (expected_error: E154): verify stage not run
test_run[ch08_reserved_vera_prefix_reference_rejected]	ch08_reserved_vera_prefix_reference_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch08_reserved_vera_prefix_binder_rejected]	ch08_reserved_vera_prefix_binder_rejected.vera	check	verify	check-level negative test (expected_error: E154): verify stage not run
test_run[ch08_reserved_vera_prefix_binder_rejected]	ch08_reserved_vera_prefix_binder_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch08_reserved_vera_prefix_effect_rejected]	ch08_reserved_vera_prefix_effect_rejected.vera	check	verify	check-level negative test (expected_error: E154): verify stage not run
test_run[ch08_reserved_vera_prefix_effect_rejected]	ch08_reserved_vera_prefix_effect_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch08_reserved_vera_prefix_ability_rejected]	ch08_reserved_vera_prefix_ability_rejected.vera	check	verify	check-level negative test (expected_error: E154): verify stage not run
test_run[ch08_reserved_vera_prefix_ability_rejected]	ch08_reserved_vera_prefix_ability_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch08_reserved_vera_prefix_constructor_rejected]	ch08_reserved_vera_prefix_constructor_rejected.vera	check	verify	check-level negative test (expected_error: E154): verify stage not run
test_run[ch08_reserved_vera_prefix_constructor_rejected]	ch08_reserved_vera_prefix_constructor_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch08_ambiguous_import_rejected]	ch08_ambiguous_import_rejected.vera	check	verify	check-level negative test (expected_error: E155): verify stage not run
test_run[ch08_ambiguous_import_rejected]	ch08_ambiguous_import_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch08_ambiguous_import_swapped_rejected]	ch08_ambiguous_import_swapped_rejected.vera	check	verify	check-level negative test (expected_error: E155): verify stage not run
test_run[ch08_ambiguous_import_swapped_rejected]	ch08_ambiguous_import_swapped_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch08_ambiguous_import_adt_lib_int]	ch08_ambiguous_import_adt_lib_int.vera	check	verify	check-level library module: verify stage not run
test_run[ch08_ambiguous_import_adt_lib_int]	ch08_ambiguous_import_adt_lib_int.vera	check	run	check-level library module: no standalone main
test_verify[ch08_ambiguous_import_adt_lib_bool]	ch08_ambiguous_import_adt_lib_bool.vera	check	verify	check-level library module: verify stage not run
test_run[ch08_ambiguous_import_adt_lib_bool]	ch08_ambiguous_import_adt_lib_bool.vera	check	run	check-level library module: no standalone main
test_verify[ch08_ambiguous_import_adt_rejected]	ch08_ambiguous_import_adt_rejected.vera	check	verify	check-level negative test (expected_error: E156): verify stage not run
test_run[ch08_ambiguous_import_adt_rejected]	ch08_ambiguous_import_adt_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch08_ambiguous_import_adt_swapped_rejected]	ch08_ambiguous_import_adt_swapped_rejected.vera	check	verify	check-level negative test (expected_error: E156): verify stage not run
test_run[ch08_ambiguous_import_adt_swapped_rejected]	ch08_ambiguous_import_adt_swapped_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch08_ambiguous_import_lib_int]	ch08_ambiguous_import_lib_int.vera	check	verify	check-level library module: verify stage not run
test_run[ch08_ambiguous_import_lib_int]	ch08_ambiguous_import_lib_int.vera	check	run	check-level library module: no standalone main
test_verify[ch08_ambiguous_import_lib_bool]	ch08_ambiguous_import_lib_bool.vera	check	verify	check-level library module: verify stage not run
test_run[ch08_ambiguous_import_lib_bool]	ch08_ambiguous_import_lib_bool.vera	check	run	check-level library module: no standalone main
test_verify[ch08_cross_module_generic_lib]	ch08_cross_module_generic_lib.vera	check	verify	check-level library module: verify stage not run
test_run[ch08_cross_module_generic_lib]	ch08_cross_module_generic_lib.vera	check	run	check-level library module: no standalone main
test_verify[ch08_module_generic_diamond_base]	ch08_module_generic_diamond_base.vera	check	verify	check-level library module: verify stage not run
test_run[ch08_module_generic_diamond_base]	ch08_module_generic_diamond_base.vera	check	run	check-level library module: no standalone main
test_run[ch08_state_alias_module_table_lib]	ch08_state_alias_module_table_lib.vera	verify	run	verify-level programs don't get a run test
test_run[ch08_state_alias_per_module_lib]	ch08_state_alias_per_module_lib.vera	verify	run	verify-level programs don't get a run test
test_verify[ch08_transitive_module_import_base]	ch08_transitive_module_import_base.vera	check	verify	check-level library module: verify stage not run
test_run[ch08_transitive_module_import_base]	ch08_transitive_module_import_base.vera	check	run	check-level library module: no standalone main
test_run[ch08_transitive_module_import_mid]	ch08_transitive_module_import_mid.vera	verify	run	verify-level programs don't get a run test
test_verify[ch08_visibility_private]	ch08_visibility_private.vera	check	verify	check-level negative test (expected_error: E150): verify stage not run
test_run[ch08_visibility_private]	ch08_visibility_private.vera	check	run	check-level negative test: no run stage
test_verify[ch08_xmod_widen_lib]	ch08_xmod_widen_lib.vera	check	verify	check-level library module: verify stage not run
test_run[ch08_xmod_widen_lib]	ch08_xmod_widen_lib.vera	check	run	check-level library module: no standalone main
test_verify[ch09_builtin_effect_redefinition_rejected]	ch09_builtin_effect_redefinition_rejected.vera	check	verify	check-level negative test (expected_error: E152): verify stage not run
test_run[ch09_builtin_effect_redefinition_rejected]	ch09_builtin_effect_redefinition_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch09_builtin_redefinition]	ch09_builtin_redefinition.vera	check	verify	check-level negative test (expected_error: E151): verify stage not run
test_run[ch09_builtin_redefinition]	ch09_builtin_redefinition.vera	check	run	check-level negative test: no run stage
test_verify[ch09_eq_non_derivable_rejected]	ch09_eq_non_derivable_rejected.vera	check	verify	check-level negative test (expected_error: E243): verify stage not run
test_run[ch09_eq_non_derivable_rejected]	ch09_eq_non_derivable_rejected.vera	check	run	check-level negative test: no run stage
test_run[ch09_http_server]	ch09_http_server.vera	verify	run	verify-level programs don't get a run test
test_run[ch09_math_builtins]	ch09_math_builtins.vera	verify	run	verify-level programs don't get a run test
test_verify[ch09_ord_adt_rejected]	ch09_ord_adt_rejected.vera	check	verify	check-level negative test (expected_error: E242): verify stage not run
test_run[ch09_ord_adt_rejected]	ch09_ord_adt_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch09_sql_injection_rejected]	ch09_sql_injection_rejected.vera	check	verify	check-level negative test (expected_error: E207): verify stage not run
test_run[ch09_sql_injection_rejected]	ch09_sql_injection_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch09_sql_placeholder_mismatch_rejected]	ch09_sql_placeholder_mismatch_rejected.vera	check	verify	check-level negative test (expected_error: E208): verify stage not run
test_run[ch09_sql_placeholder_mismatch_rejected]	ch09_sql_placeholder_mismatch_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch09_sql_placeholder_let_mismatch_rejected]	ch09_sql_placeholder_let_mismatch_rejected.vera	check	verify	check-level negative test (expected_error: E208): verify stage not run
test_run[ch09_sql_placeholder_let_mismatch_rejected]	ch09_sql_placeholder_let_mismatch_rejected.vera	check	run	check-level negative test: no run stage
test_verify[ch09_sql_numbered_placeholder_rejected]	ch09_sql_numbered_placeholder_rejected.vera	check	verify	check-level negative test (expected_error: E209): verify stage not run
test_run[ch09_sql_numbered_placeholder_rejected]	ch09_sql_numbered_placeholder_rejected.vera	check	run	check-level negative test: no run stage

Environment-gated skips — these programs require network access or a live API key that is not available in CI. They pass vera check (type-checking) but cannot be executed.

Test	Program	Declared level	Skipped stage	Reason
test_verify[ch09_http]	ch09_http.vera	check	verify	Requires outbound HTTP; unavailable in CI sandbox
test_run[ch09_http]	ch09_http.vera	check	run	Requires outbound HTTP; unavailable in CI sandbox
test_verify[ch09_inference]	ch09_inference.vera	check	verify	Requires VERA_*_API_KEY; not set in CI
test_run[ch09_inference]	ch09_inference.vera	check	run	Requires VERA_*_API_KEY; not set in CI

To run the environment-gated tests locally: set VERA_ANTHROPIC_API_KEY (or another provider key) and ensure outbound HTTP is available, then vera run tests/conformance/ch09_http.vera / vera run tests/conformance/ch09_inference.vera.

Directory structure

tests/conformance/
├── manifest.json              # Machine-readable test metadata
├── ch01_int_literals.vera     # Chapter 1: Integer literals
├── ch01_float_literals.vera   # Chapter 1: Float64 literals
├── ch01_string_escapes.vera   # Chapter 1: String escape sequences
├── ...                        # 244 programs total, organized by spec chapter
├── ch07_state_handler.vera    # Chapter 7: State<T> effect handler
├── ch07_exn_handler.vera      # Chapter 7: Exn<E> effect handler
├── ch09_numeric_builtins.vera # Chapter 9: Numeric built-in functions
├── ch09_type_conversions.vera # Chapter 9: Numeric type conversions
├── ch09_markdown.vera         # Chapter 9: Markdown standard library
├── ch09_regex.vera            # Chapter 9: Regular expression matching
├── ch09_decimal.vera          # Chapter 9: Decimal type operations
├── ch09_json.vera             # Chapter 9: JSON standard library
├── ch09_http.vera             # Chapter 9: Http effect (check level)
└── ch09_float_predicates.vera # Chapter 9: Float64 predicates and constants

Manifest

manifest.json maps each program to its spec chapter, test level, and feature tags:

{
  "id": "ch04_arithmetic",
  "file": "ch04_arithmetic.vera",
  "chapter": 4,
  "title": "Arithmetic operators",
  "level": "run",
  "spec_ref": "Section 4.1",
  "features": ["add", "sub", "mul", "div", "mod", "unary_neg"]
}

The manifest is the machine-readable feature inventory — agents can query it to find which features exist and where they are tested.

Running the conformance suite

# Via pytest (parametrized — 1,220 tests: five stages × 244 entries)
pytest tests/test_conformance.py -v

# Via standalone script (used in CI and pre-commit)
python scripts/check_conformance.py

The pytest runner (test_conformance.py) parametrizes over every manifest entry and runs five checks per program: parse, check, verify, run, and format idempotency.

Adding a conformance test

1. Write a .vera program in tests/conformance/ following the naming convention chNN_feature_name.vera
2. Include a header comment indicating the spec chapter and what the program tests
3. Ensure the program has a main function (for run-level tests)
4. Format it: vera fmt --write tests/conformance/your_file.vera
5. Add an entry to manifest.json with the appropriate level and feature tags
6. Run python scripts/check_conformance.py to validate

When implementing a new language feature, the conformance program should be written first — this is test-driven development against the spec.

Compiler Code Coverage

Coverage by module, measured by pytest --cov=vera:

Module	Stmts	Miss	Coverage
wasm/	11,130	566	95%
codegen/	3,605	239	93%
checker/	1,223	68	94%
lsp/	492	52	89%
obligations/	188	1	99%
browser/	21	0	100%
verifier.py	702	31	96%
transform.py	617	24	96%
formatter.py	675	49	93%
ast.py	462	17	96%
smt.py	651	32	95%
markdown.py	413	54	87%
types.py	182	7	96%
errors.py	129	1	99%
environment.py	339	8	98%
cli.py	583	29	95%
parser.py	45	0	100%
resolver.py	68	2	97%
slots.py	41	5	88%
skip.py	12	3	75%
tester.py	389	3	99%
prelude.py	187	9	95%
registration.py	18	0	100%
__init__.py	2	0	100%
Total	22,174	1,200	95%

The lowest-coverage files of any size are vera/lsp/server.py at 64% (pygls feature-registration glue, exercised end-to-end by editors rather than by unit tests) and wasm/inference.py at 80% (deep type-dispatch branches for specific builtin return types).

Contract Verification Coverage

Vera's verifier classifies each contract into one of three tiers. Tier 1 contracts are proved correct statically by Z3; the non-trivial runtime check is still emitted as a defensive backstop (code generation is tier-agnostic — see spec §11.8), so a Tier-1 proof means the guard provably never fires, not that it is absent. Tier 3 contracts cannot be fully decided by the SMT solver, so their runtime check is the only line of defence. The verifier never rejects a valid program; it simply warns when a contract drops to Tier 3.

Across all 43 example programs (live sums of vera verify --json; regenerate by summing the verification block over examples/*.vera):

These totals are measured at the DEFAULT per-query Z3 budget of 10,000 ms, with VERA_Z3_TIMEOUT_MS unset and no --timeout-ms flag. The budget is part of the measurement, not a detail of it: an obligation whose proof lands near it is Tier 1 on a fast host and Tier 3 on a slow one, so a re-derived total that disagrees with the figures below should be checked against the budget before it is treated as drift (#1350).

Metric	Value
Tier 1 (static)	411 obligations — proved automatically by Z3
Tier 3 (runtime)	122 obligations — checked at runtime
Total	533 obligations (77.1% static; the summary's total field equals tier1_verified + tier3_runtime, derived from the reified obligation stream)

The Tier 3 population is dominated by a few built-in-heavy examples (life.vera 29, maximum_syntax.vera 11, collections.vera 10, array_utilities.vera 9, nested_closures.vera 7, string_utilities.vera 6), with a long tail of one to five per example across twenty more. The recurring reasons: postconditions over collection/string/HTML built-in pipelines outside the decidable fragment, decreases metrics the fragment cannot express, old/new state modelling (not yet implemented), and generic type parameters without a Z3 sort.

The Tier 1 fragment covers: integer/boolean arithmetic, comparisons, if/else, let bindings, match expressions, ADT constructors, function calls (modular postcondition), length, and decreases clauses (self-recursive, mutual recursion via where-blocks, Nat and structural ADT measures).

Language Feature Coverage

How Vera language features (by spec chapter) map to test files and example programs:

Spec chapter	Feature	Test files	Conformance	Examples
Ch 1: Lexical	Literals (Int, Float64, Bool, Byte, String)	test_ast, test_codegen_*	ch01_int_literals, ch01_float_literals, ch01_bool_literals, ch01_byte_literals	most examples
Ch 1: Lexical	String escape sequences (\n, \t, \\, \", \r, \0, \u{XXXX})	test_ast, test_codegen_*	ch01_string_escapes	io_operations, file_io
Ch 1: Lexical	Comments	test_parser	ch01_comments	—
Ch 2: Types	Int, Nat, Bool, String, Float64, Byte, Unit	test_codegen_, test_checker_	ch02_builtin_types	most examples
Ch 2: Types	ADTs (algebraic data types), Option, Result	test_codegen_, test_checker_	ch02_adt_basic, ch02_adt_recursive, ch02_option_result	pattern_matching, list_ops
Ch 2: Types	Refinement types	test_codegen_, test_verifier_	ch02_refinement_types	refinement_types, safe_divide
Ch 2: Types	Generics (forall<T>)	test_codegen_monomorphize, test_checker_*	ch02_generics	generics
Ch 3: Slots	@T.n references, De Bruijn indexing	test_checker_, test_codegen_	ch03_slot_basic, ch03_slot_indexing, ch03_slot_result	all 43 examples
Ch 4: Expressions	Arithmetic, comparison, boolean, unary ops	test_codegen_, test_checker_	ch04_arithmetic, ch04_comparison, ch04_boolean_ops, ch04_int_overflow	factorial, absolute_value
Ch 4: Expressions	If/else, let, match, pipe operator	test_codegen_, test_checker_	ch04_if_else, ch04_let_binding, ch04_match_basic, ch04_match_nested, ch04_pipe_operator	pattern_matching
Ch 4: Expressions	String and array builtins	test_codegen_*	ch04_string_builtins, ch04_array_ops	string_ops
Ch 5: Functions	Declarations, recursion, mutual recursion	test_codegen_, test_checker_	ch05_basic_function, ch05_recursion, ch05_mutual_recursion	factorial, mutual_recursion
Ch 5: Functions	Closures, higher-order functions	test_codegen_closures	ch05_closures	closures
Ch 5: Functions	Visibility (public/private)	test_checker_*	ch05_visibility	modules
Ch 6: Contracts	Preconditions (requires)	test_codegen_contracts, test_verifier_*	ch06_requires	safe_divide
Ch 6: Contracts	Postconditions (ensures)	test_codegen_contracts, test_verifier_*	ch06_ensures	absolute_value
Ch 6: Contracts	Decreases clauses, assert/assume	test_verifier_, test_codegen_	ch06_decreases, ch06_assert_assume	factorial
Ch 6: Contracts	Quantifiers (forall, exists)	test_codegen_, test_verifier_	ch06_quantifiers	quantifiers
Ch 7: Effects	Pure, IO, State<T>	test_codegen_, test_checker_	ch07_pure, ch07_io, ch07_state_handler	hello_world, increment, io_operations, file_io
Ch 7: Effects	Effect handlers (State<T>, Exn<E>)	test_codegen_, test_checker_	ch07_state_handler, ch07_exn_handler	effect_handler
Ch 9: Stdlib	Numeric builtins (abs, min, max, floor, ceil, round, sqrt, pow)	test_codegen_, test_checker_	ch09_numeric_builtins	—
Ch 9: Stdlib	Type conversions (int_to_float, float_to_int, nat_to_int, int_to_nat, byte_to_int, int_to_byte)	test_codegen_, test_checker_	ch09_type_conversions	—
Ch 9: Stdlib	Float64 predicates (float_is_nan, float_is_infinite, nan, infinity)	test_codegen_, test_checker_	ch09_float_predicates	—
Ch 7: Effects	Effect subtyping (§7.8), call-site checking	test_types, test_checker_*	—	—
Ch 2: Types	Bidirectional type checking (local inference)	test_checker_*	—	—
Ch 4: Expressions	Nested constructor patterns in match	test_codegen_*	ch04_match_nested	pattern_matching
Ch 8: Modules	Imports, cross-module typing and codegen	test_codegen_modules, test_resolver	—	modules
Ch 11: Compilation	Cross-module name collision detection (E608/E609/E610)	test_codegen_modules	—	—
Ch 9: Stdlib	Markdown (md_parse, md_render, md_has_heading, md_has_code_block, md_extract_code_blocks)	test_codegen_*, test_markdown	ch09_markdown	markdown
Ch 9: Stdlib	Regex (regex_match, regex_find, regex_find_all, regex_replace)	test_codegen_, test_checker_	ch09_regex	regex
Ch 9: Stdlib	Map, Set, Decimal collections	test_codegen_, test_checker_	ch09_map, ch09_set, ch09_decimal, ch09_decimal_generics	collections
Ch 9: Stdlib	Json (json_parse, json_stringify, json_get, json_array_get, json_array_length, json_keys, json_has_field, json_type)	test_codegen_, test_checker_	ch09_json	json
Ch 9: Stdlib	Html (html_parse, html_to_string, html_query, html_text, html_attr)	test_codegen_, test_checker_	ch09_html	html
Ch 9: Stdlib	Http effect (Http.get, Http.post)	test_codegen_, test_checker_	ch09_http	http
Ch 9: Stdlib	Async/Future<T> effect (async, await, #841 concurrency)	test_checker_effects, test_codegen_effects	ch09_async	—
Ch 7: Effects	HttpServer marker effect, vera serve (§7.7.5, #305)	test_serve, test_checker_effects	ch09_http_server	http_server
Ch 11: Compilation	Contract-driven testing (Z3 input gen + WASM execution)	test_tester, test_cli	—	safe_divide, factorial
Ch 12: Runtime	Browser runtime parity (JS host bindings match Python)	test_browser	—	—
Ch 13: WASI	WASI Preview 2 target (component emission, wasip2 host runner, dual-target differential); --world server wasi:http components (§13.7)	test_wasi_target	run-level suite via the dual-target differential	—

Test Helpers

Each test module defines its own module-level helper functions rather than sharing them through conftest.py, which carries only session-scoped fixtures — opt-in JS coverage, and the VERA_Z3_TIMEOUT_MS scrub that stops tier assertions inheriting an ambient solver budget, so the ones that do not name a budget of their own measure the default (#1350) — an explicit timeout_ms= outranks the environment and was never exposed. The three split suites are the exception: the test_checker_*.py files (split from test_checker.py, #420) import their shared helpers from tests/checker_helpers.py; the test_codegen_*.py feature files (split from test_codegen.py, #419) import theirs — plus the _IO_PRELUDE / _INLINE_BUILTIN_NAMES fixture constants — from tests/codegen_helpers.py; the two json_parse accept-domain batteries (#1306 / #1308) share their Vera probe program, its JSON-into-a-Vera-literal escaper, the OK: / ERR: output protocol and the two integer-overflow boundary constants through tests/json_domain_helpers.py, because a reference-host battery and a cross-host one only mean the same thing if they send json_parse the same bytes — one mutation of that escaper reddens both, which is the property a second copy would quietly lose; and the test_verifier_*.py theme files (split from test_verifier.py, #839) import theirs — plus the EXAMPLES_DIR / ALL_EXAMPLES corpus constants and the _MK source template — from tests/verifier_helpers.py.

tests/naming_helpers.py holds one fixture constructor rather than a suite's shared helpers: alias_env_from_declarations(decls, base=None) builds a vera.naming.AliasEnv by walking a parsed program's declarations. Every production consumer builds its environment from a namespace it already holds (the checker and the verifier from a live TypeEnv, codegen from its own flat alias maps), so this walk lives test-side, where it cannot become a second source of truth for declaration-index assignment.

tests/module_fixture_helpers.py cuts across all three suites: it builds the ResolvedModule fixtures the multi-module tests need, and its two functions are two different things rather than one with an option. What separates them is parse provenance, not whether a file survives the call — neither leaves one on disk, and neither file_path can be opened after it returns. resolved_module(path, source) writes the source to a real temporary file, parses THAT via parse_file, and deletes it before returning: the module keeps a program that came through the on-disk parse path, under a realistic absolute path. fake_resolved_module(path, source) parses in memory via parse_to_ast and labels the module /fake/<path>.vera — cheaper, and correct wherever the parse path does not matter; the label is conspicuously synthetic, so a path in a failure message is recognisable as a fixture's.

Deleting is safe because nothing downstream reopens file_path: compile() and the checker work off the parsed program and the in-memory source string and keep the path only as a diagnostic label (PR #664 review). A test that needs a module file to EXIST while it runs must write one itself. TestModuleFixtureBuilders in test_checker_modules.py pins all of that, including a cross-module type-check against an already-deleted path.

Both are the canonical implementation of the tempfile, encoding and path rules in Test Fixture Conventions below — six files carried their own copies before #1228, one of which leaked a temp file per fixture, and a new multi-module test should import from here rather than write a seventh.

# test_checker_*.py pattern (helpers from tests/checker_helpers.py):
_check_ok(source)              # assert no type errors
_check_err(source, "match")    # assert at least one error matching substring

# test_verifier_*.py pattern (helpers from tests/verifier_helpers.py):
_verify_ok(source)             # assert no verification errors
_verify_err(source, "match")   # assert at least one verification error
_verify_warn(source, "match")  # assert at least one warning

# test_codegen_*.py pattern (helpers from tests/codegen_helpers.py):
_compile_ok(source)            # assert compilation succeeds
_run(source, fn, args)         # compile + execute, return result
_run_io(source, fn, args)      # compile + execute, return captured stdout
_run_trap(source, fn, args)    # compile + execute, assert WASM trap

_compile() — and therefore every helper built on it — asserts the #1185 invariant on the emitted WAT: a module that contains a call_indirect must declare a function table. This is a differential over the two sides that have to agree (the instruction stream and the table section), so a future desync fails wherever it is introduced rather than at the next vera run. test_codegen_closures.py owns a local _compile and carries the same gate explicitly, being the densest closure / call_indirect coverage in the suite. Only that direction is universal: a table with no indirect call is inert and happens legitimately when a lift succeeds but the sole carrier is dropped for an unrelated reason. Fixtures where the table's presence is itself under test use _assert_call_indirect_iff_table for the biconditional.

Round-Trip Testing

Every one of the 43 example programs in examples/ is carried through the front of the pipeline by parametrised tests that glob the directory, so a new .vera example joins them the moment it lands: parsing (test_parser.py), AST transformation (test_ast.py), type checking (test_checker_functions.py), contract verification (test_verifier_contracts.py), and canonical form (test_formatter.py).

The back of the pipeline — compilation and execution — is not covered by a directory glob, and is described in full below.

The formatter has idempotency tests: format(format(x)) == format(x) for all tested programs.

Example execution coverage

An example that parses, type-checks, verifies and compiles can still trap the instant it runs. Six layers cover examples/, and only the last three execute anything:

Layer	Mechanism	Reach
Check + verify	scripts/check_examples.py	all 43
Canonical form, parse, transform, check, verify	the directory-globbing parametrised tests above	all 43
Compilation to WASM	scripts/check_e602_clean.py — it exists to police [E602]/[E604] silent skips, but it compiles every example with --json and treats an ok: false envelope as a hard failure, so full compile coverage is real though incidental to the script's name	all 43
Execution under both runtimes	tests/test_browser.py, from two explicit lists — EXAMPLES_WITH_MAIN (10, compared on stdout) and FUNCTION_CALL_EXAMPLES (11 distinct examples, compared on return value)	21
Execution with pinned output	dedicated tests, each asserting a specific value or rendering (see the table)	12
Execution asserted trap-free	scripts/check_examples_run.py — the harness gate	35

The gate is what makes the set closed. It enumerates examples/*.vera from disk and requires every name to be either run or matched to a documented skip property, so an unclassified example fails the gate and adding an example forces the author to classify it. The table below is cross-checked against the script's own tables on every run: a row that disagrees, a missing row, or a renamed example is an error, on the same principle as check_doc_counts.py — the codebase is the oracle and the documentation must match it.

What the gate asserts is runs green, deliberately not prints what it used to: output pinning stays in the dedicated tests, which is why sqlitedb.vera's rendered city table and inference_json.vera's score line are pinned there and only trap-freedom here.

Trap-freedom is two signals, not one — the discipline check_examples.py already applies, for the same reason. An exit code alone accepts two measured failures. Every spec names its entry point rather than relying on vera run's first-export fallback, because a main that is privatised or renamed otherwise runs some other function at exit 0. And the three examples that reach outside the process — sqlitedb.vera for its committed fixture, database.vera for an in-memory database, file_io.vera for the filesystem — answer a failure by printing a message and completing normally, so each pins a substring only its success path prints. Deleting examples/sqlitedb.sqlite fails the gate on that sentinel rather than passing on the graceful in-memory arm.

Example	Executed by	Harness gate
absolute_value.vera	browser parity (return value); test_codegen_infrastructure.py pins three results	runs
array_utilities.vera	nothing, before the gate	runs
async_futures.vera	browser parity (stdout)	runs
async_http_fanout.vera	nothing	skip: network
base64.vera	browser parity (stdout)	runs
closures.vera	browser parity (return value); test_codegen_closures.py pins 15 and 105	runs
collections.vera	nothing, before the gate	runs
database.vera	nothing, before the gate	runs
effect_handler.vera	browser parity (stdout + State round-trips); test_codegen_effects.py pins six results	runs
ephemeris.vera	test_examples_ephemeris.py pins the full stdout, both geocentric distances, agreement with ERFA to 30″, and the per-function tier statuses — the eccentricity binds verified, wrap_deg at Tier 1, the transcendentals exactly tier3 at a low, the default and a generous budget, kepler_solve's termination proved	runs
factorial.vera	browser parity (return value); test_codegen_infrastructure.py pins 120	runs
file_io.vera	browser runtime only, where file IO is a documented Err stub; never run natively before the gate	runs
fizzbuzz.vera	nothing, before the gate	runs
gc_pressure.vera	browser parity (stdout)	runs
generics.vera	browser parity (return value); test_codegen_monomorphize.py compiles it without running it	runs
hello_world.vera	browser parity (stdout); test_codegen_strings.py pins the greeting	runs
html.vera	nothing, before the gate	runs
http.vera	nothing	skip: network
http_server.vera	test_wasi_target.py serves the emitted component under stock wasmtime serve and pins three request round-trips	skip: non-scalar-entry
increment.vera	browser parity (return value + State); test_codegen_effects.py	runs
inference.vera	nothing	skip: api-key
inference_json.vera	test_codegen_host_effects.py pins five score renderings and the bad-response arm against a mocked provider	skip: api-key
io_operations.vera	nothing	skip: stdin
json.vera	nothing, before the gate	runs
life.vera	nothing	skip: long-running
list_ops.vera	browser parity (return value); test_codegen_monomorphize.py pins 60	runs
markdown.vera	browser parity (stdout)	runs
maximum_syntax.vera	nothing, before the gate	runs
modules.vera	nothing, before the gate	runs
mutual_recursion.vera	browser parity (return value); test_codegen_infrastructure.py pins three results	runs
nested_closures.vera	nothing, before the gate	runs
pattern_matching.vera	browser parity (return value)	runs
quantifiers.vera	browser parity (return value)	runs
read_char.vera	nothing	skip: stdin
refinement_types.vera	browser parity (return value)	runs
regex.vera	browser parity (stdout)	runs
safe_divide.vera	browser parity (return value + precondition failure); test_codegen_infrastructure.py pins the result and the trap	runs
scoreboard.vera	nothing, before the gate	runs
sqlitedb.vera	test_db_runtime.py pins the rendered city table against the committed fixture	runs
string_ops.vera	browser parity (stdout)	runs
string_utilities.vera	nothing, before the gate	runs
url_encoding.vera	browser parity (stdout)	runs
url_parsing.vera	browser parity (stdout)	runs

Seventeen of those examples were executed by nothing at all before the gate. It runs eleven of them; the remaining six are the ones a property excludes. A twelfth example joins them natively — file_io.vera, which ran only under the browser runtime, where the file IO it demonstrates is a deliberate Err stub.

Each skip cites a property, and the gate prints the property and its reason on every run:

Property	Examples	Why the harness cannot run it
network	async_http_fanout.vera, http.vera	live outbound HTTP, so a run would depend on network reachability and a third party's uptime
api-key	inference.vera, inference_json.vera	with a provider key configured the gate would issue a real, billed request; without one it would only exercise the not-configured arm
stdin	io_operations.vera, read_char.vera	reads interactive input, so what runs is a property of the invoking terminal
non-scalar-entry	http_server.vera	no main, and handle takes a Request ADT that vera run cannot build from CLI arguments
long-running	life.vera	its only public entry point animates 300 generations at 100 ms a frame

Skipping is for programs the harness structurally cannot drive. An example that can be driven and fails is a bug in the compiler or in the example, not a candidate for the skip table.

Stress Tests

Scale-dependent regression tests live in tests/test_stress.py (#596). These exercise Vera programs at sizes where historical bugs (#570 iterative-builder shadow-stack overflow at ~4000 elements, #515 GC self-fault under sustained allocation, #593 Conway's Life corruption at 12×30+) first manifested, plus 2-3x safety margin.

The 9 initial test programs

Each test compiles a self-contained Vera program, executes it via the in-process API, and asserts on a SPECIFIC observable. Iteration counts are tuned to the smallest scale where each bug class historically manifested.

Tests marked [eager-GC] also run under the VERA_EAGER_GC=1 lane (see below).

1. test_array_map_over_10k_int_array [eager-GC] — array_map over a 10,000-element Array<Int>, each element incremented by 1. Asserts array_length of the result == 10000. Pre-#570 this class of program shadow-stack-overflowed at ~4,000 elements; 10K is a 2.5x safety margin. Pins the iterative-builder fix and acts as an early-warning for any future regression in shadow-stack hygiene under array_map.

2. test_array_map_over_5k_nested_bool_array [eager-GC] — array_map over a 5,000-element Array<Int> producing a fresh Array<Bool> ([true, false, true]) per iteration. Asserts the outer length == 5000. Tests per-iteration allocation pressure where each closure call allocates and the result must remain rooted across the loop. Pre-#570 + pre-#515 this class corrupted intermediate roots; the test pins the per-iteration alloc/root hygiene fix.

3. test_deep_tail_recursion_with_allocating_arg [eager-GC] — 1,000-deep tail recursion over loop(@Int, @Int -> @Int) where each iteration allocates a fresh let @Array<Int> = [@Int.0, @Int.1] before recursing. Asserts the final accumulator == 2,000 (1,000 × array_length([_, _]) = 1,000 × 2). Tests the TCO / GC interaction (#549) — tail-call optimisation must not discard the shadow-stack roots that keep the allocating arg live. The body allocates a genuine heap array each iteration (a string-pool literal would not trigger needs_alloc), so the eager-GC lane fires on every iteration.

4. test_conways_life_grid_alloc_and_count_alive_20x20 [eager-GC] — synthetic regression covering #593 (Life corruption from gen 1+ at 12×30). Bug is closed; this test pins the fix. The program builds a 20×20 all-false Array<Array<Bool>> via nested array_map-of-array_range, then runs a single count_alive pass — an array-fold over array-fold that walks every cell. Asserts the count == 0. This is a structural-shape test, not a Life simulation: it does NOT run 100 generations (the original test name implied that; the rename in #669 corrects it). The structural shape — 400-cell allocation, nested array_fold of array_fold, captured outer-binding references inside the inner closure — is what matters; the trivially-deterministic outcome (all-false → 0) makes the test fast and unambiguous while still exercising the code paths #593 hit. (An earlier version of this entry also cited #595 — that was misattributed; #595 is a cleanup-path bug exercised by TestHostSleepKeyboardInterrupt in test_runtime_traps.py, not by this stress test.)

5. test_array_fold_100k_iterations — array_fold over an array_range(0, 100000) summing all values. Asserts the result == 4,999,950,000 (the closed-form sum of 0..99999). Tests the fold accumulator across many GC cycles. Pre-#487 / #348 (worklist + multi-page grow) this class of program ran the heap into multi-page territory and tripped allocation-pressure bugs; the test pins the fixes. The closed-form assertion catches any regression that silently short-circuits or skips iterations. Not in the eager-GC lane — allocation-pressure target, not GC-rooting; 100K × forced-GC would inflate suite time without strengthening detection.

6. test_10k_string_allocations [eager-GC] — array_fold over array_range(0, 10000) where each iteration produces a fresh String via let @String = "\(@Int.0)" and accumulates string_length. Asserts the total == 38,890 (10 × 1-digit + 90 × 2-digit + 900 × 3-digit + 9000 × 4-digit). Pre-#573 (wrap-table compaction) and #575 / #576 (host-store reclamation) this class of program would leak handles or self-fault under sustained String allocation; the test pins the fixes. The digit-count assertion is uniquely sensitive to any short-circuit because it varies non-linearly with iteration count.

7. test_state_handler_1k_ops [eager-GC] — 1,000 State<Int> get/put cycles within a single handle[State<Int>](@Int = 0) { ... } in { ... } scope, driven by a count_up(@Int -> @Int) helper that does get(()); put(state + 1); count_up(n - 1). Asserts the final state == 1000. Pins the handler installation + resume continuation plumbing under sustained host-import call rate. Pre-stage-11 / pre-#535 work, large State-handler programs accumulated captured-frame roots without bound.

8. test_10k_io_print_calls — 10,000 IO.print("x\n") calls in sequence via a loop(@Int -> @Unit) helper, with tee_stdout=True so the captured output buffer grows in lock-step. Asserts the captured stdout contains exactly 10,000 x characters. Exercises the host_print bridge at sustained rate; tests the in-process stdout-capture buffer's growth and the host-import call path under load. The character-count assertion (rather than line-count) is robust to subtle buffering variations. Not in the eager-GC lane — host-import target, not GC-rooting; the host_print bridge doesn't allocate Vera-heap data.

9. test_tco_with_allocation_1m_iterations [eager-GC] — 1,000,000-deep tail recursion over loop(@Int, @Int -> @Int) with a fresh let @Array<Int> = [_, _] per iteration. Asserts the final accumulator == 2,000,000 (1M × 2). The high-volume companion to #3. 1M plain calls would blow the WASM call stack at ~30K frames; the return_call + $gc_sp restore keeps shadow-stack usage flat, so 1M iterations complete in constant memory in ~190ms in both default and eager-GC modes. A shadow-stack leak per iteration would trap the overflow guard around 1,300 iterations (16K shadow stack / ~12 bytes per leaked frame); completing all 1M proves the invariant.

Eager-GC lane

Seven of the nine tests target GC-rooting bug classes (#570 / #515 / #549 / #573 / #593 / captured-frame State handlers). Each of those runs under two parameter modes: default GC and VERA_EAGER_GC=1. The VERA_EAGER_GC env var (read at compile time by vera/codegen/assembly.py) emits a call $gc_collect as the first instruction of the runtime's $alloc function, forcing a full GC pass on every allocation.

This converts latent missing-shadow-root bugs from "fires occasionally at scale" to "fires on the very next allocation," so a regression that would normally require thousands of iterations to surface will fail on the first or second iteration under eager GC. The eager lane embeds this diagnostic capability as ongoing regression coverage.

The eager-GC lane is implemented via a pytest.mark.parametrize("eager_gc", [False, True], ids=["default_gc", "eager_gc"]) decorator + a monkeypatch fixture that scopes the env var to the parametrised test instance. The two non-parametrised tests — test_array_fold_100k_iterations (allocation-pressure target, not GC-rooting) and test_10k_io_print_calls (host-import target) — would inflate the suite under eager GC without strengthening detection of the relevant bug class.

Configuration and behaviour

Default behaviour: stress tests are skipped from the per-PR pytest run via addopts = "-m 'not stress'" in pyproject.toml. Local invocation:

pytest -m stress                    # all 26 marker-carrying instances: test_stress.py's 16 (9 logical tests, 7 with an eager-GC twin) + TestHostHandleReclamation573's 10
pytest tests/test_stress.py -m stress -v   # full stress suite, verbose
pytest tests/test_stress.py::test_array_map_over_10k_int_array -m stress -v   # both modes of one test
pytest "tests/test_stress.py::test_array_map_over_10k_int_array[eager_gc]" -m stress -v   # one mode only

CI integration: .github/workflows/nightly-stress.yml runs them in three triggers:

1. Nightly cron (0 6 * * * UTC) — primary safety net, catches drift in a daily window so bisection cost stays small. Failures auto-file (or comment on) a tracking issue with the stress-regression label so the regression is visible to anyone watching the issue feed. See the failure-reporting subsection below.
2. Path-filtered PRs touching vera/codegen/**, vera/wasm/**, vera/checker/**, tests/test_stress.py, or the workflow file itself — fail-fast for PRs that change code most likely to break stress invariants. vera/checker/** is included because the AST shape it produces flows into codegen — a checker change that subtly alters the AST can break runtime invariants without touching vera/codegen/ or vera/wasm/. PR failures show on the PR's checks tab; no tracking issue is filed (the PR author already sees the failure).
3. workflow_dispatch — manual trigger from the Actions tab for local-suspicious commits. Failures are visible to whoever triggered the run; no tracking issue is filed.

Failure reporting (cron only): when the nightly cron fails, the workflow opens an issue titled "Nightly stress regression on main (tracking)" with the stress-regression label, including the commit SHA and the run URL. If an open issue with that label already exists, the new failure posts a comment on it instead of filing a duplicate — so the issue persists across days of failures until a maintainer manually closes it. The stress-regression label is auto-created on first failure. This converts cron failures from "visible only to whoever opens the Actions tab" to "visible in the issue feed where Vera work is already triaged." Implementation uses actions/github-script@v9 with issues: write job-scoped permission.

Budget: the workflow's suite — tests/test_stress.py per the invocation above; the marker's other 10 instances in test_codegen_gc_reclamation.py currently run only under an explicit pytest -m stress invocation, since the per-PR suite deselects the marker and this workflow is file-scoped (#1328) — completes in well under the 5-minute target: measured at 0.66s in-process on a developer laptop on 2026-05-13 for its 16 test instances (9 logical × eager-GC lane on 7 of them). CI cold-start adds workflow setup time on top. Iteration counts are tuned to the smallest scale where each bug class has historically manifested with ~2-3x safety margin, NOT maximised — the goal is reliable detection of the bug class, not benchmarking. If this measured figure drifts more than ~2x in either direction, treat it as a signal: either iteration counts have grown without rationale (revisit per the "Adding a stress test" rule 2) or a runtime perf regression has landed.

Assertion shape: each test asserts on a SPECIFIC observable (e.g. array_fold returning the closed-form sum 4999950000, IO.print producing exactly 10000 x characters), not just "completed without crashing". This catches a future regression where the loop silently short-circuits or skips iterations.

Adding a stress test

A new stress test should:

1. Target a specific scale axis (iteration count, allocation pressure, recursion depth, handler-op rate, etc.) and name the bug class it guards against in its docstring. Reference the issue number(s).
2. Pick the smallest scale that reliably manifested the bug class historically, plus ~2-3x safety margin. Don't maximise — bigger isn't better and inflates the suite.
3. Assert on a SPECIFIC observable with a closed-form or otherwise unambiguous expected value. Avoid "no exception raised" — that passes silently when the loop short-circuits.
4. Use the _run helper (or a parallel helper for non-pure tests) — it handles tempfile lifecycle, parsing, compilation, error checking, and execution.
5. Carry pytestmark = pytest.mark.stress at module level (the file already does) so the test is collected only under pytest -m stress.
6. Opt into the eager-GC lane if the target bug class is GC-rooting-related (shadow-stack, captured-frame, alloc-pressure-root-loss). Add @EAGER_GC_PARAMS above the function, change the signature to (eager_gc: bool, monkeypatch: pytest.MonkeyPatch), and pass both through to _run(src, eager_gc=eager_gc, monkeypatch=monkeypatch). Skip the lane if the bug class is unrelated to GC rooting (host-import call rate, parser perf) — doubling the test cost without strengthening detection is the wrong trade.

Mutation Testing

A passing suite is necessary, not sufficient — a green test can pass for the wrong reason (the #680 audit found 8 such tests in one 57-test battery; #734 had to mutation-validate its own harness). Mutation testing checks the checker: it deliberately breaks each line of vera/ and confirms a test flips RED. A surviving mutant is a test gap — a weak test to strengthen or an equivalent mutant to annotate (# pragma: no mutate).

The full mechanics — the tool decision (mutmut, the [mutation] extra, the [tool.mutmut] config), the in-process-oracle caveat (subprocess suites import the un-mutated package, so they can't kill mutants), resume-after-hard-kill, the Z3-flakiness guardrail, and the survivor-triage workflow — live in the runbook: MUTATION.md.

Baseline — soundness core. The first sweep covers verifier.py, smt.py, checker/, and obligations/: 10,620 mutants, 80.8% caught, 2,038 survivors. The committed score is mutation-summary.csv (per-module, diff-able) plus a README badge (mutation.json, regenerated by scripts/mutation_report.py); the full survivor inventory and per-module chart are attached to #387. Soundness-core triage and the whole-vera/ sweep — deferred behind the #421 execute() decomposition, which otherwise inflates a mutant file mutmut can't index — are tracked there.

Mutation testing runs locally for now (the measure-all sweep is multi-day; CI's 6 h job cap can't hold it). A non-gating on-demand workflow and a diff-scoped PR gate are deferred to a focused follow-up PR — see MUTATION.md § CI.

Test Fixture Conventions

Footguns in how a fixture is written or run — most cross-platform, from the post-#637 Windows CI rollout (PRs #639/#643/#644/#646) and #1246's, and one about which checkout a suite actually measures. Each has a workaround that makes the fixture portable across Linux / macOS / Windows. This section is the one place they are stated; for the specific job of building a ResolvedModule fixture, tests/module_fixture_helpers.py applies all of them and is what a multi-module test should import (#1228).

Running against ANOTHER checkout: the argument decides, not PYTHONPATH

To measure a test file against a different revision — a baseline worktree, to prove a new cell is red before a fix — it is not enough to set PYTHONPATH to that checkout and pass the test file by path:

# WRONG — silently measures the CURRENT checkout
cd /path/to/baseline
PYTHONPATH=/path/to/baseline pytest /path/to/current/tests/test_x.py

pytest resolves its rootdir from the ARGUMENTS, finds the current checkout's pyproject.toml, and inserts that directory at sys.path[0] — ahead of PYTHONPATH. import vera then loads the tree the file came from, so the "baseline" run exercises the code under test and passes. Nothing warns; the run simply proves the opposite of what it appears to.

# RIGHT — copy the file in, so rootdir and sys.path[0] are the baseline.
# The SOURCE path is absolute: a relative one resolves against whatever
# directory you are in, and the block above has already left you in the
# baseline — where it would copy the file over itself and measure nothing.
cp /path/to/current/tests/test_x.py /path/to/baseline/tests/
cd /path/to/baseline && pytest tests/test_x.py

The same trap has a second form, and it is the one most people meet first: for python -c and python -m, sys.path[0] is the process's CWD, so those invocations follow the directory you are standing in and ignore a PYTHONPATH that points elsewhere — including the canary below, which is why the canary must be run from the tree you mean to measure.

Assert the canary rather than trusting it: python -c "import vera; print(vera.__file__)", run from the baseline directory, must name the baseline. A red-proof is worth exactly as much as the certainty about which compiler produced it.

Tempfiles handed off to subprocesses must use delete=False

Windows can't reopen a file while another handle is still held; if a test fixture writes to a tempfile via with tempfile.NamedTemporaryFile(delete=True) as f: and then runs subprocess.run([..., f.name]) inside the with block, the subprocess fails with a PermissionError because the parent still holds the handle. Unix allows concurrent handles so the same fixture works there.

# Wrong — fails on Windows:
with tempfile.NamedTemporaryFile(mode="w", suffix=".vera", delete=True) as f:
    f.write(content)
    f.flush()
    subprocess.run([sys.executable, "-m", "vera.cli", "check", f.name])

# Right — portable:
f = tempfile.NamedTemporaryFile(mode="w", suffix=".vera", delete=False)
try:
    f.write(content)
    f.close()
    subprocess.run([sys.executable, "-m", "vera.cli", "check", f.name])
finally:
    Path(f.name).unlink(missing_ok=True)

Surfaced via tests/test_html.py::TestHtmlCodeSamples — see PR #646 for the fix.

Corollary — the cleanup must be sequenced, not just present. delete=False means the file outlives its with, so a failure inside the block leaves it behind and the fixture needs its own cleanup. It is tempting to put that in an except next to the write — but Windows cannot delete a file whose handle is still open, so an unlink there is PermissionError (WinError 32) rather than a cleanup. Both rules are satisfied by capturing the name first, letting the with close the handle on its way out however it leaves, and unlinking once afterwards:

# Wrong — cleans up on failure, but while the handle is still open:
with tempfile.NamedTemporaryFile(mode="w", delete=False, encoding="utf-8") as f:
    fp = f.name
    try:
        f.write(source)
    except BaseException:
        os.unlink(fp)          # WinError 32 on Windows
        raise

# Right — one cleanup site, after the handle is closed, on every path:
tmp = tempfile.NamedTemporaryFile(mode="w", delete=False, encoding="utf-8")
fp = tmp.name
try:
    with tmp as f:             # closes the handle however this block exits
        f.write(source)
    ...
finally:
    Path(fp).unlink(missing_ok=True)

The ordering is observable without a Windows machine — record whether the handle is closed at the moment each unlink is issued — which is how TestModuleFixtureBuilders::test_the_handle_is_closed_before_every_unlink pins it on every platform. Surfaced by #1228's leak fix, which was green on POSIX and red on all three Windows cells.

Paths embedded into Vera string literals must use POSIX form

Windows tempfile paths look like C:\Users\runner\AppData\Local\Temp\.... Vera's grammar (correctly) rejects \U as an invalid string-literal escape, so embedding such a path via f-string interpolation trips [E009] Invalid escape sequence: \U at parse time. Convert to POSIX form before embedding:

# Wrong — fails on Windows:
source = f'IO.read_file("{tmp_path}")'

# Right — portable (Windows file APIs accept forward slashes).
# `Path(tmp_path).as_posix()` works whether `tmp_path` is a str
# (from `tempfile.NamedTemporaryFile().name`) or a `pathlib.Path`
# (from pytest's `tmp_path` fixture).  Don't use `tmp_path.replace`
# — that's `str.replace` on a string but `Path.replace` (the
# rename method!) on a Path, which would silently move the file.
vera_path = Path(tmp_path).as_posix()
source = f'IO.read_file("{vera_path}")'

Surfaced via tests/test_codegen_io.py::TestIOOperations::test_io_read_file_* — see PR #643 for the fix.

Repo-relative paths COMPARED as strings must be POSIX form

The rule above is about a path embedded in Vera source; this one is about a path used as a key. str(path.relative_to(ROOT)) renders tests\conformance\x.vera on Windows, so any later startswith("tests/conformance/"), "examples/" in origin, or dict lookup against a POSIX-spelled literal matches nothing — and matching nothing is silent. A filter that classifies zero files does not raise; it reports an empty population, which reads as "the thing you were counting shrank", not "your comparison is broken". It is also invisible to a local hook run, because macOS and Linux satisfy the POSIX spelling.

# Wrong — the string is native-separator, so every POSIX prefix misses on Windows:
origin = str(path.relative_to(ROOT))
maintained = [o for o in origins if o.startswith("examples/")]   # [] on Windows

# Right — POSIX by construction, at the point the path becomes a string:
origin = path.relative_to(ROOT).as_posix()

Do the conversion where the string is created, not at each comparison: one as_posix() makes the property hold for every consumer, where a per-comparison fix has to be remembered by each new one. Path.parts tuples are an equally portable alternative when you are matching whole segments rather than a prefix.

Surfaced via tests/test_slot_naming_differential.py::test_corpus_is_almost_entirely_parseable, which re-anchored its floor on the maintained corpus (examples/ + tests/conformance/) and went red on all three Windows cells with AssertionError: (0, 428) — the walk had collected all 428 files, and the classification matched none of them. That test now also asserts no origin contains a backslash, so the regression names its own cause.

A path a converter RETURNED must not be asserted by its POSIX shape

The two rules above are about paths the test constructs — embedded into Vera source, or compared as a repo-relative key. This is their assertion-side twin: a path handed back by a standard-library converter is in the platform's spelling, so pinning it against a literal /-shaped string passes on Linux and macOS and fails on all three Windows cells. urllib.request.url2pathname("/tmp/x.vera") is /tmp/x.vera on POSIX and \tmp\x.vera on Windows; url2pathname("/") is / and \. The POSIX cells greening proves nothing about the Windows ones, which is what makes this class of assertion easy to write and impossible to notice locally.

Assert the property, relationally, so no shape is named:

# Wrong — a POSIX shape, so red on every Windows cell:
assert uri_to_path("FILE:///tmp/x.vera") == "/tmp/x.vera"
assert uri_to_path("file:///") == "/"

# Right — case-insensitivity is "every spelling gives the same answer as
# the lowercase one", and the inequality keeps three non-conversions from
# satisfying it by all agreeing:
lowercase = uri_to_path("file:///tmp/x.vera")
assert uri_to_path("FILE:///tmp/x.vera") == lowercase
assert uri_to_path("FILE:///tmp/x.vera") != "FILE:///tmp/x.vera"

# Right — "is a root" holds of `/` and `\` alike:
root = Path(uri_to_path("file:///"))
assert root.name == "" and root.parent == root

Assertions that compare against a path the test itself built (str(tmp_path / "x.vera"), or a round-trip through Path.as_uri()) are already portable — the expected value is in the same spelling as the actual. So are assertions that the INPUT comes back unchanged, which is how the opaque/pass-through cases are pinned. Surfaced by tests/test_lsp.py::TestUriToPath (#1246), where two of nine assertions named a shape and seven did not.

File I/O without explicit encoding falls back to the locale default

Python's text-mode open() / read_text() / write_text() without an explicit encoding= kwarg defaults to locale.getpreferredencoding(), which is cp1252 on en-US Windows. Tests that read or write files containing → (right arrow), — (em-dash), or other non-ASCII characters fail on Windows with UnicodeEncodeError: 'charmap' codec can't encode '→' or UnicodeDecodeError: ... 0x97.

Every text-mode open() / read_text() / write_text() under vera/, scripts/, tests/ — and every subprocess.run/Popen/check_output(..., text=True) capture and text-mode tempfile.NamedTemporaryFile — therefore MUST pass an explicit encoding="utf-8", enforced by scripts/check_explicit_encoding.py (pre-commit + CI lint, #645). The vera CLI additionally reconfigures its stdin/stdout/stderr to UTF-8 at startup, so a Vera program reading or printing → / — is UTF-8 on any locale. Together these made text I/O locale-independent and let the PYTHONUTF8=1 CI backstop (#641) be removed. Use the explicit form (a deliberate non-UTF-8 site can opt out with # encoding-exempt: <reason>):

# Implicit — locale-dependent (cp1252 on Windows); rejected by the gate:
text = path.read_text()

# Explicit — works everywhere:
text = path.read_text(encoding="utf-8")

Surfaced via ~9 tests across test_codegen_monomorphize.py, test_codegen_closures.py, test_html.py, and the other test_codegen_*.py split files — see PR #646 for the CI-side fix.

Evidence about temp files must name them, not sweep a shared directory

CI runs pytest -v -n auto, so several xdist workers build fixtures at the same time, each creating its own tmp*.vera in the one system temp directory. A test that asserts over the contents of that directory is therefore reading other workers' files, and a sibling's fixture that lives for the microseconds between the snapshot and the assertion reads as litter this test left:

# Wrong — the evidence set includes every worker's files:
pattern = str(Path(tempfile.gettempdir()) / "*.vera")
before = set(glob.glob(pattern))
...
assert set(glob.glob(pattern)) - before == set()

# Right — the evidence is the path THIS call created:
created: list[str] = []
monkeypatch.setattr(helpers.tempfile, "NamedTemporaryFile", recording_ntf)
...
assert len(created) == 1, created          # else the check is vacuous
assert [n for n in created if Path(n).exists()] == []

The sweep form was flaky rather than wrong: it passed for a whole PR and then failed on the v0.1.10 release push over a C:\...\tmp*.vera on worker gw1, an hour after the identical tree passed (~33% reproducible on macOS under a second writer). Capturing the name removes the race instead of relocating it — no shared directory is read at all — and a len(...) == 1 guard keeps it from passing vacuously if the builder stops creating its file that way. Redirecting TMPDIR/TEMP/TMP at a private directory is the other cure, but it costs an env triple plus a reset of tempfile.tempdir (which caches the resolved directory, so the env alone changes nothing) and still asserts over a directory rather than a file.

Adding Tests

When extending the compiler, add tests following the existing patterns:

1. New grammar construct: Add parser tests to test_parser.py (positive and negative)
2. New AST node: Add transformation tests to test_ast.py (check node fields, spans, serialisation)
3. New type rule: Add checker tests to the matching test_checker_*.py phase file using _check_ok()/_check_err() (imported from tests/checker_helpers.py)
4. New SMT support: Add verifier tests to the matching test_verifier_*.py theme file using _verify_ok()/_verify_err() (imported from tests/verifier_helpers.py)
5. New codegen support: Add compilation tests to the matching test_codegen_*.py feature file using _compile_ok()/_run()/_run_trap() (imported from tests/codegen_helpers.py) 5a. New multi-module test (any suite): Build the imported modules with resolved_module() / fake_resolved_module() from tests/module_fixture_helpers.py — never a local tempfile copy
6. New example program: Add to examples/ -- it is automatically included in round-trip tests
7. New error pattern: Add formatting tests to test_errors.py
8. New tester feature: Add tests to test_tester.py using _test(source) helper
9. New host binding: Add parity tests to test_browser.py to ensure the JavaScript runtime stays in sync with the Python runtime

Validation Scripts

Twenty-nine scripts in scripts/ validate cross-cutting concerns beyond unit tests (one of them — build_site.py — generates rather than checks; the doc-block gates share the fence-annotation reader scripts/doc_annotations.py, a helper module rather than a gate):

Script	What it validates
check_conformance.py	All 244 conformance entries hold at their declared level (parse/check/verify/run) — positives pass; the negatives fail at the stage their expected_error_stage names (check by default, or compile, which also asserts the program type-checks cleanly) with their expected_error E-code
check_examples.py	All 43 .vera examples pass vera check + vera verify
check_corpus_canonical.py	All 294 corpus programs (recursive over examples/ + tests/conformance/) are in canonical form under vera fmt
check_examples_readme.py	Every vera run command in examples/README.md references an existing file and exported function
check_spec_examples.py	189 parseable code blocks from spec chapters: parse, type-check, and verify
check_readme_examples.py	All Vera code blocks in README.md parse correctly
check_skill_examples.py	All Vera code blocks in SKILL.md parse correctly
check_faq_examples.py	All Vera code blocks in FAQ.md parse correctly
check_debruijn_examples.py	All Vera code blocks in DE_BRUIJN.md parse correctly
check_pypi_readme_examples.py	All Vera code blocks in PYPI_README.md parse, check, and verify
check_examples_doc.py	All Vera code blocks in EXAMPLES.md parse correctly
check_html_examples.py	All Vera code blocks in docs/index.html pass parse + check + verify
check_site_assets.py	Generated site assets under docs/ are up-to-date, and check_fact_coherence() verifies the load-bearing facts of docs/index.html and docs/index.md agree (#1154)
check_version_sync.py	The same version in five files: pyproject.toml, vera/__init__.py, docs/index.html (the badge, whose URL and link text are checked separately), README.md's "active development at vX.Y.Z", and uv.lock's editable veralang entry. It does NOT read CHANGELOG.md — the matching ## [X.Y.Z] section is a separate requirement, enforced by the changelog gate and the release workflow
check_doc_counts.py	A fixed set of named citations match the live codebase — not every number in the docs. Filesystem-derived counts (conformance programs, examples, test files, pre-commit hooks, CI jobs, corpus programs, releases against git tag) and pytest-collection counts (suite total, per-file test and line counts) where TESTING.md, CONTRIBUTING.md, CLAUDE.md, README.md, SKILL.md, AGENTS.md, FAQ.md and ROADMAP.md cite them; TESTING.md's passed/stress/skipped breakdown against the collected total and its conformance skip total against its own table; vera/README.md's module map and its Test Suite paragraph's four counts; the landing-page facts (#528); KNOWN_ISSUES refactoring counts within ±10%; HISTORY version-row format; and the CI-pipeline lint row enumerating exactly the scripts ci.yml's lint job runs, in its order. Each is keyed to the sentence that carries it, so a reworded citation is an error rather than a silent skip — but a count in prose the script does not name is not read at all, and hand-written program lists (such as the conformance-level lists in this document) are outside its scope entirely. CHANGELOG.md is excluded deliberately: its counts are frozen historical snapshots
check_limitations_sync.py	Limitation tables consistent across KNOWN_ISSUES.md, vera/README.md, spec chapters, SKILL.md, and LSP_SERVER.md
check_changelog_updated.py	CHANGELOG.md gains an entry when substantive files change (Skip-changelog: trailer to bypass)
check_walker_coverage.py	Every walker function in vera/ covers every Expr subclass via isinstance dispatch or # WALKER_COVERAGE: checklist comment (#597)
check_diagnostic_fields.py	Every diagnostic in vera/ carries rationale + spec_ref, and errors also a fix (warnings exempt); every present spec_ref resolves to a real spec section; every literal error_code is registered in ERROR_CODES (#828); # diag-fields-exempt: <reason> waives missing/unresolvable fields only — never a wrong-but-resolving spec_ref or an unregistered error_code (#682, #955)
check_explicit_encoding.py	Every text-mode open() / read_text() / write_text(), subprocess.run/Popen/check_output text capture, and text-mode tempfile.NamedTemporaryFile under vera/, scripts/ and tests/ passes an explicit encoding="utf-8"; # encoding-exempt: <reason> opts a deliberate non-UTF-8 site out (#645)
check_e602_clean.py	No unexpected E602/E604 silent-skip sites outside the explicit allowlist
check_examples_run.py	Every examples/*.vera either runs trap-free under the native runtime or carries a documented skip property. Two signals, as in check_examples.py: the exit code, and an output signal — every spec names its entry point (so a privatised or renamed main exits 1 instead of silently running another export) and every example that declares a resource effect or calls a resource operation pins a success sentinel (so a vanished fixture fails rather than passing on a graceful arm), the set being derived from those declarations rather than named. An unclassified example is an error, and TESTING.md's execution-coverage table must match the script's own classification
check_doc_builtin_shadowing.py	No documentation example defines a function named after an opaque verifier-modelled built-in (would fail vera check with E151); the spec/09 signature reference is exempt (#819)
check_grammar_alignment.py	Every rule header in spec/10-grammar.md's EBNF has a same-named rule in vera/grammar.lark, and the reverse (#683); every terminal is declared and referenced within its own file, every regex-bodied terminal carries the same pattern in both, and each shared production's right-hand side refers to the same rules and terminals (#1290). The shape of a right-hand side — alternation, grouping, repetition — is still not compared
check_editor_grammars.py	Every editor grammar under editors/ (vscode, TextMate, Vim), and the two extension READMEs that repeat the list in prose, carries every built-in effect name from the live registry — read from the checked-out tree, not from whatever vera is importable. Word-boundary presence: absence is conclusive, presence is optimistic — the observed failure is omission. A completeness guard fails any grammar discovered under editors/ that the checked list doesn't name (#1156)
check_distribution.py	The built wheel and sdist carry the project's own name and version, ship the files the installed package needs plus a packaged LICENSE, and exclude tests/ and generated Python files
check_wheel_availability.py	Every runtime dependency ships wheels for all supported platforms
check_licenses.py	All installed packages have MIT-compatible licenses
build_site.py	Regenerates the AI-readable site assets that check_site_assets.py verifies

Each runs in its configured pre-commit hook or CI job, so issues are caught locally before they reach the remote; build_site.py is the generator whose output check_site_assets.py verifies.

One script is deliberately outside that set. check_corpus_differential.py compiles every corpus program at two revisions and reports the ones whose WAT moved, including the ones that compile on only one side — the measurement behind a "codegen is unchanged" claim, and the scope list when output is meant to change. It costs minutes rather than milliseconds, so it is a burndown instrument run by hand (--base-ref origin/main), not a hook and not a CI gate; a test asserts its absence from .pre-commit-config.yaml so that claim cannot rot. check_doc_counts.py --check-bug-issues is opt-in for the same kind of reason — it needs the GitHub API, which a commit hook must not — and belongs to the release PR (see RELEASING.md).

Spec validation pipeline

check_spec_examples.py pushes spec code blocks through three compiler stages. A block that intentionally fails a stage carries an inline annotation on the line before its fence — <!-- vera:skip-parse category="..." reason="..." --> (or vera:skip-check / vera:skip-verify; see scripts/doc_annotations.py and #538):

Stage	Pass	Annotated	Categories
Parse	92	96	FRAGMENT (83), FUTURE (13)
Type-check	86	6	INCOMPLETE (5), ILLUSTRATIVE (1)
Verify	85	1	ILLUSTRATIVE (1)

Annotations travel with their fence through spec edits, so there are no line numbers to maintain (no line-number-keyed allowlist to maintain — #538/#606). Stale-detection is built in: the gate still runs the exempted stage, and an annotated block that passes it fails the gate until the annotation is removed — when a feature lands, the skip surface shrinks. The INCOMPLETE check entries reference functions or types not defined in the block (e.g. is_sorted in a data invariant); the ILLUSTRATIVE entries demonstrate syntax with contracts that are intentionally imprecise. The same annotation mechanism (parse stage only) covers SKILL.md, FAQ.md, README.md, and EXAMPLES.md; check_html_examples.py reads it from HTML comments before <pre> blocks in docs/index.html. build_site.py strips the annotations from generated site assets.

JSON Output Stability

vera check --json, vera verify --json, and vera test --json emit structured JSON for downstream tooling (CI pipelines, IDE plugins, agent feedback loops). The field set is a public API — see spec/00-introduction.md §0.5.8 for the stability rules. Tests in tests/test_cli.py assert on the documented field set, so a regression that drops a documented field will fail at least one test.

vera check --json / vera verify --json

Top-level:

Field	Type	Description
ok	bool	true iff the file passed all checks at the requested stage; the canonical exit-code signal
file	string	The source file checked (echoes the path argument)
diagnostics	array	List of error-severity Diagnostic objects (see below)
warnings	array	List of warning-severity Diagnostic objects
verification	object	Only on vera verify --json — counts of tier1_verified, tier3_runtime, total
slot_environments	array	Only when --explain-slots is passed — per-function slot tables

Diagnostic shape: severity, description, location, source_line, rationale, fix, spec_ref, error_code (the error_code set is documented in vera/errors.py::ERROR_CODES).

vera test --json

Top-level:

Field	Type	Description
ok	bool	true iff summary.failed == 0 and no verifier errors; the canonical exit-code signal
file	string	The source file tested
functions	array	Per-function FunctionTestResult: name, category (one of "verified", "tested", "failed", "skipped"), reason, trials_run, trials_passed, trials_failed, failures
summary	object	Aggregate counts (see below)
diagnostics	array	Verifier-error diagnostics that fed into "failed" classifications

summary field set:

Field	Description
verified	Functions classified Tier 1 (proved by Z3)
tested	Functions exercised with Z3-generated inputs
passed	Subset of tested where all trials passed
failed	Verifier-refuted OR Tier-3-tested-with-trial-failures
skipped	Functions whose inputs can't be Z3-generated (e.g. ADT params)
total_trials	Sum of trials run across all tested functions
total_passes	Sum of passing trials
total_failures	Sum of failing trials
unlisted_errors	Verifier-error diagnostics whose attributable function isn't in the displayed functions list (--fn filtering, private helpers). Added in v0.0.156.

Stability contract

Per spec/00-introduction.md §0.5.8: fields MAY be added (consumers MUST tolerate unknowns), fields MUST NOT be removed or renamed without a major version bump, and field semantics MUST NOT change. ok is the canonical gate; downstream CI SHOULD read it rather than parse field-by-field.

Pre-commit Hooks

The repository configures 36 hooks across two stages: 34 run at the commit stage (after pre-commit install), and 2 (check-changelog-updated, uv-lock-check) run at the push stage (after pre-commit install --hook-type pre-push). Many commit-stage hooks use per-hook files: / types: filters and only fire when matching files are staged — a docs-only commit triggers a small subset, a compiler-level commit triggers most. Full list:

Hook	What it does
trailing-whitespace	Strip trailing whitespace
end-of-file-fixer	Ensure files end with a newline
check-yaml	Validate YAML syntax
check-toml	Validate TOML syntax
check-merge-conflict	Detect conflict markers
check-added-large-files	Reject files >500 KB
debug-statements	Detect pdb/ipdb imports
ruff check .	Lint Python with ruff (default F + E rules)
mypy vera/	Type-check compiler in strict mode
pytest tests/ -q	Run full test suite
check_conformance.py	All 244 conformance entries hold at their declared level — positives pass; negatives fail at the stage their expected_error_stage names (check or compile) with their expected_error E-code
check_examples.py	All 43 examples pass vera check + vera verify
check_corpus_canonical.py	All 294 examples/ + tests/conformance/ programs (recursive) are in canonical form (vera fmt)
check_examples_readme.py	vera run commands in examples/README.md reference existing files and exported functions
check_readme_examples.py	README code blocks parse correctly
check_examples_doc.py	EXAMPLES.md code blocks parse correctly
check_skill_examples.py	SKILL.md code blocks parse correctly
check_faq_examples.py	FAQ.md code blocks parse correctly
check_debruijn_examples.py	DE_BRUIJN.md code blocks parse correctly
check_pypi_readme_examples.py	PYPI_README.md code blocks parse, check, and verify
check_html_examples.py	HTML landing page code blocks pass parse + check + verify
check_doc_builtin_shadowing.py	No doc example defines a function named after an opaque built-in (would fail vera check with E151); spec/09 signature reference exempt (#819)
check_grammar_alignment.py	Spec EBNF and Lark grammar agree on every rule name (#683), every terminal, and the symbols each shared production refers to (#1290)
check_editor_grammars.py	Every editor grammar under editors/, and the two extension READMEs, carry every built-in effect name from the live registry (#1156)
check_e602_clean.py	No unexpected [E602] (body unsupported) / [E604] (param unsupported) silent skips outside the explicit allowlist (Layer 1 of #626)
check_examples_run.py	Every example runs trap-free (exit code plus an output signal) or carries a documented skip property, and TESTING.md's execution-coverage table matches
check_doc_counts.py	Counts in docs match live codebase
check_walker_coverage.py	Every walker function covers every Expr subclass via dispatch or checklist comment (#597)
check_diagnostic_fields.py	Every diagnostic in vera/ carries rationale + spec_ref, and errors also a fix (warnings exempt); every present spec_ref resolves to a real spec section; every literal error_code is registered in ERROR_CODES (#828); # diag-fields-exempt: <reason> waives missing/unresolvable fields only — never a wrong-but-resolving spec_ref or an unregistered error_code (#682, #955)
explicit-encoding	Every text-mode open() / read_text() / write_text(), subprocess.run/Popen/check_output text capture, and text-mode tempfile.NamedTemporaryFile passes encoding="utf-8" (#645)
check_limitations_sync.py	Limitation tables consistent across KNOWN_ISSUES.md, vera/README.md, spec chapters, SKILL.md, and LSP_SERVER.md
check_licenses.py	All package licenses are MIT-compatible
build_site.py	Regenerate AI-readable site assets (llms.txt, llms-full.txt, robots.txt, sitemap.xml, index.md)
browser parity	Browser runtime matches the Python runtime across the surface the two share
check-changelog-updated (pre-push)	CHANGELOG has a new entry when substantive files changed
uv-lock-check (pre-push)	uv.lock is in sync with pyproject.toml

The validation hooks are smart about triggers -- each fires only when files matching its own files: pattern in .pre-commit-config.yaml change, so that file is the authority on any given hook's trigger set. The common patterns are .vera sources, vera/**/*.py, grammar.lark, and the Markdown file a doc gate reads; narrower ones exist too, such as editors/* for the editor-grammar gate and vera/browser/* for browser parity. The two pre-push hooks only fire at push time.

Scheduled limitations sync

.github/workflows/limitations-sync.yml runs check_limitations_sync.py --check-states every Monday 07:00 UTC (and on demand via workflow_dispatch): every issue a KNOWN_ISSUES.md / vera/README.md / spec / SKILL.md / LSP_SERVER.md limitation row cites is queried against the tracker, and a closed issue still listed as a limitation fails the run — as does an issue whose state cannot be determined (gh auth failure / rate limit / timeout), which errors rather than passing vacuously (#852, #960). Deliberately not a required merge check: issue state drifts independently of any PR, so it is a visibility signal — a cron failure files or updates a limitations-drift-labelled tracking issue, mirroring nightly-stress.yml's failure routing.

CI Pipeline

GitHub Actions (.github/workflows/ci.yml) runs the following nine parallel jobs on every push and pull request to main (the test row is split into a baseline variant and a coverage-instrumented variant on the gating cell, sharing the same underlying job definition):

Job	Matrix / Runner	What it checks
test	Python 3.11, 3.12, 3.13 × ubuntu-latest, macos-15, macos-26, windows-latest, plus advisory ubuntu-24.04-arm × 3.12 (13 combos)	pytest -v passes on all combinations
test (coverage)	Python 3.12 x Ubuntu only	pytest --cov=vera --cov-fail-under=80
typecheck	Python 3.12 x Ubuntu	mypy vera/ clean in strict mode
lint	Python 3.12 x Ubuntu	check_changelog_updated.py, check_conformance.py, check_examples.py, check_corpus_canonical.py, check_examples_readme.py, check_version_sync.py, check_spec_examples.py, check_grammar_alignment.py, check_readme_examples.py, check_skill_examples.py, check_faq_examples.py, check_debruijn_examples.py, check_pypi_readme_examples.py, check_html_examples.py, check_doc_builtin_shadowing.py, check_e602_clean.py, check_examples_run.py, check_editor_grammars.py, check_diagnostic_fields.py, check_explicit_encoding.py, check_site_assets.py, check_licenses.py, check_doc_counts.py, check_limitations_sync.py, ruff check ., ruff check --select S vera/ (security rules), uv lock --check
security	Ubuntu	Gitleaks secret scanning on full history
dependency-audit	Python 3.12 x Ubuntu	pip-audit --skip-editable — checks all installed packages against the OSV vulnerability database (skips the local editable vera package)
wheel-preflight	Python 3.12 x Ubuntu	python scripts/check_wheel_availability.py — verifies every runtime dep has prebuilt wheels for every (platform, python-version) tuple documented in README §Supported platforms; structural backstop for #691-class install regressions
package-distribution	Python 3.12 x Ubuntu	python -m build, twine check dist/*, and python scripts/check_distribution.py dist on the artifacts that will ship under the veralang name, then a wheel smoke-test: install dist/*.whl into a fresh venv outside the checkout and run vera version / vera check / vera run over hello_world.vera. PR CI validates the archives and publishes nothing (#737)
sbom	Python 3.12 x Ubuntu	cyclonedx-py environment — generates a CycloneDX JSON SBOM of the full installed dependency tree and uploads it as a 90-day CI artifact
browser-parity	Python 3.12 + Node.js 22 x Ubuntu	pytest tests/test_browser.py -v — verifies JS runtime matches Python runtime; collects V8 coverage via NODE_V8_COVERAGE and uploads to Codecov

The coverage threshold of 80% is enforced in CI. Current coverage is 95% Python, 87% JavaScript — matching the overview table above. The two are reported as two figures and never blended into one: they come from different collectors over different line populations (pytest --cov over the Python compiler, V8 over vera/browser/), so a combined percentage would need a line-weighted total that neither report produces. JavaScript coverage for vera/browser/runtime.mjs is collected separately using V8's built-in coverage and uploaded to Codecov with the javascript flag, independently of the Python pytest --cov report.

Each job uses scoped permissions (contents: read; the security job additionally has security-events: write) and all checkout steps set persist-credentials: false to prevent the GITHUB_TOKEN from being baked into .git/config. Action refs are pinned to major-version tags (actions/checkout@v7), with two exceptions pinned to full commit SHAs: pypa/gh-action-pypi-publish (the Trusted Publishing step, which holds the pypi environment's credentials) and codecov/codecov-action (a third-party uploader that runs with the repository checkout). Each SHA carries the tag it corresponds to in a trailing comment.

Open CI/Tooling Issues

Tracked improvements to the testing and CI infrastructure:

Issue	Description
#1295	Decide whether the four abilities (Eq/Hash/Ord/Show) highlight distinctly from ordinary types in the editor grammars
#1103	Migrate GitHub Pages off legacy branch-deploy to a self-owned Actions workflow
#712	Watch: Codecov → Harness migration (action / token / endpoint / badge). The JavaScript side is also unasserted today — codecov.yml marks both JavaScript statuses informational: true with target: auto (a comparison against the base commit, not an absolute floor), and the browser-parity job uploads lcov.info without printing or asserting a percentage, so nothing holds runtime.mjs above a threshold the way pytest --cov holds the Python side
#540	Add lychee + markdownlint MD051 for cross-doc anchor validation
#402	Investigate parser fuzzing with Atheris for crash detection
#386	Add property-based testing for parser/formatter round-trip

Opportunities

Testing infrastructure that could be added in the future:

• Property-based testing -- hypothesis is installed as a dev dependency but not yet used. Could generate random programs to test parser robustness and formatter idempotency at scale.
• Formatter round-trip invariant -- verify parse(format(parse(src))) == parse(src) for all valid programs, not just the examples.
• WASM inference.py coverage -- wasm/inference.py at 80% has the most remaining gaps, mostly in deep type-dispatch branches for specific builtin function return types. These branches require very specific expression nesting patterns to reach.
• Performance benchmarks -- no benchmark infrastructure exists. Could track compilation time and Z3 verification time across releases.