Verify each finding against the current code and only fix it if needed.

Inline comments:
In `@README.md`:
- Line 588: Update the coverage percentage in README.md by replacing the phrase
"The compiler has 91% code coverage" with "The compiler has 96% code coverage"
so the front-page metric matches TESTING.md; ensure the sentence referencing CI
and coverage remains unchanged except for the updated percentage, and
double-check the exact phrase "The compiler has 91% code coverage" is the one
you modify.

In `@tests/test_browser.py`:
- Around line 716-726: Add a new unit test in tests/test_browser.py that mirrors
test_fallback_on_type_error but patches importlib.resources.files to raise
FileNotFoundError, calls vera.browser.emit._runtime_source_path(), and asserts
the returned Path-like object's name equals "runtime.mjs"; name it e.g.
test_fallback_on_file_not_found and use unittest.mock.patch to target
"importlib.resources.files" so the FileNotFoundError branch in
_runtime_source_path() is exercised.

In `@tests/test_checker.py`:
- Around line 4358-4372: The test test_handle_unknown_effect currently only
asserts len(diags) > 0 which is too weak; update it to assert that at least one
diagnostic produced by calling _check(...) about the handler contains the text
"NoSuchEffect" (or mentions NoSuchEffect) so the test specifically pins the
unknown-effect diagnostic rather than any unrelated message; locate the diags
variable returned by _check in test_handle_unknown_effect and replace/add an
assertion that any(d for d in diags if "NoSuchEffect" in d.message or
"NoSuchEffect" in str(d)) to ensure the intended error is covered.
- Around line 4098-4193: Each test that currently only asserts a warning (e.g.,
test_if_one_branch_none, test_if_then_unknown_returns_else,
test_if_else_unknown_returns_then and the other similar cases referenced) should
also assert that no errors were produced: after computing diags and deriving
warnings, add an errors = [d for d in diags if d.severity == "error"] and assert
not errors (or assert len(errors) == 0) so the test guarantees the path is
warning-only and not erroring or failing to recover the fallback type.
- Around line 4603-4623: The test uses the type name Type in the local
annotation mapping: dict[str, Type] but never imports it; add an import for Type
from vera.types (alongside FunctionType, PureEffectRow, TypeVar, PRIMITIVES) so
the annotation is defined and linters/type-checkers stop complaining; update the
import line that brings in FunctionType, PureEffectRow, TypeVar, PRIMITIVES to
also include Type.

In `@tests/test_cli.py`:
- Around line 1648-1662: The test function test_run_io_exit_code_non_json
currently declares an unused pytest fixture parameter capsys; remove capsys from
the test signature (def test_run_io_exit_code_non_json(self, tmp_path: Path) ->
None:) to eliminate the static-analysis warning, or if you intended to suppress
output, call capsys.readouterr() inside the test to consume output—update the
signature and any references accordingly to keep the test focused on asserting
rc == 7.

In `@tests/test_parser.py`:
- Around line 944-965: The current tests only assert that result.diagnostics and
result.summary are non-None; strengthen both tests to fail on regressions by
asserting there are no error diagnostics and the summary indicates success:
after calling verify_file (used in test_verify_file_valid and
test_verify_file_accepts_str_path), check that result.diagnostics contains zero
errors (or no entries indicating errors) and that result.summary reflects a
successful verification (e.g., zero reported errors / a success flag) instead of
just non-None values.

In `@tests/test_verifier_coverage.py`:
- Around line 22-58: The shared test helpers are too permissive: update _verify,
_verify_ok, and _verify_warn so type-check failures and error-level diagnostics
cannot be ignored. Modify _verify(source) to fail/assert if typecheck(ast,
source) reports any errors (raise or assert on type-check diagnostics) before
calling verify; change _verify_ok(source) to assert there are zero error or
warning diagnostics (not just errors); and change _verify_warn(source, match) to
assert there are no error diagnostics and at least one matching warning. Use the
function names _verify, _verify_ok, and _verify_warn to locate and apply these
stricter assertions.
- Around line 639-648: The test test_check_valid_unknown doesn't exercise the
unknown branch because using goal = z3.BoolVal(True) makes the solver
immediately unsat; change the test to stub/mock the underlying solver's check()
to return z3.unknown (e.g. patch the solver instance used by SmtContext or
monkeypatch SmtContext.check invocation) so that when invoking
SmtContext.check_valid(...) it yields a result whose status maps to "unknown",
and then assert result.status == "unknown"; reference SmtContext, check_valid,
and result.status when locating and updating the test.

