Eventual consensus in Synod: verification using a failure-aware actor model

Saswata Paul, Gul Agha, Stacy Patterson, Carlos Varela

Research output: Contribution to journalArticlepeer-review


Successfully attaining consensus in the absence of a centralized coordinator is a fundamental problem in distributed multi-agent systems. We analyze progress in the Synod consensus protocol—which does not assume a unique leader—under the assumptions of asynchronous communication and potential agent failures. We identify a set of sufficient conditions under which it is possible to guarantee that a set of agents will eventually attain consensus using Synod. First, a subset of the agents must not permanently fail or exhibit Byzantine failure until consensus is reached, and second, at least one proposal must be eventually uninterrupted by higher-numbered proposals. To formally reason about agent failures, we introduce a failure-aware actor model (FAM). Using FAM, we model the identified conditions and provide a formal proof of eventual progress in Synod. Our proof has been mechanically verified using the Athena proof assistant and, to the best of our knowledge, it is the first machine-checked proof of eventual progress in Synod.

Original languageEnglish (US)
Pages (from-to)395-410
Number of pages16
JournalInnovations in Systems and Software Engineering
Issue number4
StatePublished - Dec 2023


  • Athena
  • Fairness
  • Formal theorem proving
  • Liveness
  • Paxos
  • Urban air mobility

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Eventual consensus in Synod: verification using a failure-aware actor model'. Together they form a unique fingerprint.

Cite this