The claim
Seven live repositories still carry this footer:
Part of PulseEngine — formally verified WebAssembly toolchain for safety-critical systems
meld · sigil · spar · temper · rules_verus · wasm-component-examples · template-mcp-server
It is the same flat claim already corrected in three places: the site description (#121 / #127), the mcp README (mcp#101), and the org profile page (.github#9). These seven are what remains.
Why it matters more than a wording nit
The toolchain as a whole is not formally verified, and saying so unprompted is the fastest way to lose a formal-methods reader. What is true is specific and defensible: ordeal's Lean-checked LRAT checker, scry's mechanized Rocq soundness, spar's Lean scheduling proofs, gale/relay's Verus + Rocq + Kani properties, loom's per-run translation validation.
The footer flattens all of that into a badge. It is also on repos that carry no proofs at all — template-mcp-server and wasm-component-examples are scaffolding and examples — which is where it overclaims hardest and is least defensible.
Our own claim-verification skill names this exact anti-pattern:
Copy-pasting a shared claim (the org tagline) into every repo where it drifts — single-source it.
Two ways to do it
A. Fix the string, seven times. Replace with the wording already adopted elsewhere:
Part of PulseEngine — a WebAssembly toolchain for safety-critical systems, with formally verified components
Cheap, mechanical, and it can ship today.
B. Single-source it, then fix once. The footer exists in ~10 places because it was copy-pasted; the same will happen again with the next shared string. Options: a temper-enforced snippet (temper already holds repos to org standards and applied the branch-protection ruleset), or a claim-check predicate that fails CI when a repo's footer diverges from the recorded org wording.
Recommendation: A now, B as the follow-up. Seven repos is small enough to fix by hand today, and leaving the overclaim live while designing a mechanism is the wrong trade. But A alone guarantees a third round of this later.
Kill-criterion
grep -rl "formally verified WebAssembly toolchain" across all non-archived org repos returns nothing, and a claim-check predicate keeps it that way.
Note on archived repos
wasi-mcp, timedate-mcp and moonbit_checksum_updater also carry the footer but are archived and therefore read-only. Leaving them is the right call — unarchiving to edit a footer is churn, and an archived repo is understood as a historical record.
🤖 Filed during an org-wide repository reassessment.
The claim
Seven live repositories still carry this footer:
meld·sigil·spar·temper·rules_verus·wasm-component-examples·template-mcp-serverIt is the same flat claim already corrected in three places: the site description (#121 / #127), the
mcpREADME (mcp#101), and the org profile page (.github#9). These seven are what remains.Why it matters more than a wording nit
The toolchain as a whole is not formally verified, and saying so unprompted is the fastest way to lose a formal-methods reader. What is true is specific and defensible: ordeal's Lean-checked LRAT checker, scry's mechanized Rocq soundness, spar's Lean scheduling proofs, gale/relay's Verus + Rocq + Kani properties, loom's per-run translation validation.
The footer flattens all of that into a badge. It is also on repos that carry no proofs at all —
template-mcp-serverandwasm-component-examplesare scaffolding and examples — which is where it overclaims hardest and is least defensible.Our own
claim-verificationskill names this exact anti-pattern:Two ways to do it
A. Fix the string, seven times. Replace with the wording already adopted elsewhere:
Cheap, mechanical, and it can ship today.
B. Single-source it, then fix once. The footer exists in ~10 places because it was copy-pasted; the same will happen again with the next shared string. Options: a
temper-enforced snippet (temper already holds repos to org standards and applied the branch-protection ruleset), or aclaim-checkpredicate that fails CI when a repo's footer diverges from the recorded org wording.Recommendation: A now, B as the follow-up. Seven repos is small enough to fix by hand today, and leaving the overclaim live while designing a mechanism is the wrong trade. But A alone guarantees a third round of this later.
Kill-criterion
grep -rl "formally verified WebAssembly toolchain"across all non-archived org repos returns nothing, and aclaim-checkpredicate keeps it that way.Note on archived repos
wasi-mcp,timedate-mcpandmoonbit_checksum_updateralso carry the footer but are archived and therefore read-only. Leaving them is the right call — unarchiving to edit a footer is churn, and an archived repo is understood as a historical record.🤖 Filed during an org-wide repository reassessment.