It's a semantics for the intermediate representation used by most of the LLVM optimization passes defined in a theorem prover.
With it you can, for example, write your own LLVM pass in Coq's specification language and prove that it can't introduce bugs by changing the meaning of a program.
See also Compcert[1] and CakeML[2] for some other recent work in this area.