ABSTRACT. A multitude of weak memory models exists supporting various types of relaxations and different synchronization primitives. On one hand, they must be lax enough to allow for hardware and compiler optimizations; on the other, the more lax the model, the harder it is to reason about programs. Though the right balance is up for debate, a memory model should provide what is known as the SC-DRF guarantee: data-race free programs behave in a sequentially consistent manner. Memory models are often defined axiomatically where the notion of a program is abstracted away (often as a graph with memory events as nodes) and orderings of memory events are defined via constraints. In this work we present a weak memory model for a calculus inspired by Go. Different from previous approaches, we thus focus on a memory model with buffered channel communication as the sole synchronization primitive. We formalize the memory model via an operational semantics and prove the SC-DRF guarantee using a standard simulation technique. The proof highlights meaningful invariants and gives insight into the workings of the memory model. Finally, we provide a concrete implementation in K, a rewrite-based executable semantic framework, which allows us to derive an interpreter for the proposed language.