Maja Trela

Software engineer @ Jane Street

I studied Computer Science at University of Cambridge, where my love of formal verification, functional programming, and similar topics awakened. For my master's thesis I worked with Conrad Watt on verifying WasmRef-Isabelle, the results of which were incorporated into its associated paper. As of now I'm working as a software engineer at Jane Street.

WasmRef-Isabelle – or how to formally verify a not-slow interpreter with not-insane amount of effort

OBJECTIVES

• High-level strategy for formally verifying more efficient programs
• That proof automation in Isabelle/HOL is pretty cool 
• That better tools keep lowering the barrier to practical formal verification

AUDIENCE

People with some interest in formal verification

DESCRIPTION

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.

←Back