VeLLVM [1]} formalizes the LLVM [2]} IR semantics using the Coq proof assistant. While the approach is similar, the target IR is substantially different. LLVM shares some common properties such as being in SSA form, but the GraalVM IR is a sea-of-nodes graph structure that unifies a program's control-flow and data-flow, while the LLVM IR is in traditional basic block SSA form.
