content/_index.md sets the site-wide description to "The formally verified WebAssembly Component Model engine for safety-critical systems." The "engine" is the kiln WASM core, which carries zero formal proofs (see the kiln audit, pulseengine/kiln#423). The real, scoped formal verification in the toolchain lives in other components — ordeal (Lean-checked LRAT checker), spar (Lean scheduling proofs), gale/relay (Verus/Kani/Lean) — not the engine.
As the org's top-level public claim, this is the highest-visibility overclaim: it flattens component-level proofs into a blanket "the engine is formally verified." Suggest scoping the tagline to what is actually proven — e.g. "a WebAssembly toolchain with formally verified components," or name the verified pieces. (The identical phrase also appears as a footer in spar's README.)
🤖 Filed via Claude Code as part of the org-wide verification-claim honesty audit (follows pulseengine/kiln#423). Root: pulseengine/.github#8
content/_index.mdsets the site-widedescriptionto "The formally verified WebAssembly Component Model engine for safety-critical systems." The "engine" is the kiln WASM core, which carries zero formal proofs (see the kiln audit, pulseengine/kiln#423). The real, scoped formal verification in the toolchain lives in other components — ordeal (Lean-checked LRAT checker), spar (Lean scheduling proofs), gale/relay (Verus/Kani/Lean) — not the engine.As the org's top-level public claim, this is the highest-visibility overclaim: it flattens component-level proofs into a blanket "the engine is formally verified." Suggest scoping the tagline to what is actually proven — e.g. "a WebAssembly toolchain with formally verified components," or name the verified pieces. (The identical phrase also appears as a footer in spar's README.)
🤖 Filed via Claude Code as part of the org-wide verification-claim honesty audit (follows pulseengine/kiln#423). Root: pulseengine/.github#8