pith. machine review for the scientific record. sign in

arxiv: 2604.16097 · v1 · submitted 2026-04-17 · 💻 cs.DC

Recognition: unknown

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

Authors on Pith no claims yet

Pith reviewed 2026-05-10 07:42 UTC · model grok-4.3

classification 💻 cs.DC
keywords swarm protocolscompositional verificationdistributed systemsasynchronous communicationpeer-to-peer systemsformal methodsprotocol reuseimplementation integration
0
0 comments X

The pith

Swarms become compositional so that verified protocols and machines can be reused in larger systems without breaking guarantees.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops theory and techniques to add compositionality to swarm protocols. Swarms are peer-to-peer systems of independent machines that exchange events asynchronously and can advance locally without constant connectivity. Earlier models did not support combining smaller verified swarms into larger ones, which blocked modular design and reuse. The new methods let developers specify, verify, and implement complex swarms by correctly assembling pre-existing components, with a software artifact handling automatic integration. This would make reliable large-scale distributed applications easier to build by allowing safe reuse of designs and proofs.

Core claim

We present novel theory and techniques for the compositional specification, verification, and implementation of swarms. These results enable the correct compositional reuse of pre-existing swarm protocols and machine implementations. We implement these contributions in a companion software artifact which enables the automatic integration of independently designed and verified swarm components.

What carries the argument

Compositional operators that extend the local-first asynchronous event propagation model while preserving the behaviors and guarantees of individual swarm protocols and machines.

Load-bearing premise

The local-first model with asynchronous event propagation can be extended with compositional operators without introducing inconsistencies that break existing swarm behaviors or verification guarantees.

What would settle it

A pair of independently verified swarm protocols whose composition under the new operators produces a system that violates a property each component was proven to satisfy.

read the original abstract

Swarm protocols are a recently introduced formalism for specifying, implementing, and verifying peer-to-peer systems called swarms. A swarm consists of distributed agents called machines that communicate by asynchronous event propagation. Following a local-first model, each machine can progress without requiring continuous connectivity to other machines. Existing models of swarms are not compositional, making the modular development of large and complex swarm applications as well as the reuse of code difficult. We address these issues by presenting novel theory and techniques for the compositional specification, verification, and implementation of swarms. These results enable the correct compositional reuse of pre-existing swarm protocols and machine implementations. We implement these contributions in a companion software artifact which enables the automatic integration of independently designed and verified swarm components.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The paper introduces novel theory and techniques for the compositional specification, verification, and implementation of swarms—peer-to-peer systems of machines that communicate via asynchronous event propagation under a local-first model. It addresses the non-compositional nature of prior swarm models by defining operators that enable correct reuse of existing swarm protocols and machine implementations, supported by a companion software artifact for automatic integration of independently designed and verified components.

Significance. If the compositional operators preserve local-first asynchronous semantics and prior verification guarantees without introducing inconsistencies, the work would meaningfully advance modular development and reuse in distributed systems, reducing the difficulty of building large-scale swarm applications from pre-verified parts.

major comments (1)
  1. The central claim of 'correct compositional reuse' while preserving existing behaviors and verification guarantees is load-bearing but unsupported by any explicit preservation theorems, derivations, or counterexample checks in the provided abstract and high-level description; without these, the extension of the local-first model cannot be confirmed to avoid breaking semantics.
minor comments (1)
  1. The abstract and overview would benefit from an early, self-contained definition of the new compositional operators before discussing their properties.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful review and for identifying the need to strengthen the presentation of our central claims. We respond to the major comment below.

read point-by-point responses
  1. Referee: The central claim of 'correct compositional reuse' while preserving existing behaviors and verification guarantees is load-bearing but unsupported by any explicit preservation theorems, derivations, or counterexample checks in the provided abstract and high-level description; without these, the extension of the local-first model cannot be confirmed to avoid breaking semantics.

    Authors: We appreciate the referee highlighting this point. The full manuscript contains the requested support: Section 3 defines the compositional operators and includes Lemma 3.1 and Theorem 3.2 deriving semantic preservation for the local-first asynchronous model; Section 4 presents Theorem 4.1 (preservation of verification guarantees) and Theorem 4.2 (no introduction of inconsistencies under composition), with full derivations in Appendix B. Section 6 provides counterexample validation via the software artifact on composed protocols. The abstract and introduction high-level overview summarize the results but do not explicitly name the theorems. We will revise the abstract and introduction to reference these theorems and lemmas directly. revision: partial

