Here's a high level description in TLA+: https://github.com/nicholassm/disruptor-rs/blob/main/verification/Disruptor.tla https://github.com/nicholassm/disruptor

Here's a high level description in TLA+: https://github.com/nicholassm/disruptor-rs/blob/main/verification/Disruptor.tla https://github.com/nicholassm/disruptor-rs/blob/main/verific... (Disclaimer: I wrote it.) There's also a spec for a Multi Producer Multi Consumer (MPMC) Disrupter.