The core of Infinispan can be represented in very simple "primitives": a set of nodes send messages to each other. The fundamental rules are also relatively simple:

• a message can't be received before it's sent
• a message could be lost
• a node could be killed at any time

From these basic building blocks one can start building some logical consequences:

• messages sent to multiple nodes might arrive at different times
• multiple messages sent to multiple nodes might be delivered in different order

Some of these problems are resolved by JGroups - but even then it must be configured accordingly, meaning Infinispan' s usage of it is sensible to using the wrong method or flags.

While the Java/Scala code in Infinispan is not overly complex, it's not suited for reasoning on the consequences of often-needed changes in the codebase. It would be very useful to be able to define patterns in an ad-hoc meta language, and provide a proof correctness of the patterns it uses, or at least proof the events it should avoid can not happen.

A great help for the project would be to sketch such a language and try it out on some of the distribution schemes Infinispan uses to proof they are correct or identify flaws in correctness. In a second step (optional) one could build some tooling around this to provide automatic demonstration / simulation for proposed changes expressed in this meta language.
The Promela language could be used for this purpose; so one could build tooling around it, try to apply it on Infinispan, and possibly work on ad-hoc extesions.

See also previous proposal: "Visualization and tracing of messages between nodes" -> that would make it possible to trace the real Infinispan behaviour and then demonstrate it's correctness or identify problems before they happen.