Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
55 changes: 55 additions & 0 deletions safety/requirements/roadmap-requirements.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -543,3 +543,58 @@ 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: 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
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.
Loading