In `@tests/test_wasm_coverage.py`:
- Around line 3745-3746: The test class named TestClosureCoverage duplicates an
earlier class with the same name and therefore shadows and disables the first
set of tests; rename the later class TestClosureCoverage (the one defined in
tests/test_wasm_coverage.py) to a unique name (e.g.,
TestClosureCoverageAdditional or TestClosureCoverageV2) so pytest will collect
both classes, and update any internal references to that class if present (look
for class TestClosureCoverage and its methods in that file to locate and rename
the correct definition).

---

Outside diff comments:
In `@TESTING.md`:
- Around line 172-194: Update the coverage table in TESTING.md so it matches the
PR description: change the `cli.py` and `parser.py` coverage entries to the new
reported values (e.g., 100% if the PR claims 68%→100% and 64%→100%), and adjust
any other module rows (like `wasm/` and `wasm/inference.py`) to reflect the
improved percentages noted in the PR; locate and edit the table rows containing
the module names `cli.py`, `parser.py`, `wasm/`, and `wasm/inference.py` to
replace the old numeric values with the updated coverage numbers and update the
Total row if required so the table consistently reflects the PR objectives.

Verify each finding against the current code and only fix it if needed.

Duplicate comments:
In `@tests/test_verifier_coverage.py`:
- Around line 639-648: The test test_check_valid_unknown is non-deterministic
because it relies on a timeout; update it to stub the underlying solver's
check() to return z3.unknown so it deterministically exercises
SmtContext.check_valid's mapping to "unknown": create a mock or monkeypatch of
the solver instance used by SmtContext (locate where SmtContext constructs/holds
the solver), make its check() method return z3.unknown, call
ctx.check_valid(goal, []), and assert result.status == "unknown" (instead of
allowing "verified"); reference SmtContext and its check_valid method to find
where to inject the stub.
- Around line 22-58: Update the shared helpers so type-check failures and
warnings can't hide verification regressions: modify _verify to fail
(raise/assert) if typecheck emits any errors before calling verify; change
_verify_ok to assert there are zero errors AND zero warnings in
result.diagnostics; and change _verify_warn to assert there are zero errors and
at least one warning matching match (rather than allowing mixed outcomes).
Reference the functions _verify, _verify_ok, and _verify_warn to locate and
implement these assertions.

Verify each finding against the current code and only fix it if needed.

Inline comments:
In `@TESTING.md`:
- Line 10: The top-line "Compiler code coverage" row is inconsistent with the
detailed table: update the headline row (the markdown line containing
"**Compiler code coverage**") to match the detailed coverage totals (the
detailed table total of 15,149 statements) and recompute the percent coverage
accordingly (or update the detailed table if the detailed total is stale),
ensuring both the percentage and "of X statements" values agree across
TESTING.md.

In `@tests/test_cli.py`:
- Around line 2262-2329: The three tests (test_test_failure_output,
test_test_failure_json, test_skipped_function_output) use nondeterministic/loose
assertions so formatting branches (FAILED/SKIPPED) aren't actually verified;
make them deterministic and assert the exact expected category: update
test_test_failure_output to use a failing fixture or fixed seed/trials and
assert the output contains "FAILED" (referencing cmd_test and the buggy_hash
source), update test_test_failure_json to run cmd_test(as_json=True) on a
deterministically failing input and assert the parsed JSON contains a failure
summary (e.g., data["functions"] includes a function with status "FAILED"), and
update test_skipped_function_output to assert the output contains "SKIPPED"
specifically for the IO-effect function (using the hello source and cmd_test)
rather than accepting any "Results:" line.
- Around line 1664-1679: The test test_run_runtime_trap_json currently only
asserts a generic failure; update it to force and verify the fallback
runtime-violation branch by asserting the JSON contains the specific runtime
diagnostic (e.g. that the top-level diagnostic/message or diagnostics array
includes the string "Runtime contract violation") in addition to rc == 1 and ok
== False; locate the test and the call to cmd_run(...) and add an assertion that
inspects the parsed data (data["diagnostic"] or data["diagnostics"] /
data["message"]) to confirm the distinct "Runtime contract violation" text is
present.

