LLVM is an industrial-strength compiler that's used for everything from iOS development to academic research.  However, like any piece of complicated software, LLVM IR itself has a complex specification, making it hard to fully understand, and its implementation has bugs, which can cause potentially catastrophic mis-compilation errors. These properties make the LLVM framework a sweet spot for bug-finding and verification technologies--any improvements to it are amplified across its many applications.

This talk will survey the Vellvm (Verified LLVM) project, which aims to define a formal, mathematical specification for a large, useful subset of LLVM.  Vellvm is implemented in the Rocq interactive theorem prover, which can be used for developing machine-checkable properties about LLVM IR programs and compiler optimization passes.  Along the way, we'll explore some subtleties of LLVM IR semantics and see how Vellvm models them in a modular way by composing "monadic interpreters" built on top of a data structure called _interaction trees_. We'll also see some applications of Vellvm for verified compiler construction.