A verified WebAssembly interpreter in Lean

Alex Ionescu


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.

Jun 12, 2024 10:00 AM — 11:00 AM
Live talk in EA Lecture Hall

Alex Ionescu is a Computing Science Master’s student at Utrecht University, currently working on verified WebAssembly interpretation. He’s passionate about functional programming, programming languages & compilers, and cybersecurity.

Alex Ionescu’s webpage