Fail closed when `vera test` sees E500/E501/E502 verifier diagnostics instead of reporting verifier-refuted contracts as successful Tier 1 results.

Preserve verifier diagnostics in JSON, return ok=false with a nonzero exit, and show human diagnostics so private, unselected, or otherwise non-displayed verifier failures cannot disappear.

Attribute E501 call-site precondition failures to the caller while preserving E500/E502 attribution, keep --fn rows filtered while whole-file verifier errors still fail closed, and distinguish static verifier failures from Tier 3 E700 runtime failures in human summaries.

Add regression coverage for JSON and human output, private helper failures, --fn fail-closed diagnostics, E501 caller attribution, E502 underflow attribution, mixed static/Tier 3 summaries, E700 runtime failures, multiple diagnostics on one displayed failed function, and CLI dispatch return codes.

CodeRabbit posted three findings on rzyns's PR plus there's a CI
gate (doc-counts) and a project convention (empty Bugs table) to
address.  Two additional minor refactors (DRY constant, public
helper rename) included since they touch the same files.

**CR Finding 1: _bad_vera missing encoding="utf-8"** (test
portability).  Pre-existing helper used 30+ times in test_cli.py
since long before aallan#685, but CR caught it now because rzyns's new
tests added more callers.  Windows runs would fall back to cp1252
on the default text-mode encoding and corrupt UTF-8 sequences in
Vera fixtures.  CLAUDE.md "Cross-platform pitfalls" already flags
this as a convention.  One-line fix on the helper benefits every
caller.

**CR Finding 2: needs_pos.category != "failed" too weak**
(test_tester.py).  In `test_call_precondition_error_fails_caller_
not_callee`, the negative assertion would still pass if needs_pos
were classified as "skipped" or any other non-failed bucket.
Strengthened to `== "verified"` so the test actually pins that the
callee is correctly proven, not just that it avoided the failed
bucket.

**CR Finding 3: failed_fns dict overwrite is order-dependent**
(vera/tester.py).  When a single function attracts multiple
verifier errors (e.g. `ensures(false)` produces E500 AND
`@Nat - @Nat` produces E502 on the same body — the
`test_displayed_failed_function_does_not_double_count_verifier_
errors` test exercises exactly this shape), the loop overwrites
the dict entry and the displayed `reason` flips with diagnostic
iteration order.  Switched to first-hit (`if name not in
failed_fns`) — `setdefault`-style semantics, no judgement call on
which code "should" win.

**Doc counts: 7 stale numbers** (CI gate would fail).
`check_doc_counts.py` flagged TESTING.md total, test_cli.py +
test_tester.py + test_tester_coverage.py rows, and ROADMAP.md
test count.  Updated all 7 plus README.md test count for
consistency: 3,905 → 3,916 total.  All counts now consistent.

**KNOWN_ISSUES.md empty table** (project convention).  PR
removed the aallan#674 row but left the table header `| Bug | Issue |`
with no body.  Per the convention established at aallan#673's release
("retain the Bugs section, and just have some text in it to say
'No known bugs'"), replaced the empty table with the convention
line.

**Nit 1: DRY** — `{"E500", "E501", "E502"}` was duplicated
between vera/tester.py and vera/cli.py.  Extracted as
`VERIFICATION_ERROR_CODES = frozenset(...)` module-level in
vera/tester.py; cli.py imports it.  `frozenset` over plain set so
the constant is immutable (matches its semantic role as a
classifier-set constant).

**Nit 2: private name reaching across modules** — `cli.py` was
importing `_failed_function_name` from vera/tester.py.  The
single-underscore prefix signals "private by convention" but
cli.py's reliance on it was a leak.  Renamed
`_failed_function_name` → `failed_function_name` (public);
docstring updated to mention the cli.py call site explicitly.

Validation:
- pytest 3,886 / 3,886 (no test count change — the renames don't
  affect test behaviour, just the names)
- mypy clean
- ruff S clean
- conformance 86/86, examples 34/34
- check_doc_counts.py consistent
- limitations sync consistent
- check_changelog_updated.py passes (existing [Unreleased] entry
  from rzyns's commit + the additional carry-over from PR aallan#684)
- check_site_assets.py up-to-date

Co-Authored-By: Claude <noreply@anthropic.invalid>

CR's two new comments after my cleanup commit:

**Finding 1: missing text-mode sibling for the --fn filter test**
(test_cli.py).  `test_fn_filter_surfaces_unselected_verifier_
error` covered the JSON path but not the human/text path — both
codepaths can drift independently (text rendering has its own
diagnostics section, summary line, unlisted-error counter), so
the JSON-only coverage left a real gap.

Added `test_fn_filter_surfaces_unselected_verifier_error_text`
mirroring the JSON test for human output: asserts the displayed
function list stays scoped to `identity` (per `--fn`), `broken`'s
verifier error still surfaces in the Diagnostics section, the
summary line names the unlisted verifier error, and the exit
code is 1.

**Finding 2: classifier internals exported for CLI-only use**
(vera/tester.py).  Last round I dropped the underscore from
`_failed_function_name` so cli.py could import it across the
module boundary.  CR pushed back: those exports (along with
`VERIFICATION_ERROR_CODES`) are CLI-only bookkeeping and don't
belong on `vera.tester`'s public surface.

Three options from CR:
- (a) Privatise the exports — cli.py keeps reaching across the
  underscore boundary
- (b) Move the logic into a CLI-only shared helper
- (c) Expose the computed value as structured data on
  TestResult/TestSummary so cli.py reads it as a field

Went with (c) — it's the cleanest because the only thing cli.py
needed the exports for was a single count (verifier errors
whose target function isn't in the displayed list).  Adding
`unlisted_errors: int = 0` to TestSummary, computing it in the
engine after the main loop, and reading it as
`s.unlisted_errors` in cli.py makes vera/cli.py purely
presentational — no logic, no regex, no classifier internals.
The engine returns the canonical answer and the formatter just
renders it.

Specifically:
- `vera/tester.py::TestSummary` gains `unlisted_errors: int = 0`
- `vera/tester.py::_TestEngine.run()` computes
  `summary.unlisted_errors` before returning by counting
  verifier-error diagnostics whose attributable function isn't
  in the `displayed_failed` set derived from `results`
- `VERIFICATION_ERROR_CODES` → `_VERIFICATION_ERROR_CODES`
  (private; only the engine uses it now)
- `failed_function_name` → `_failed_function_name` (private;
  only the engine uses it now)
- `vera/cli.py` drops the imports + the local `displayed_failed`
  set + the `sum(...)` comprehension; just reads
  `s.unlisted_errors` directly
- JSON output gains `"unlisted_errors": s.unlisted_errors` in
  the summary dict for downstream CI consumers
- `test_fn_filter_surfaces_unselected_verifier_error` (JSON)
  now also asserts `data["summary"]["unlisted_errors"] == 1`
  to pin the new structured field

This is option (c) — the principled long-term shape.  Option
(a) (which I did last round) was the minimum-touch fix but
left `vera.tester`'s public API leaking implementation details
the CLI happened to need.  CR is right that (c) is the better
contract.

Validation: pytest 3,887 / 3,887 (one new test for Finding 1),
mypy clean, ruff S clean, conformance 86/86, examples 34/34,
doc-counts consistent (3,916 → 3,917 total; test_cli.py
225 → 226 tests, 3,250 → 3,300 lines).

Co-Authored-By: Claude <noreply@anthropic.invalid>