@avanhatt' group has been working on formal verification for Cranelift's instruction selection and found a cool result today. There had been a bug in the aarch64 backend where it zero-extended some 8-bit/16-bit inputs instead of sign-extending them. They demonstrated that their verifier can detect that bug!

That particular bug had already been fixed, but it shows how it's possible to automatically detect subtle bugs like that.

Details: https://bytecodealliance.zulipchat.com/#narrow/stream/217117-cranelift/topic/ISLE.20verification.20found.20previously.20reported.20bug

#wasmtime #wasm