In `@tests/test_verifier_coverage.py`:
- Around line 595-599: The test currently ignores typecheck diagnostics and
calls verify() directly, which can hide type-check regressions; modify the test
around parse_to_ast/ typecheck/ verify so it first asserts that typecheck
produced no errors (e.g., inspect the diagnostics returned by typecheck(prog,
src, resolved_modules=[mod]) and fail if any error diagnostics exist) before
calling verify(), or replace the sequence with the provided test helpers
(_check_ok() followed by _verify_ok()) to enforce failing on type-check errors;
reference parse_to_ast, typecheck, verify, and the diagnostics list when making
the change.

In `@tests/test_wasm_coverage.py`:
- Around line 3784-3813: The test's closure never accesses the captured ADT
because the closure creates a fresh local `@Box` (used as `@Box.0`) instead of
the captured argument which, due to De Bruijn indexing, is at `@Box.1`; update
the test source in test_closure_capturing_adt so the closure body reads from the
captured `@Box` (e.g. reference/match `@Box.1` or otherwise use `@Box.1`'s
contents) so the captured ADT pointer is actually placed into the closure
environment — change the code in the make_box_fn closure (and any pattern-match
or return expression) to use the captured `@Box` (symbol: make_box_fn, closure
body, variable `@Box`) instead of the fresh local `@Box.0`.

---

Duplicate comments:
In `@tests/test_checker.py`:
- Around line 4098-4113: Update the listed tests (test_if_one_branch_none,
test_match_scrutinee_none, test_match_arm_unknown,
test_unknown_constructor_pattern, test_unknown_nullary_pattern) to assert that
diagnostics contain zero errors in addition to the existing warning checks:
after collecting diags, add an assertion that no diag has severity == "error"
(e.g. assert not any(d.severity == "error" for d in diags)), preserving the
current warnings predicate; apply the same zero-error assertion pattern to the
other test blocks noted in the review so these recovery-path tests ensure
warning-only behavior.

In `@tests/test_parser.py`:
- Around line 958-968: The test test_verify_file_accepts_str_path should assert
the zero-error path for the string overload of verify_file: after calling
verify_file(str(src)) check both result.summary (e.g., result.summary is not
None and result.summary.total == 0) and that result.diagnostics is empty (e.g.,
len(result.diagnostics) == 0 or result.diagnostics == []) so the test fails if
verification emits errors in the str-path branch; update the assertions to
include these checks referencing verify_file, result.summary, and
result.diagnostics.

In `@tests/test_verifier_coverage.py`:
- Around line 649-665: The test test_check_valid_unknown is vacuous because it
accepts every status; replace the timeout probe with a deterministic stubbed
solver so check_valid returns "unknown" and assert that exactly. Modify the test
to inject a fake/monkeypatched solver into SmtContext (or into ctx) that
simulates Z3 returning an "unknown" result for the given goal, call
ctx.check_valid(goal, []) and assert result.status == "unknown"; ensure you
reference and override the concrete solver interface used by
SmtContext/check_valid so the test is deterministic and does not rely on timing.

Verify each finding against the current code and only fix it if needed.

Inline comments:
In `@TESTING.md`:
- Around line 172-193: The coverage table in TESTING.md has an off-by-one in the
statements total: the module rows sum to 15,149 but the Total row shows 15,150;
run the real coverage report (pytest --cov=vera) to confirm the correct overall
statement count, then update either the individual module row that is wrong (one
of the module "Stmts" values such as codegen/, checker/, wasm/, etc.) or correct
the Total row to match the sum, ensuring the Module rows sum and the Total
"Stmts" value are consistent.

In `@tests/test_cli.py`:
- Around line 1765-1795: test_fn_name_filter and test_trials_display lack
meaningful assertions: update test_fn_name_filter (which calls
cmd_test(SAFE_DIVIDE, fn_name="safe_divide")) to assert the output specifically
indicates the safe_divide function was selected (e.g. contains "safe_divide" or
"Testing: safe_divide") and does not list other functions; update
test_trials_display (which calls cmd_test(str(path), trials=5)) to assert the
trials summary appears and reflects the requested count (e.g. contains "Trials:"
and a mention of 5 trials or "5") so the fn-name filter and trial-summary
branches are actually exercised.

