Summary
The org profile profile/README.md displays a static, always-green
badge next to the tagline Formally verified WebAssembly toolchain for safety-critical systems.
The badge links to nothing and reflects no gate — it asserts a uniform, org-wide, completed verification status that no single artifact backs, and that is not true of the toolchain as a whole. This is the same failure mode an external formal-verification reviewer (relayed via Christof Petig) flagged on kiln's README (fixed in pulseengine/kiln#423), one level up.
Why this is the root
This profile is the single source of the "formally verified WebAssembly toolchain for safety-critical systems" tagline that ~9 tooling/example repos echo verbatim in their footers. Fixing it here is the highest-leverage correction — the echoes (tracked in sibling issues) are downstream of this string.
What's actually true (so the fix is precise, not blanket removal)
The toolchain has real, scoped formal verification in specific components — gale (Verus+Rocq+Lean, CI-gated, with a disclosed trust ledger), relay (Kani as a required merge gate), ordeal (Lean-checked LRAT checker, zero sorry), loom (per-run Z3 translation validation), spar (Lean scheduling theorems). The problem is flattening those distinct, partial, component-level results into one green org-wide checkmark.
Suggested fix
- Drop the flat
Formally_Verified badge. Keep the accurate per-tool NOTE (Rocq / Kani / Z3 / Verus / Lean) that already names techniques.
- If a tagline stays, make it describable and honest — either an aspiration ("building a formally verified WebAssembly toolchain…") or name the components that actually back it ("…with formally verified components").
- Consider adopting the pattern from kiln#423: a claim-check gate + CI-published evidence so the org-level claim can't drift.
🤖 Filed via Claude Code as part of the org-wide verification-claim honesty audit (follows kiln#423).
Summary
The org profile
profile/README.mddisplays a static, always-greenbadge next to the tagline
Formally verified WebAssembly toolchain for safety-critical systems.The badge links to nothing and reflects no gate — it asserts a uniform, org-wide, completed verification status that no single artifact backs, and that is not true of the toolchain as a whole. This is the same failure mode an external formal-verification reviewer (relayed via Christof Petig) flagged on kiln's README (fixed in pulseengine/kiln#423), one level up.
Why this is the root
This profile is the single source of the "formally verified WebAssembly toolchain for safety-critical systems" tagline that ~9 tooling/example repos echo verbatim in their footers. Fixing it here is the highest-leverage correction — the echoes (tracked in sibling issues) are downstream of this string.
What's actually true (so the fix is precise, not blanket removal)
The toolchain has real, scoped formal verification in specific components —
gale(Verus+Rocq+Lean, CI-gated, with a disclosed trust ledger),relay(Kani as a required merge gate),ordeal(Lean-checked LRAT checker, zerosorry),loom(per-run Z3 translation validation),spar(Lean scheduling theorems). The problem is flattening those distinct, partial, component-level results into one green org-wide checkmark.Suggested fix
Formally_Verifiedbadge. Keep the accurate per-tool NOTE (Rocq / Kani / Z3 / Verus / Lean) that already names techniques.🤖 Filed via Claude Code as part of the org-wide verification-claim honesty audit (follows kiln#423).