README: flat "Formally Verified" badge overstates un-gated, partial Kani evidence

[avrabe]

The README carries a static green Formally_Verified shields badge and the tagline "Every transformation carries mechanized proofs covering parsing, resolution, merging, and adapter correctness."

meld genuinely has Kani harnesses on meld-core (resolver, merger, abi, parser) — real work, and unlike kiln these proofs are on the core. But three things falsify the flat badge as written:

1. the badge is unlinked and always-green — it reflects no job;
2. Kani runs in no CI workflow — meld-core/src/abi_proofs.rs itself notes "Not yet in CI — the smithy runners do not ship the Kani toolchain; recorded in SR-40 as local-evidence verification";
3. "every transformation … parsing" is contradicted by that same file's documented scope cuts, where the canonical-ABI size/alignment and aggregate-padding contracts did not converge in CBMC and fell back to unit tests.

This is a relabel-and-gate, not a "you have no proofs": (a) replace the flat badge with a technique-named, CI-linked one (e.g. "Kani BMC" pointing at a real gating job), (b) gate the converging harnesses in CI, (c) narrow the tagline from "every transformation" to the subset actually proven. See kiln#423 for the claim-check pattern.

---

🤖 Filed via Claude Code as part of the org-wide verification-claim honesty audit (follows pulseengine/kiln#423). Root: pulseengine/.github#8

[avrabe]

Disposition: the badge/tagline honesty asks are already satisfied in the current README; the remainder is infra-blocked

Re-checked the current README.md against the three asks — grounded by line:

• (a) flat always-green Formally_Verified badge → technique-named + qualified: DONE. Line 15 is
  [![Formal Methods](…Formal_Methods-Rocq_%2B_Kani_(partial)…)](#formal-verification) — technique-named (Rocq + Kani), explicitly (partial), and linked (to the Formal Verification section). No flat "Formally Verified" badge remains.
• (c) narrow "every transformation … parsing": DONE. Line 38 now scopes the claim to "the core transformations — resolution, index-space merging, and adapter generation," and states outright that "some stages are specified but not yet proved, and the Kani harnesses are run locally, not gated in CI." Lines 161/169 carry the honest per-stage matrix, the Kani-not-in-CI note, and the CBMC-non-convergence → unit-test fallback.
• (b) gate the converging Kani harnesses in CI + link the badge to that job: NOT done, and blocked on infra — the shared smithy runners do not ship the Kani toolchain (SR-40 records this as local-evidence verification; the README documents it at line 169). The badge therefore links to the honest section rather than a (non-existent) gating job. This unblocks only when a Kani-capable runner is available.

So the overstatement this issue was filed against no longer exists in the README; the residual is the CI-gating, which is an infra dependency, not a wording fix.

One optional residual: the footer (line 227) still reads "PulseEngine — formally verified WebAssembly toolchain," an org-level descriptor. If the org-wide honesty audit wants that softened too, it's a one-line change — but it's an org tagline, so flagging rather than changing it unilaterally.

Suggest: narrow this issue to "(b) gate Kani in CI once a Kani-capable runner exists", or close as addressed with (b) tracked under the Kani-in-CI infra dependency.