vellvm/vellvm: The Vellvm II coq development. https://github.com/vellvm/vellvm
"Vellvm is a Coq formalization of the semantics of (a subset of) the LLVM compiler IR that is intended for formal verification of LLVM-based software. It is being developed at the University of Pennsylvania as part of the DeepSpec project."