Google, IBM & Meta Certificates — All 10,000+ Courses at 40% Off
One annual plan covers every course and certificate on Coursera. 40% off for a limited time.
Get Full Access
A conference talk from CoqPL 2025 that explores the Vellvm project, an extensive effort to formalize LLVM IR in the Coq proof assistant. Learn about the challenges of formalizing a widely-used intermediate language that serves as the foundation for many programming languages. The presenters, Calvin Beck, Hanxi Chen, and Steve Zdancewic from the University of Pennsylvania, discuss how proof assistants like Coq can reveal issues in informal specifications, how testing tools like QuickChick help bridge the gap between real-world implementations and formal semantics, and how LLVM IR could be improved to better support verification efforts. The talk also covers technical challenges encountered during the project, including limitations of Coq's type system, extraction bugs, and performance issues with proofs and extracted code. This 23-minute presentation was part of the CoqPL 2025 workshop held on January 25, 2025, sponsored by ACM SIGPLAN.