Circularity Check

0 steps flagged

No significant circularity detected in compositional swarm theory

full rationale

The paper presents novel compositional operators for specification, verification, and implementation of swarms extending a local-first asynchronous event model. The abstract and context describe these as independent contributions enabling reuse of pre-existing protocols without reducing any central claim to self-definition, fitted inputs renamed as predictions, or load-bearing self-citations. No equations or steps in the provided material equate outputs to inputs by construction, and the derivation relies on new theory rather than imported uniqueness theorems or ansatzes from overlapping prior work. The approach is self-contained against external swarm protocol benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Insufficient information from abstract alone; no specific free parameters, axioms, or invented entities can be identified without the full technical development.

pith-pipeline@v0.9.0 · 5435 in / 921 out tokens · 67167 ms · 2026-05-10T07:42:36.521545+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

53 extracted references · 29 canonical work pages

  1. [1]

    Actyx decentralized event database, streaming and processing engine, 2024

    Actyx AG. Actyx decentralized event database, streaming and processing engine, 2024. URL: https://github.com/Actyx/Actyx

  2. [2]

    @actyx/machine-check library, 2024

    Actyx AG. @actyx/machine-check library, 2024. accessed 13-12-2024. URL: https://www.npmjs.com/package/@actyx/machine-check

  3. [3]

    @actyx/machine-runner library, 2024

    Actyx AG. @actyx/machine-runner library, 2024. accessed 13-12-2024. URL: https://www.npmjs.com/package/@actyx/machine-runner

  4. [4]

    Actyx developer website

    Actyx AG . Actyx developer website . https://developer.actyx.com, 2024. [Online; accessed on 29 October 2024]

  5. [5]

    Actors: A Model of Concurrent Computation in Distributed Systems

    Gul Agha. Actors: A Model of Concurrent Computation in Distributed Systems . The MIT Press, 12 1986. https://doi.org/10.7551/mitpress/1086.001.0001 doi:10.7551/mitpress/1086.001.0001

  6. [6]

    Behavioral types in programming languages

    Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deni \'e lou, Simon J Gay, Nils Gesbert, Elena Giachino, Raymond Hu, et al. Behavioral types in programming languages. Foundations and Trends in Programming Languages , 3(2-3):95--230, 2016

  7. [7]

    Consistent global states of distributed systems: Fundamental concepts and mechanisms

    Ozalp Babaoglu and Keith Marzullo. Consistent global states of distributed systems: Fundamental concepts and mechanisms. Distributed Systems , 53, 1993

  8. [8]

    Pregui c a

    Valter Balegas, S \' e rgio Duarte, Carla Ferreira, Rodrigo Rodrigues, and Nuno M. Pregui c a. IPA: invariant-preserving applications for weakly consistent replicated databases. Proc. VLDB Endow. , 12(4):404--418, 2018. URL: http://www.vldb.org/pvldb/vol12/p404-balegas.pdf, https://doi.org/10.14778/3297753.3297760 doi:10.14778/3297753.3297760

  9. [9]

    Next generation protocols for heterogeneous systems (dagstuhl seminar 24051)

    Stephanie Balzer, Marco Carbone, Roland Kuhn, and Peter Thiemann. Next generation protocols for heterogeneous systems (dagstuhl seminar 24051). Dagstuhl Reports , 14(1):108--129, 2024. https://doi.org/10.4230/DAGREP.14.1.108 doi:10.4230/DAGREP.14.1.108

  10. [10]

    Connecting open systems of communicating finite state machines

    Franco Barbanera, Ugo de'Liguoro, and Rolf Hennicker. Connecting open systems of communicating finite state machines. J. Log. Algebraic Methods Program. , 109, 2019. URL: https://doi.org/10.1016/j.jlamp.2019.07.004, https://doi.org/10.1016/J.JLAMP.2019.07.004 doi:10.1016/J.JLAMP.2019.07.004

  11. [11]

    Multicompatibility for multiparty-session composition

    Franco Barbanera, Mariangiola Dezani-Ciancaglini, Lorenzo Gheri, and Nobuko Yoshida. Multicompatibility for multiparty-session composition. In Proceedings of the 25th International Symposium on Principles and Practice of Declarative Programming , pages 1--15, 2023

  12. [12]

    Composition and decomposition of multiparty sessions

    Franco Barbanera, Mariangiola Dezani - Ciancaglini, Ivan Lanese, and Emilio Tuosto. Composition and decomposition of multiparty sessions. J. Log. Algebraic Methods Program. , 119:100620, 2021. URL: https://doi.org/10.1016/j.jlamp.2020.100620, https://doi.org/10.1016/J.JLAMP.2020.100620 doi:10.1016/J.JLAMP.2020.100620

  13. [13]

    On composing communicating systems

    Franco Barbanera, Ivan Lanese, and Emilio Tuosto. On composing communicating systems. In Cl \' e ment Aubert, Cinzia Di Giusto, Larisa Safina, and Alceste Scalas, editors, Proceedings 15th Interaction and Concurrency Experience, ICE 2022, Lucca, Italy, 17th June 2022 , volume 365 of EPTCS , pages 53--68, 2022. https://doi.org/10.4204/EPTCS.365.4 doi:10.42...

  14. [14]

    Composition of synchronous communicating systems

    Franco Barbanera, Ivan Lanese, and Emilio Tuosto. Composition of synchronous communicating systems. J. Log. Algebraic Methods Program. , 135:100890, 2023. URL: https://doi.org/10.1016/j.jlamp.2023.100890, https://doi.org/10.1016/J.JLAMP.2023.100890 doi:10.1016/J.JLAMP.2023.100890

  15. [15]

    Principles of eventual consistency

    Sebastian Burckhardt. Principles of eventual consistency. Found. Trends Program. Lang. , 1(1–2):1–150, oct 2014. https://doi.org/10.1561/2500000011 doi:10.1561/2500000011

  16. [16]

    Sebastian Burckhardt, Manuel F \"a hndrich, Daan Leijen, and Benjamin P. Wood. Cloud types for eventual consistency. In James Noble, editor, ECOOP 2012 -- Object-Oriented Programming , pages 283--307, Berlin, Heidelberg, 2012. Springer

  17. [17]

    Global Sequence Protocol: A Robust Abstraction for Replicated Shared State

    Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, and Manuel F \"a hndrich. Global Sequence Protocol: A Robust Abstraction for Replicated Shared State . In John Tang Boyland, editor, 29th European Conference on Object-Oriented Programming (ECOOP 2015) , volume 37 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 568--590, Dagstuhl,...

  18. [18]

    Distributed programming using role-parametric session types in go: statically-typed endpoint apis for dynamically-instantiated communication structures

    David Castro - Perez , Raymond Hu, Sung - Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. Distributed programming using role-parametric session types in go: statically-typed endpoint apis for dynamically-instantiated communication structures. Proc. ACM Program. Lang. , 3( POPL ):29:1--29:30, 2019. https://doi.org/10.1145/3290342 doi:10.1145/3290342

  19. [19]

    Fundamental properties of infinite trees

    Bruno Courcelle. Fundamental properties of infinite trees. Theor. Comput. Sci. , 25:95--169, 1983. https://doi.org/10.1016/0304-3975(83)90059-2 doi:10.1016/0304-3975(83)90059-2

  20. [20]

    Modular Compilation for Higher-Order Functional Choreographies

    Lu \' s Cruz-Filipe, Eva Graversen, Lovro Lugovi\' c , Fabrizio Montesi, and Marco Peressotti. Modular Compilation for Higher-Order Functional Choreographies . In 37th European Conference on Object-Oriented Programming (ECOOP 2023) , volume 263 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 7:1--7:37, 2023. https://doi.org/10.4230/LI...

  21. [21]

    Towards refinable choreographies

    Ugo de'Liguoro, Hernán Melgratti, and Emilio Tuosto. Towards refinable choreographies. Journal of Logical and Algebraic Methods in Programming , 127:100776, 2022. https://doi.org/10.1016/j.jlamp.2022.100776 doi:10.1016/j.jlamp.2022.100776

  22. [22]

    Dynamic multirole session types

    Pierre - Malo Deni \' e lou and Nobuko Yoshida. Dynamic multirole session types. In Thomas Ball and Mooly Sagiv, editors, POPL , pages 435--446. ACM , 2011. https://doi.org/10.1145/1926385.1926435 doi:10.1145/1926385.1926435

  23. [23]

    Parameterised multiparty session types

    Pierre - Malo Deni \' e lou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. Log. Methods Comput. Sci. , 8(4), 2012. https://doi.org/10.2168/LMCS-8(4:6)2012 doi:10.2168/LMCS-8(4:6)2012

  24. [24]

    Criterion documentation, 2025

    Criterion Developers. Criterion documentation, 2025. Accessed 18-02-2026. URL: https://docs.rs/criterion/0.7.0/criterion

  25. [25]

    Eugster, Pascal A

    Patrick Th. Eugster, Pascal A. Felber, Rachid Guerraoui, and Anne-Marie Kermarrec. The many faces of publish/subscribe. ACM Comput. Surv. , 35(2):114–131, June 2003. https://doi.org/10.1145/857076.857078 doi:10.1145/857076.857078

  26. [26]

    Compositional design, implementation, and verification of swarms: Artifact, 2026

    Florian Furbach, Lucas Clorius, Roland Kuhn, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto. Compositional design, implementation, and verification of swarms: Artifact, 2026. https://doi.org/10.5281/zenodo.18459720 doi:10.5281/zenodo.18459720

  27. [27]

    Behavioural Types: from Theory to Tools

    Simon Gay and Antonio Ravara, editors. Behavioural Types: from Theory to Tools . Automation, Control and Robotics. River, 2009

  28. [28]

    Hybrid multiparty session types: Compositionality for protocol specification through endpoint projection

    Lorenzo Gheri and Nobuko Yoshida. Hybrid multiparty session types: Compositionality for protocol specification through endpoint projection. Proc. ACM Program. Lang. , 7(OOPSLA), April 2023. https://doi.org/10.1145/3586031 doi:10.1145/3586031

  29. [29]

    Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services,

    Seth Gilbert and Nancy Lynch. Brewer's conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News , 33(2):51--59, June 2002. URL: http://doi.acm.org/10.1145/564585.564601, https://doi.org/10.1145/564585.564601 doi:10.1145/564585.564601

  30. [30]

    Consistency Models with Global Operation Sequencing and their Composition

    Alexey Gotsman and Sebastian Burckhardt. Consistency Models with Global Operation Sequencing and their Composition . In Andr \'e a W. Richa, editor, 31st International Symposium on Distributed Computing (DISC 2017) , volume 91 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 23:1--23:16, Dagstuhl, Germany, 2017. Schloss Dagstuhl--Leibn...

  31. [31]

    ' C ause i'm strong enough: reasoning about consistency choices in distributed systems

    Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro. ' C ause i'm strong enough: reasoning about consistency choices in distributed systems. In POPL 2016 , pages 371--384, 2016

  32. [32]

    A universal modular actor formalism for artificial intelligence

    Carl Hewitt, Peter Bishop, and Richard Steiger. A universal modular actor formalism for artificial intelligence. In Proceedings of the 3rd International Joint Conference on Artificial Intelligence , IJCAI'73, page 235–245, San Francisco, CA, USA, 1973. Morgan Kaufmann Publishers Inc

  33. [33]

    Multiparty asynchronous session types

    Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT S ymposium on principles of programming languages , pages 273--284, 2008

  34. [34]

    Multiparty asynchronous session types

    Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. Journal of the ACM (JACM) , 63(1):1--67, 2016

  35. [35]

    Hans H \" u ttel, Ivan Lanese, Vasco T. Vasconcelos, Lu \' s Caires, Marco Carbone, Pierre - Malo Deni \' e lou, Dimitris Mostrous, Luca Padovani, Ant \' o nio Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of session types and behavioural contracts. ACM Comput. Surv. , 49(1):3:1--3:36, 2016

  36. [36]

    Exploring type-level bisimilarity towards more expressive multiparty session types

    Sung-Shik Jongmans and Nobuko Yoshida. Exploring type-level bisimilarity towards more expressive multiparty session types. In Peter M \"u ller, editor, Programming Languages and Systems , pages 251--279, Cham, 2020. Springer International Publishing

  37. [37]

    Safe replication through bounded concurrency verification

    Gowtham Kaki, Kapil Earanky, KC Sivaramakrishnan, and Suresh Jagannathan. Safe replication through bounded concurrency verification. Proceedings of the ACM on Programming Languages , 2(OOPSLA):1--27, 2018

  38. [38]

    Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software , pages =

    Martin Kleppmann, Adam Wiggins, Peter van Hardenberg, and Mark McGranaghan. Local-first software: You own your data, in spite of the cloud. In Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software , Onward! 2019, page 154–178, New York, NY, USA, 2019. Association for Computing ...

  39. [39]

    Local-first cooperation: Autonomy at the edge, secured by crypto, 100\ https://www.infoq.com/articles/local-first-cooperation/, 2021

    Roland Kuhn. Local-first cooperation: Autonomy at the edge, secured by crypto, 100\ https://www.infoq.com/articles/local-first-cooperation/, 2021. [Online; accessed on 29 October 2024]

  40. [40]

    Behaviorally typed state machines in typescript for heterogeneous swarms

    Roland Kuhn and Alan Darmasaputra. Behaviorally typed state machines in typescript for heterogeneous swarms. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis , ISSTA 2023, page 1475–1478, New York, NY, USA, 2023. Association for Computing Machinery. https://doi.org/10.1145/3597926.3604917 doi:10.1145/3597926.3604917

  41. [41]

    Melgratti, and Emilio Tuosto

    Roland Kuhn, Hern \' a n C. Melgratti, and Emilio Tuosto. Behavioural types for local-first software. In Karim Ali and Guido Salvaneschi, editors, 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States , volume 263 of LIPIcs , pages 15:1--15:28. Schloss Dagstuhl - Leibniz-Zentrum f \" u r ...

  42. [42]

    Cambridge University Press (2023)

    Fabrizio Montesi. Introduction to Choreographies . Cambridge University Press, 2023. https://doi.org/10.1017/9781108981491 doi:10.1017/9781108981491

  43. [43]

    The Power of Well-Structured Systems , booktitle =

    Fabrizio Montesi and Nobuko Yoshida. Compositional choreographies. In Pedro R. D'Argenio and Hern \' a n C. Melgratti, editors, CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings , Lecture Notes in Computer Science, pages 425--439. Springer, 2013. https://doi.org/10.1007/...

  44. [44]

    Detection of mutual inconsistency in distributed systems

    D Stott Parker, Gerald J Popek, Gerard Rudisin, Allen Stoughton, Bruce J Walker, Evelyn Walton, Johanna M Chow, David Edwards, Stephen Kiser, and Charles Kline. Detection of mutual inconsistency in distributed systems. IEEE transactions on Software Engineering , (3):240--247, 1983

  45. [45]

    On the criteria to be used in decomposing systems into modules

    David Lorge Parnas. On the criteria to be used in decomposing systems into modules. Communications of the ACM , 15(12):1053--1058, 1972

  46. [46]

    Benjamin C. Pierce. Types and programming languages . MIT Press, 2002

  47. [47]

    URL:https: //www.usenix.org/conference/nsdi24/presentation/ryabinin

    Fred B. Schneider. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Comput. Surv. , 22(4):299--319, 1990. https://doi.org/10.1145/98163.98167 doi:10.1145/98163.98167

  48. [48]

    Conflict-free replicated data types

    Marc Shapiro, Nuno M. Pregui c a, Carlos Baquero, and Marek Zawirski. Conflict-free replicated data types. In SSS 2011 , pages 386--400, 2011. URL: http://dx.doi.org/10.1007/978-3-642-24550-3_29, https://doi.org/10.1007/978-3-642-24550-3_29 doi:10.1007/978-3-642-24550-3_29

  49. [49]

    HasChor: Functional Choreographic Programming for All

    Gan Shen, Shun Kashiwa, and Lindsey Kuper. HasChor: Functional Choreographic Programming for All . Proceedings of the ACM on Programming Languages , 7(ICFP):541--565, 2023. https://doi.org/10.1145/3607849 doi:10.1145/3607849

  50. [50]

    Declarative programming over eventually consistent data stores

    KC Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan. Declarative programming over eventually consistent data stores. In PLDI 2015 , pages 413--424. ACM, 2015

  51. [51]

    Composable partial multiparty session types for open systems

    Claude Stolze, Marino Miculan, and Pietro Di Gianantonio. Composable partial multiparty session types for open systems. Software and Systems Modeling , 22(2):473--494, 2023

  52. [52]

    Replication-aware linearizability

    Chao Wang, Constantin Enea, Suha Orhun Mutluergil, and Gustavo Petri. Replication-aware linearizability. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation , pages 980--993, 2019

  53. [53]

    Parameterised multiparty session types

    Nobuko Yoshida, Pierre - Malo Deni \' e lou, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. In C. - H. Luke Ong, editor, Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyp...