✨ This talk was recorded at Lambda Days in June 2024. If you're curious about our upcoming event, check https://lambdadays.org ✨ Abstract WasmRef-Isabelle is a WebAssembly interpreter written in Isabelle/HOL verified to be sound with respect to the WasmCert-Isabelle mechanisation of WebAssembly. Its main improvement on both the existing verified interpreter included in WasmCert-Isabelle and even the official (but unverified) WebAssembly reference interpreter is in performance – in fact, thanks to that, the Wasmtime (one of the main WebAssembly implementations) team adopted it as their fuzzing oracle. So, how much direct effort does it take to achieve such a practical result in formal verification? Actually, not an insane amount. I'll talk about how we verified WasmRef-Isabelle as a two-step refinement proof, using the WasmCert-Isabelle interpreter as the springboard so to speak, in a single (one-year) master's thesis time. Let's keep in touch! Follow us on: 💥Twitter: https://twitter.com/LambdaDays 💥LinkedIn: https://www.linkedin.com/company/lambda-days 💥Facebook: https://www.facebook.com/lambdadays 💥Mastodon: https://genserver.social/codesync