From 09102626bdf48a0ee57593fc5b778026bec63846 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 11 Jul 2026 08:07:02 +0200 Subject: [PATCH 1/2] docs(rivet): add safety-critical interpreter comparison targets (spacewasm, DLR-FT) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Land REQ_ENGINE_COMPARISON: benchmark + differentially validate kiln against its true peers — the safety-critical Rust WebAssembly interpreters — besides the wasmtime JIT. - NASA spacewasm (flight-compliant Rust interpreter for spacecraft; deterministic memory, streaming, CoreMark, libfuzzer). - DLR-FT/wasm-interpreter (minimal in-place Rust interpreter for avionics, DO-178C/DO-332; passes full WAST minus unfinished proposals; fuel halt/refill/ resume mirroring kiln; live migration). NASA's spacewasm reqs derive from it. Two workstreams: (1) use both as additional differential oracles alongside wasmtime (extends SR-35/#401 — Rust + embeddable, peer-engine agreement is high-signal); (2) a competitive matrix on conformance / perf / memory / resumable-fuel AND the verification-evidence axis where kiln leads (Verus + Lean proofs, witness MC/DC on real Wasm, sigil attestation, rivet traceability). Outcompete = lead on verification evidence while matching/beating on conformance + determinism. Sharpens #283 positioning. derives-from SR-35. Issue #413. Trace: skip --- safety/requirements/roadmap-requirements.yaml | 49 +++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/safety/requirements/roadmap-requirements.yaml b/safety/requirements/roadmap-requirements.yaml index 7093c558..7a6c13e6 100644 --- a/safety/requirements/roadmap-requirements.yaml +++ b/safety/requirements/roadmap-requirements.yaml @@ -543,3 +543,52 @@ artifacts: model: claude-opus-4-8 timestamp: 2026-07-08T22:48:04Z release: v0.7.0 + + - id: REQ_ENGINE_COMPARISON + type: requirement + title: Benchmark and differentially validate kiln against the safety-critical Rust interpreter field (NASA spacewasm, DLR-FT), not only wasmtime + description: > + kiln's differential/perf comparisons must include its TRUE peers — the + safety-critical Rust WebAssembly interpreters — besides the wasmtime JIT + (the "unverified TCB" foil of #283). Two peers, same niche as kiln + (Rust, no_std-friendly, fuel-bounded, deterministic, cert-oriented): + - NASA spacewasm (github.com/nasa/spacewasm): flight-compliant ground-up + Rust interpreter for on-board spacecraft; design levied from + flight-software standards; deterministic dynamic-memory model, + streaming for low peak memory, CoreMark + libfuzzer; draws on wasmi, + wasm3, DLR-FT. + - DLR-FT/wasm-interpreter (github.com/DLR-FT/wasm-interpreter): minimal + in-place Rust interpreter from DLR Institute of Flight Systems for + avionics (ED-12C/DO-178C, ED-217/DO-332); passes the full WAST suite + minus unfinished proposals; fuel halt/refill/resume (mirrors kiln's + resumable-fuel model); live instance migration. DASC 2025 paper "On + the Design of a WebAssembly Interpreter for Aviation." NASA spacewasm's + requirements are levied from this work. + Two workstreams. (1) Differential correctness — extend SR-35/#401: use + spacewasm + DLR-FT as additional differential ORACLES alongside wasmtime + (both Rust + embeddable, far cheaper than WasmRef-Isabelle; peer-engine + agreement is high-signal). Cross-check the WAST suite + fuzz-generated + modules across {kiln, wasmtime, spacewasm, DLR-FT}. (2) Competitive matrix + — measure kiln vs the field on WAST conformance pass rate, performance + (CoreMark-style + the per-poll micro methodology from REQ_ASYNC_BENCH), + peak/deterministic memory, no_std/no_alloc footprint, and resumable-fuel + determinism — AND the verification-evidence axis where kiln is meant to + LEAD: Verus + Lean/Aeneas proofs, witness MC/DC on the real Wasm, sigil + attestation, rivet end-to-end traceability (spacewasm/DLR are + cert-DESIGNED but not proof-carrying / MC/DC-attested to this stack level). + "Outcompete" = lead decisively on verification evidence while matching or + beating on conformance + determinism. Research / benchmark-infrastructure + direction, not a defect. + status: proposed + release: v0.7.0 + tags: [benchmark, differential-testing, oracle, conformance, positioning, research, direction, release-v0.7.0] + links: + - type: derives-from + target: SR-35 + fields: + upstream-ref: https://github.com/pulseengine/kiln/issues/413 + note: > + Peer field: NASA spacewasm + DLR-FT/wasm-interpreter. Sharpens #283 + (positioning vs the unverified Wasmtime TCB) to also cover the + cert-designed-but-unproven Rust field. Reuses the WAST mechanical oracle + (REQ_FUNC_022) and the executor-comparison bench methodology. From c4709b21b412229d0231ba4fca07cae9996d606b Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 11 Jul 2026 08:11:08 +0200 Subject: [PATCH 2/2] docs(rivet): add WasmRef-Isabelle verified-oracle leg to REQ_ENGINE_COMPARISON MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The differential set is now {kiln, wasmtime, spacewasm, DLR-FT, WasmRef-Isabelle} with tiered signal: WasmRef-Isabelle (PLDI 2023) is the machine-checked GOLD oracle (a kiln-only disagreement is a correctness bug), the safety-critical Rust peers are cheap cross-checks, wasmtime is the JIT baseline. Per SR-35, the verified leg is load-bearing — an interpreter you also wrote is not its own oracle. Trace: skip --- safety/requirements/roadmap-requirements.yaml | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/safety/requirements/roadmap-requirements.yaml b/safety/requirements/roadmap-requirements.yaml index 7a6c13e6..a523bad6 100644 --- a/safety/requirements/roadmap-requirements.yaml +++ b/safety/requirements/roadmap-requirements.yaml @@ -564,11 +564,17 @@ artifacts: resumable-fuel model); live instance migration. DASC 2025 paper "On the Design of a WebAssembly Interpreter for Aviation." NASA spacewasm's requirements are levied from this work. - Two workstreams. (1) Differential correctness — extend SR-35/#401: use - spacewasm + DLR-FT as additional differential ORACLES alongside wasmtime - (both Rust + embeddable, far cheaper than WasmRef-Isabelle; peer-engine - agreement is high-signal). Cross-check the WAST suite + fuzz-generated - modules across {kiln, wasmtime, spacewasm, DLR-FT}. (2) Competitive matrix + Two workstreams. (1) Differential correctness — extend SR-35/#401: run a + multi-oracle differential across {kiln, wasmtime, spacewasm, DLR-FT, AND + the VERIFIED reference interpreter WasmRef-Isabelle (PLDI 2023)}. The tiers + carry different signal: WasmRef-Isabelle is the machine-checked GOLD oracle + (a kiln-only disagreement with it is a kiln correctness bug, full stop); + the safety-critical Rust peers (spacewasm, DLR-FT) are cheap-to-embed + cross-checks whose agreement is high-signal and whose disagreement flags a + spec-interpretation delta worth a note; wasmtime is the JIT baseline. Per + SR-35, "an interpreter you also wrote is not its own oracle" — so the + verified leg is load-bearing, not optional. Cross-check the WAST suite + + fuzz-generated modules across all engines. (2) Competitive matrix — measure kiln vs the field on WAST conformance pass rate, performance (CoreMark-style + the per-poll micro methodology from REQ_ASYNC_BENCH), peak/deterministic memory, no_std/no_alloc footprint, and resumable-fuel