We present the first formal specification and verification of the fine-grained concurrent multi-producer-multi-consumer queue algorithm from Facebook’s C++ library Folly of core infrastructure components. The queue is highly optimized, practical, and used by Facebook in production where it scales to thousands of consumer and producer threads. We present an implementation of the algorithm in an ML-like language and formally prove that it is a contextual refinement of a simple coarse-grained queue (a property which implies that the MPMC queue is linearizable). We use the ReLoC relational logic and the Iris program logic to carry out the proof and to mechanize it in the Coq proof assistant. The MPMC queue is implemented using three modules, and our proof is similarly modular. By using ReLoC and Iris’s support for modular reasoning we verify each module in isolation and compose these together. A key challenge of the MPMC queue is that it has a so-called \emph{external linarization point}, which ReLoC has no support for reasoning about. Thus we extend ReLoC, both on on paper and in Coq, with novel support for reasoning about external linearization points.