  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.
First, a subset of the agents must behave correctly and not permanently fail
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.
