Here's a high level description in 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.