docs(verification): honest, gated verification claims (drop "Formally Verified" overclaim) - #423
Merged
Merged
Conversation
… honest evidence External formal-verification review (Conrad Watts, relayed via Christof Petig) flagged kiln's flat green "Formally Verified" badge as an overclaim: the WebAssembly interpreter core (kiln-runtime / kiln-instructions / kiln-decoder / kiln-component) carries ZERO formal proofs — it is conformance-tested and unit-tested, not mechanically proven. The Kani harnesses that DO exist are on peripheral utility crates. The claim could not be backed as written. This replaces the claim with what the evidence actually supports, and binds it so it cannot drift again: - README: drop the flat "Formally Verified" badge and the Rocq/Z3/Verus "Formal Verification" note; add an honest "Verification & correctness" section. Lead with the un-spoofable file ratio — 261/280 spec-suite files (93.2%) — because a file that fails to *parse* (custom-descriptors) contributes zero assertions to the 99.98%-of-executed-assertions figure and would otherwise hide. State plainly: the interpreter's semantics are not formally proven. - Spec-suite badge is now a shields.io ENDPOINT badge re-derived by CI from the live suite result (tools/spec-badge.py), never hand-typed — it cannot drift. - claims.yaml + tools/claim-check.py: gate the doc claims against source. The gate re-counts that the interpreter core has 0 #[kani::proof] and that the flat badge cannot return; re-adding it turns the gate red (falsification- verified). Wired into .github/workflows/verification-honesty.yml alongside a continuous spec-suite run that publishes the badge JSON on main. Numbers (clean-main, cargo-kiln testsuite --run-wast): 261/280 files, 65,618/65,633 executed assertions (99.98%), 2,370 modules. Created-By: Claude Code (Anthropic) Model: claude-opus-4-8[1m] Session-Id: c7e925b0-4761-45b4-95cc-97727a810844 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
avrabe
enabled auto-merge (squash)
July 11, 2026 09:35
This was referenced Jul 11, 2026
README: drop the unbacked "formally verified WebAssembly toolchain" org footer
pulseengine/temper#60
Open
Closed
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
🔍 Build Diagnostics ReportSummary
🎯 Impact AnalysisIssues in Files You Modified
Cascading Issues (Your Changes Breaking Other Files)
✅ No Issues DetectedPerfect! Your changes don't introduce any new errors or warnings, and don't break any existing code. 📊 Full diagnostic data available in workflow artifacts 🔧 To reproduce locally: # Install cargo-kiln
cargo install --path cargo-kiln
# Analyze your changes
cargo-kiln build --output json --filter-severity error
cargo-kiln check --output json --filter-severity warning |
avrabe
added a commit
to pulseengine/witness
that referenced
this pull request
Jul 14, 2026
…rification dogfood) (#151) Witness applied the claim-verification skill to kiln (pulseengine/kiln#423) and ordeal (pulseengine/ordeal#69); this turns the same discipline on witness's own prose. Witness is a COVERAGE tool, not a correctness prover — its integrity lives entirely in its scope hedges, which are exactly what a formal-methods skeptic would attack if they silently drifted into overclaims. mark → bind → gate: - claims.yaml marks 4 load-bearing claims and binds each to a re-derivable predicate: * WITNESS-NOT-A-CORRECTNESS-PROOF — README keeps "does **not** prove"; forbid "formally verified" / "proves correctness" ever appearing. * WITNESS-MCDC-STYLE-NOT-CERTIFIED — "MC/DC-style" stays; forbid flat "MC/DC/DO-178C certified/compliant". * WITNESS-CHECKER-QUALIFIABLE-NOT-QUALIFIED — "qualifiable kernel" stays; forbid present-tense "is/already/fully qualified" before the v1.0 DO-330 artifact ships. * WITNESS-SIGNATURE-SCOPE — SECURITY.md keeps enumerating what a signature does NOT prove. - tools/claim-check.py re-derives every predicate from the actual docs. - .github/workflows/claim-check.yml gates it on every PR/main push. Drift = red; falsification-verified (each of the 4 goes red on an injected overclaim, green on revert). Also fixes a real in-prose drift: the demo scoreboard said "715 br_ifs" while the TOTAL table two lines up (and the same paragraph, "672/716 branches") says 716. Per the skill's boundary, the example numbers themselves stay narrative (not gated). Created-By: Claude Code (Anthropic) Model: claude-opus-4-8[1m] Session-Id: c7e925b0-4761-45b4-95cc-97727a810844 Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Jul 14, 2026
…point to the CI badge (#434) The "Verification & correctness" section hard-coded "261/280 files" and "65,618/65,633 (99.98%)". The dynamic endpoint badge (added in #423) has since re-derived the live rate from CI — currently 263/281 files · 99.20% asserts — so the prose numbers drifted the moment the testsuite pin advanced. That is exactly the anti-pattern the badge was meant to kill: a number typed in prose goes stale. Replace the frozen figures with a pointer to the CI-re-derived badge, keeping the durable qualitative argument (lead with the file ratio because a parse-failure contributes zero assertions and hides in the assertion rate; the known gaps). No number in prose can now diverge from the evidence. Created-By: Claude Code (Anthropic) Model: claude-opus-4-8[1m] Session-Id: c7e925b0-4761-45b4-95cc-97727a810844 Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Why
External formal-verification review (Conrad Watts, relayed via Christof Petig) flagged kiln's flat green "Formally Verified" badge + "formally verified WebAssembly toolchain" tagline as an overclaim. Audited claim vs. evidence:
kiln-runtime/kiln-instructions/kiln-decoder/kiln-component) carries zero formal proofs — it is conformance-tested (spec suite) and unit-tested, not mechanically proven. (Re-verified on currentmain:#[kani::proof]count across those crates = 0.)We couldn't back "formal proof of the interpreter." This PR replaces the claim with what the evidence supports — and gates it so it can't drift back.
What changed
Formally Verifiedbadge and the Rocq/Z3/Verus "Formal Verification" note; add an honestVerification & correctnesssection. It leads with the un-spoofable file ratio (261/280, 93.2%): a file that fails to parse (custom-descriptors) contributes zero assertions to the "99.98% of executed assertions" figure and would otherwise hide exactly where a skeptic looks. States plainly that the interpreter's semantics are not formally proven.tools/spec-badge.py), never hand-typed. Cannot drift from the evidence.claims.yaml+tools/claim-check.py— gate the doc claims against source (flat badge can't return; interpreter-core proof count must stay 0; spec suite must be vendored). Falsification-verified: re-adding the badge turns the gate red..github/workflows/verification-honesty.yml— runs claim-check as a hard gate on every PR, runs the spec suite continuously, and publishes the badge JSON to thebadgesbranch onmain.Numbers (clean
main,cargo-kiln testsuite --run-wast)Known gaps (stated in the README): GC-proposal validation strictness (a few should-be-invalid modules currently accepted) +
custom-descriptorsparse failure.Notes for review
origin/main.kani-verification.ymlis already re-enabled upstream, so this PR does not touch it.badgesbranch is already seeded, so the endpoint badge renders now (not broken-until-first-CI-run).🤖 Generated with Claude Code