research lead: position kiln + witness as a verified-semantics runtime vs the unverified Wasmtime TCB

[avrabe]

From a focused web-research pass.

The opening: the "Wasm sandboxes untrusted agent code" wave (e.g. Microsoft Wassette, https://github.com/microsoft/wassette) rests on Wasmtime, which is not formally verified — and on 9 Apr 2026 Wasmtime shipped 12 advisories incl. a real sandbox escape, CVE-2026-34971 (Cranelift aarch64 miscompilation → guest arbitrary host read/write: https://advisories.gitlab.com/pkg/cargo/wasmtime/CVE-2026-34971/ , https://bytecodealliance.org/articles/wasmtime-security-advisories).

The narrative for kiln + witness: a runtime whose semantics are checked against WasmCert-Coq (Wasm 2.0, 100% conformance — https://github.com/WasmCert/WasmCert-Coq) + witness providing MC/DC structural-coverage evidence over a formal semantics is a credible verified alternative to Wasmtime-for-untrusted-code. Standard DO-178C tooling has no MC/DC-on-Wasm — that's a witness lead too.

Concrete first step: validate kiln's interpreter semantics against WasmRef-Coq / the Coq spec rather than an ad-hoc semantics.

(Tracking issue from research; not scoped to a release yet.)

[avrabe]

Strong opening, and the CVE is real leverage — but let's position it falsifiably, because the honest current state matters more than the pitch.

What we can NOT claim today (from the bootstrap-verification audit just done): kiln is not a formally-verified Wasmtime replacement. The only formal method gating kiln CI is Verus, and it proves invariants of an abstract model of two bounded collections — not the interpreter, executor, or memory system. Kani is nightly/non-gating (#237), the interpreter itself is the std QM reference, and rivet validate still has open errors (#280). Claiming "verified semantics" end-to-end right now would be exactly the kind of overclaim the methodology says to avoid.

What IS defensible — and is a genuinely different proposition from Wasmtime:

1. The CVE is a Cranelift codegen escape (aarch64 miscompilation). That's the AOT/JIT codegen-TCB problem. Our answer there is synth's Rocq-verified transcoding to ARM/RISC-V, not the interpreter — that's where the "verified vs miscompiling JIT" story is strongest. Lead with synth for the codegen-trust narrative.
2. kiln's contribution is the cert-scope split, not interpreter-vs-Wasmtime: a QM reference interpreter that proves the work body (incl. the meld-fused core) executes correctly in a normal environment, and a no_std/no-alloc embedded core that is verifiable-by-construction — kiln-async (forbid-unsafe, no heap, fuel-bounded) with Verus invariants + Lean+Aeneas refinement reusing spar's RTA/RM/EDF proofs. That just landed its variant model (chore(rivet): product-line variant model — interpreter-QM vs embedded-cert scope #289) binding the safety case to the embedded variant.
3. witness adds MC/DC truth-table evidence on the Wasm — structured evidence, not a semantics proof. sigil adds signed attestation. Together that's "auditable runtime," which is the real, ownable claim.

Recommendation: frame it as "verifiable embedded core + reference interpreter + MC/DC evidence + signed attestation," with synth carrying the codegen-trust counter to the Cranelift CVE — not "verified Wasmtime killer." Every claim should map to a green oracle (Verus/Lean/witness), and we publish the falsification when a claim doesn't yet hold. Happy to turn this into a positioning doc once the kiln-async Verus/Lean phases (3/5) actually land, so the claims are backed by green proofs rather than intent.