At the ISSA laboratory seminar Steve Zdancewic gave a talk entitled: "Vellvm - Verifying the LLVM"

Prof. Steve Zdancewic, University of Pennsylvania

The Low-Level Virtual Machine (LLVM) compiler provides a modern, industrial-strength SSA-based intermediate representation (IR) along with infrastructure support for many source languages and target platforms. Much of the LLVM compiler is structured as IR to IR translation passes that apply various optimizations and analyses.

In this talk, I will describe the Vellvm project, which seeks to provide a formal framework for developing machine-checkable proofs about LLVM IR programs and translation passes. I'll discuss some of the subtleties of modeling the LLVM IR semantics. I'll also describe some of the proof techniques that we have used for reasoning about LLVM IR transformations and sketch some example applications including verified memory-safety instrumentation and program optimizations. 
Vellvm is implemented in the Coq theorem prover and provides facilities for extracting LLVM IR transformation passes and plugging them into the LLVM compiler, thus enabling us to create verified optimization passes for LLVM and evaluate them against their unverified counterparts. 
This is joint work with many collaborators at Penn, and Vellvm is part of the NSF Expeditions project: The Science of Deep Specications.