kiln is the runtime/interpreter — which makes it the org's natural candidate for a reference executable oracle: the trusted-enough interpreter that transcoded/dissolved artifacts (synth output, the gust dissolve) are differential-tested against. Right now kiln is 'an interpreter that works'; the approach move is to invest it into a reference oracle with an independent witness of its own correctness.
- Reference oracle: make 'runs identically on kiln and on the shipped path' a standard differential gate for the dissolve pipeline (gale already differentials dissolved-native vs wasmtime; kiln is the wasm-side reference).
- Independence against an external artifact: validate kiln itself by differential-testing against an external, independently-verified interpreter — a mechanised/verified Wasm reference interpreter used elsewhere as a fuzzing oracle (e.g. WasmRef-Isabelle, PLDI 2023) is exactly this kind of prior art. An interpreter you also wrote is not its own oracle; an external verified interpreter is the independent witness that catches what kiln's own tests can't.
This is the spec-as-machine-oracle pattern: the value of a verified interpreter is less 'it's proven' and more 'it's the thing everything else is differential-tested against'.
Part of a verification-approach sweep (direction, not a defect): prefer generation over checking (a single source emits the artifacts, so drift becomes unrepresentable), use independence adversarially (run a second mechanisation to hunt spec bugs rather than shelving it), and invest reference oracles (one artifact everything else differential-tests against).
kiln is the runtime/interpreter — which makes it the org's natural candidate for a reference executable oracle: the trusted-enough interpreter that transcoded/dissolved artifacts (synth output, the gust dissolve) are differential-tested against. Right now kiln is 'an interpreter that works'; the approach move is to invest it into a reference oracle with an independent witness of its own correctness.
This is the spec-as-machine-oracle pattern: the value of a verified interpreter is less 'it's proven' and more 'it's the thing everything else is differential-tested against'.
Part of a verification-approach sweep (direction, not a defect): prefer generation over checking (a single source emits the artifacts, so drift becomes unrepresentable), use independence adversarially (run a second mechanisation to hunt spec bugs rather than shelving it), and invest reference oracles (one artifact everything else differential-tests against).