docs(337): make the verification claim accurate (relabel + narrow)

[avrabe]

Corrects the README verification claim to match the actual evidence (the claim-verification "relabel-and-gate" pattern #337 asks for). Grounded in proofs/STATUS.md and meld-core/src/abi_proofs.rs.

Why the old claim overstated

• Flat always-green Formally_Verified badge — unlinked, reflects no job.
• "Every transformation carries mechanized proofs covering parsing, resolution, merging, and adapter correctness" — but the coverage matrix shows parser / rewriter / segments / attestation are placeholders, orchestration is unproven, semantic preservation is a forward simulation only, and one FACT adapter lemma is Admitted.
• Kani harnesses are VERIFICATION SUCCESSFUL locally (SR-40), not gated in CI (shared runners lack the Kani toolchain); ABI size/align + aggregate-padding contracts fell back to unit tests.

What changed (all README)

• Badge → linked Formal_Methods: Rocq + Kani (partial) → #formal-verification (informational, not a false CI-gate).
• Tagline → narrowed to the core stages actually proven, with a scope caveat + link.
• Formal Verification section → rewritten to state the 350 closed Rocq proofs honestly: real/substantial on resolver·merger·adapter·spec, but not whole-pipeline; forward-simulation only; the one Admitted lemma called out; Kani local-not-CI; unit-test fallback noted. Links proofs/STATUS.md.

This neither over- nor under-sells — it credits the genuine 350-proof body of work while scoping it accurately.

Not addressed here

#337(b) — gating the converging Kani harnesses in CI — needs the Kani toolchain on the shared smithy runners (an infra change), so it's a follow-up, not this docs PR.

Refs #337.

🤖 Generated with Claude Code

[github-actions]

LS-N verification gate

✅ 59/59 approved LS entries verified

	count
Passed (≥1 test, all green)	59
Failed (≥1 test failure)	0
Missing (no ls_*_NN_* test found)	0

_{Approved loss-scenarios.yaml entries are expected to have a
regression test named ls_<letter>_<num>_* (e.g. LS-A-11 →
ls_a_11_*). The gate runs each prefix via cargo test --lib --no-fail-fast and aggregates pass/fail/missing.}

Failed LS entries

(none)

Missing regression tests

(none)

_{Updated automatically by tools/post_verification_comment.py.
Source of truth: safety/stpa/loss-scenarios.yaml.}