A strategic-mode review on 2026-05-18 surfaced 6 findings.  All 6
independently verified against HEAD (v0.0.155, commit 08c1197).
This PR addresses the docs half — code fixes land separately
under the filed issues.

## What changed

**README.md** — softened the "Contracts the compiler proves"
section.  The previous wording ("Division by zero is not a runtime
error — it is a type error.  The compiler checks every call site
to prove the divisor is non-zero.") overclaimed: the verifier
checks contracts the programmer wrote, not auto-synthesised
obligations on primitive operations.  New wording correctly
describes what's static (declared preconditions discharged at
every call site) and what's runtime (unguarded primitives trap
with Vera-native diagnostic), with a forward reference to #680
which tracks the implementation work to make the original claim
true.

**FAQ.md** — new Q&A "Does the compiler prove division-by-zero,
out-of-bounds indexing, etc. can't happen?".  Explicitly walks
through the static/runtime split, references the #520 Nat-
subtraction precedent (the one auto-synthesised obligation that
exists today), and points at #680 + #427 as the long-term path.

**spec/06-contracts.md** — new §6.4.3 "Primitive Operation Safety"
between Call Site Verification and SMT Solver Integration.  States
explicitly that obligations on `a / b`, `a % b`, `arr[i]`,
`string_at(s, i)`, etc. are not auto-synthesised; the exception
is `@Nat` subtraction (#520).  Cross-references #680 and #427.
Subsequent sections re-numbered (§6.4.4 SMT Solver Integration,
§6.4.5 Counterexample Reporting — was §6.4.3 and §6.4.4).

**KNOWN_ISSUES.md** — restored the Bugs section with #681 (`vera
test` reports refuted functions as VERIFIED).  This was confirmed
by the review with a clean reproducer:

  `vera verify` correctly emits E500 with counterexample, but
  `vera test` reports the buggy function as `VERIFIED (Tier 1)`
  with exit code 0.

The classifier at `vera/tester.py:393` only harvests
`severity == "warning"` Tier 3 codes; `severity == "error"`
codes flow past untouched.  Workaround documented: run
`vera verify` before trusting `vera test` results.  Fix is half
a day's work, landing separately.

**ROADMAP.md** — three new tracking items added under CI tooling
(#682 diagnostic-tagging discipline, #683 grammar drift), one
under verification depth (#680 auto-inject primitive obligations),
one under testing gaps (#679 Chapter 8 conformance programs).

**Auxiliary**:
- `scripts/check_faq_examples.py` and `scripts/check_spec_examples.py`
  allowlist line numbers updated (auto-fixed via
  `python scripts/fix_allowlists.py --fix`) — the Abilities snippet
  in FAQ shifted by ~11 lines from the new Q&A insertion; the spec
  example in §6.4.5 shifted from line 323 to 338 from the new §6.4.3.
- Site assets regenerated (`docs/llms-full.txt`, `docs/sitemap.xml`).

## Findings deferred from this PR

| Finding | Status |
|---|---|
| **P0-1** (`vera test` mis-classification) | #681 filed; documented in KNOWN_ISSUES.md; fix is a separate ~half-day PR |
| **P1-1** (diagnostic tagging) | #682 filed; ROADMAP entry added; multi-day mechanical work scoped for a follow-up PR |
| **P1-2** (Ch 8 conformance) | #679 filed; ROADMAP entry added; ~day of work |
| **P2-1** (grammar drift) | #683 filed; scoped to nominal renames only (expression-precedence ladders are deliberate notational difference) |
| **P2-2** (Tier 2 / `invariant()` strategic call) | Tier 2 (#427) genuinely long-running; `invariant()` doc-state already resolved by PR #650.  Strategic call deferred — flagged to Alasdair for direction. |

## Validation

- [x] `pytest tests/` — 3,875 passed, 14 skipped, 16 stress-deselected
- [x] `python scripts/check_conformance.py` — 86/86
- [x] `python scripts/check_examples.py` — 34/34
- [x] `python scripts/check_doc_counts.py` — consistent
- [x] `python scripts/check_limitations_sync.py` — consistent (30 in KNOWN_ISSUES, 18 in vera/README, 4 across spec)
- [x] `python scripts/check_readme_examples.py` — pass
- [x] `python scripts/check_faq_examples.py` — pass (after allowlist update)
- [x] `python scripts/check_spec_examples.py` — pass (after allowlist update)
- [x] `python scripts/check_skill_examples.py` — pass
- [x] `python scripts/check_site_assets.py` — up-to-date

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

External contributor @rzyns filed two careful reports on 2026-05-15
(#674 and #675).  This commit addresses #675 inline with the
existing docs PR (#684) and reassigns the KNOWN_ISSUES.md entry
from #681 to #674 (my dupe of #674 from today's compiler-review
sweep — closed as duplicate).

## #675 — E500 fix text names all three repair classes

Pre-fix `fix=` text at `vera/verifier.py:1306-1308` named only
two repair classes: strengthen `requires(...)` or weaken
`ensures(...)`.  It missed the third (often most common) class:
fix the implementation to satisfy the existing contract.  When
E500 catches a typo in the function body (e.g. `@Int.0 + @Int.0
+ 1` when the contract says `@Int.0 + @Int.0`), the user's
intended repair is almost always "fix the typo" — the previous
wording implicitly biased them toward weakening the contract
instead.

New wording lists all three repair classes neutrally:

> Resolve the mismatch between the function body and its
> contract: fix the implementation so it satisfies this
> ensures() clause, strengthen requires(...) if the
> counterexample is outside the intended input domain, or
> weaken/change ensures(...) if the postcondition overstates
> the intended guarantee.

Implementation-repair comes first because it's the most
common case in practice; the verifier is otherwise neutral
about which artifact is "the source of truth".

Tightened `tests/test_verifier.py::TestCounterexamples::
test_violation_has_fix_suggestion` to assert all three
classes appear in the lowercased fix text.  The pre-existing
assertion (`"precondition" or "postcondition" in fix.lower()`)
survives the rewrite but would not have caught a regression
dropping "implementation"; the new assertion does.

Closes #675.

## #674 / #681 reassignment

#674 was filed by @rzyns on 2026-05-15 reporting that `vera
test --json` reports `category: "verified"` for functions the
verifier has refuted with E500.  I filed the same bug as #681
today (2026-05-18) from a strategic compiler-review session
without realising #674 existed.

#681 is closed as a duplicate; the `KNOWN_ISSUES.md` Bugs entry
now references #674 with a polished reproducer (@rzyns's
`@Int + @int + 1` form is cleaner than my `@Nat * 2 + 1`) and
explicit mention of the CI-consumes-JSON failure mode.

The underlying bug remains open; the fix is a separate code
PR (half a day's work — extend `vera/tester.py::_classify_
functions` to harvest `severity == "error"` codes too, add
a `"failed"` category, set non-zero exit code).

## Validation

- [x] `pytest tests/test_verifier.py::TestCounterexamples::test_violation_has_fix_suggestion -v` passes
- [x] `pytest tests/` — 3,875 passed, 14 skipped, 16 stress-deselected
- [x] `mypy vera/` clean
- [x] `ruff check --select S vera/` clean
- [x] `check_doc_counts.py`, `check_limitations_sync.py`, `check_readme_examples.py`, `check_faq_examples.py`, `check_spec_examples.py`, `check_site_assets.py` all consistent
- [x] TESTING.md test_verifier.py line count: 2,094 → 2,124

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

CI's check_changelog_updated.py correctly flagged that PR #684
touches vera/verifier.py and spec/06-contracts.md without a
matching CHANGELOG.md entry.

Adds an [Unreleased] section covering:

- Fixed: #675 E500 fix-text rewording (external report from @rzyns)
- Documentation: the 2026-05-18 compiler-review docs sweep
  (README softening, FAQ Q&A, spec section 6.4.3, KNOWN_ISSUES
  #674 reassignment, ROADMAP additions for #679/#680/#682/#683)

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