Mixed choice multiparty message passing is an expressive concurrency programming paradigm where components use non-determinism to choose between concurrent options for sending and receiving messages. This
flexibility makes it possible to program advanced algorithms, such as leader election protocols, succinctly. We
present Mixtris, a mechanised higher-order separation logic for reasoning about functional correctness of
higher-order imperative programs with mixed choice multiparty message passing in a shared memory setting.
Mixtris builds upon recent work on separation logic for (non-mixed choice) multiparty message-passing
programs, by drawing inspiration from session type systems for mixed choice multiparty message-passing
programs. Mixtris is the first program logic for mixed choice multiparty message passing. We prove soundness
of Mixtris using a novel model of our mixed choice multiparty protocols. We demonstrate how Mixtris can be
used to formally reason about challenging examples, including some leader election protocols such as Chang
and Roberts’s ring leader election protocol. All the results in the paper (both meta-theory and examples) have
been formalised in the Rocq proof assistant on top of the Iris program logic framework.