[quazar]

Formal specification of LLVM and compile semantics to Z3, I would guess.

[boomanaiden154]

Pretty much this. It's called Alive2.

https://dl.acm.org/doi/abs/10.1145/3453483.3454030

[isaacfrond]

tnanks