LLVM Translation Validation Automated with Large Language Models and Lean

Chunhao Liao, Hongxu Xu, Xintong Zhou +2

LLVM is the cornerstone of modern compilers, but its subtle intermediate representation (IR) semantics make transformations error-prone and necessitate formal verification. Alive2,…