A verified WebAssembly interpreter in Lean

Abstract

WebAssembly is a new low-level programming language designed with the goal to increase interoperability and security across the software ecosystem. The WebAssembly specification is defined by the World Wide Web Consortium, with a multitude of implementors, ranging from browsers to standalone runtimes.

In order to ensure adherence to the specification, some WebAssembly implementations use formally-verified interpreters as testing oracles. This thesis explores a novel approach to designing a formally-verified interpreter, by using an intrinsically-typed representation of the WebAssembly syntax.

This intrinsically-typed interpreter is implemented in the Lean 4 proof assistant, leveraging its functional-but-in-place features to achieve good performance without sacrificing functional purity.