In `@tests/test_verifier_coverage.py`:
- Around line 568-612: The test test_pipe_to_module_call currently discards the
pipe-form fixture and only exercises util::inc(`@Int.0`); restore coverage by
using the parsed pipe source (src) for typecheck() and verify() instead of
src_direct (i.e. don't reassign prog = parse_to_ast(src_direct) and pass
prog/src to typecheck and verify), and if the known module-qualified pipe arity
bug triggers, avoid module-qualified callee by importing the symbol into scope
and switching the pipe call to inc() (e.g. make the call `@Int.0` |> inc()) so the
pipe desugaring path is actually exercised for parse_to_ast/typecheck/verify
with util::inc present.

---

Duplicate comments:
In `@tests/test_cli.py`:
- Around line 2265-2319: The tests test_test_failure_output and
test_test_failure_json are not asserting the CLI failure results: update
test_test_failure_output to assert that cmd_test(...) returned 1 (rc == 1) to
catch summary.failed > 0, and update test_test_failure_json to stop checking for
a non-existent "failed" category and instead assert the JSON uses failure fields
(e.g., data["summary"]["failed"] > 0 or data.get("trials_failed", 0) > 0 or
len(data.get("failures", [])) > 0); reference the test helpers cmd_test and the
JSON fields summary.failed, trials_failed, failures so the tests accurately
detect failures reported by the CLI.

In `@tests/test_verifier_coverage.py`:
- Around line 1065-1079: The test test_verify_with_empty_source calls
typecheck(prog, "") but doesn't assert that typechecking succeeded, so a
regression could mask type errors; update the test to capture the typecheck
result (from typecheck(prog, "")) and assert that it has no diagnostics with
severity "error" (or otherwise assert typecheck success) before calling
verify(prog, ""), ensuring the verifier is exercised only when the program is
typechecked.
- Around line 662-679: The test test_check_valid_unknown is nondeterministic;
instead of relying on a 1ms timeout produce a deterministic 'unknown' by
stubbing the solver and then assert the exact mapping. In
tests/test_verifier_coverage.py modify test_check_valid_unknown to monkeypatch
or patch SmtContext's underlying solver check (or SmtContext.check_valid) so it
returns z3.unknown (or a z3 check result that maps to 'unknown'), then call
ctx.check_valid(goal, []) and assert result.status == "unknown"; keep references
to SmtContext, test_check_valid_unknown and the check_valid mapping so the
change is local and explicit.

Verify each finding against the current code and only fix it if needed.

Inline comments:
In `@tests/test_verifier_coverage.py`:
- Line 47: The assertion uses an unnecessary f-string: replace the f-string in
the assertion (the line asserting errors: "assert errors, f\"Expected at least
one error, got none\"") with a plain string literal so the message is not an
f-string (e.g., change to "assert errors, 'Expected at least one error, got
none'") to avoid Ruff F541; update the assertion in
tests/test_verifier_coverage.py where the failing check is made.

---

Duplicate comments:
In `@tests/test_cli.py`:
- Around line 1765-1797: Update the two tests to assert specific, unambiguous
output: in test_fn_name_filter (which calls cmd_test(SAFE_DIVIDE,
fn_name="safe_divide")), assert that the output contains "safe_divide" and does
NOT contain other function names (or assert the filtered-list header equals
"safe_divide") so the function filter is actually enforced; in
test_trials_display (which writes clamp.vera and calls rc = cmd_test(str(path),
trials=5)), assert the output explicitly reflects the requested trial count
(e.g., contains "trials: 5", "5 trials", or shows 5 attempts for clamp) and that
clamp appears exactly in the processed-results section so the trial-count
rendering and function processing are verifiably correct.

In `@tests/test_verifier_coverage.py`:
- Around line 651-667: The test test_check_valid_unknown currently accepts any
status and thus doesn't verify the unknown branch; update the test to
deterministically force the solver to return unknown by stubbing/monkeypatching
the solver's check method used by SmtContext (e.g., patch the SmtContext
instance's internal solver.check or z3.Solver.check to return z3.z3.L_UNKNOWN /
z3.unknown), call ctx.check_valid(goal, []), and assert result.status ==
"unknown" (use the SmtContext and check_valid symbols to locate where to stub
and to verify the result).