Weakestmo is a recently proposed memory consistency model that uses event structures to resolve the infamous “out-of-thin-air” problem, and to enable efficient compilation to hardware. Nevertheless, this latter property—compilation correctness—has not yet been formally established. This paper closes this gap by establishing correctness in Coq of the intended compilation schemes from Weakestmo to a wide range of formal hardware memory models (x86, POWER, ARMv7, ARMv8). Our proof is the first that establishes correctness of compilation of an event-structure-based model that forbids “thin-air” behaviors, as well as the first mechanized compilation proof of a weak memory model supporting sequentially consistent accesses to such a range of hardware platforms. Our compilation proof goes via the recent Intermediate Memory Model (IMM), which we suitably extend with sequentially consistent accesses.