Vellvm: Formalizing the Informal
summary
Formal Coq semantics for a large subset of LLVM IR uses interaction trees (coinductive freemonads) plus event handlers to capture nondeterminism and a published memory model; an executable interpreter is extracted and supports printf/args and differential testing. A custom generator GenLVM (QuickChick) produces 10,000+ programs and finds real bugs — e.g., an extractvalue off‑by‑one when compiling a packed struct with a vector. The development is large (about 50,000 lines of spec and 100,000 lines of proof), with Coq extraction, type-system and coinduction/Prop-elimination constraints as pain points.
AI-written summary · about
chapters (16)
- 0:00Vellvm project introduction
- 1:02What is LLVM and IR
- 2:04Complexities of LLVM undef
- 4:08Goal of formalizing LLVM
- 5:11Vellvm’s event-based semantics
- 7:58Vellvm’s supported features
- 8:41Scale of Vellvm proof
- 9:24Edge cases uncovered
- 11:35Experience with Rock
- 13:41Rock’s constraints
- 14:24Differential testing in Vellvm
- 15:48Generating LLVM IR
- 17:32Why not existing generators
- 18:16Bug in GenLVM
- 19:18Takeaways and future work
- 19:59Q&A
related talks
01h 06mVerifying a compiler through equational means- 01h 06mVerifying a compiler through equational means
29mTowards Formally Verified Just-In-Time Compilation
53mSemantics-based program manipulation in the age of LLMs
31mFormal Specification
24mCode Extraction from Coq to ML-like languages
11mFormally Verifying YUL Level Static Analyses and Optimization with Coq
22mReconciling High-level Optimizations and Low-level Code in LLVM