  Peer-to-peer systems are the most resilient form of distributed computing,
but the design of robust protocols for their coordination is difficult. This
makes it hard to specify and reason about global behaviour of such systems.
This paper presents swarm protocols to specify such systems from a global
viewpoint. Swarm protocols are projected to machines, that is local
specifications of peers.
  We take inspiration from behavioural types with a key difference: peers
communicate through an event notification mechanism rather than through
point-to-point message passing. Our goal is to adhere to the principles of
local-first software where network devices collaborate on a common task while
retaining full autonomy: every participating device can locally make progress
at all times, not encumbered by unavailability of other devices or network
connections. This coordination-free approach leads to inconsistencies that may
emerge during computations. Our main result shows that under suitable
well-formedness conditions for swarm protocols consistency is eventually
recovered and the locally observable behaviour of conforming machines will
eventually match the global specification.
  The model we propose elaborates on an existing industrial platform and
provides the basis for tool support (sketched here and fully described in a
companion artifact paper), wherefore we consider this work to be a viable step
towards reasoning about local-first and peer-to-peer software systems.
