Scaling Instruction-Selection Verification against Authoritative ISA Semantics

Secure, performant execution of untrusted code—as promised by WebAssembly (Wasm)—requires correct compilation to native code that enforces a sandbox. Errors in instruction selection can undermine the sandbox’s guarantees, but prior verification work struggles to scale to the complexity of realistic industrial compilers. We present Arrival , an instruction-selection verifier for the Cranelift production Wasm-to-native compiler. Arrival enables end-to-end, high-assurance verification while reducing developer effort. Arrival ( 1 ) automatically reasons about chains of instruction-selection rules, thereby reducing the need for develop-er-supplied intermediate specifications, ( 2 ) introduces a lightweight, efficient method for reasoning about stateful instruction-selection rules, and ( 3 ) automatically derives high-assurance machine code specifications. Our work verifies nearly all AArch64 instruction-selection rules reachable from Wasm core. Furthermore, Arrival reduces the developer effort required: 60 % of all specifications benefit from our automation, thereby requiring 2.6 × fewer hand-written specifications than prior approaches. Arrival finds new bugs in Cranelift’s instruction selection, and it is viable for integration into production workflows.