Swarm protocols are a recently-introduced formalism for specifying and verifying the intended behaviour of a distributed ensemble of agents (called “machines”) that interact in a swarm. These swarm adhere to a local-first paradigm, meaning any machine can make progress at any time without having up-to-date information or even an active connection. Thus, they are very efficient and robust. The machines communicate by emitting events and propagating them asynchronously throughout a swarm. Each machine subscribes only to certain types of events and ignores others. It maintains a local log of received events during runtime and corrects its computation whenever events are invalidated by earlier events being propagated to its log. In order to verify the behaviour of swarms, they are required to satisfy eventual fidelity. This means that once every event has been propagated to every machine, all relevant machines need to reach a consensus on the current execution of the swarm protocol. Eventual fidelity is guaranteed through a well-foundedness property of swarm protocols.

We study how different swarms can be composed into a single swarm. Unfortunately, the existing verification and implementation techniques for swarm protocols are not compositional: i.e., given two well-founded swarm protocols G1 and G2, their composition may not be well-founded and must be verified “from scratch.” Moreover, the machines that implement G1 may need to be adjusted by subscribing to events from G2 (and vice versa) in order to behave correctly in the composed swarm. These limitations make verification inefficient, prevent the modular design of large swarm protocols as compositions of simpler protocols, and hinder the reusability of machine implementations.

To address these issues, we develop novel theory and techniques for the compositional specification and verification of swarm protocols. We develop methods to compose swarms as well as their protocols. To ensure that a combined swarm is eventually faithful to the composition of the swarm protocols, we propose a new notion of well-foundedness along with additional runtime-monitoring methods for machines. Our goal is to minimize the communication between the swarms while still maintaining eventual fidelity. Ideally, machines that occur in both swarms maintain sufficient synchronisation and thus a machine does not need to subscribe to machines from the other swarm.