This paper shows that deterministic consensus in synchronous distributed
systems with link faults is possible, despite the impossibility result
of (Gray, 1978). Instead of using randomization, we overcome this
impossibility by moderately restricting the inconsistency that link faults
may cause system-wide. Relying upon a novel hybrid fault model that
provides different classes of faults for both nodes and links, we
provide a formally verified proof that the m+1-round Byzantine
agreement algorithm OMH (Lincoln & Rushby, 1993) requires n> 2f_ls +
f_lr + f_lra + 2(f_a+f_s) + f_o + f_c + m nodes for transparently masking
at most f_ls broadcast and f_lr receive link faults (including at
most f_lra arbitrary ones) per node in each round, in addition to
at most f_a, f_s, f_o, f_c arbitrary, symmetric, omission, and
manifest node faults, provided that m >= f_a+f_o+1. Our approach to
modeling link faults is justified by a number of theoretical results,
which include tight lower bounds for the required number of nodes
and an analysis of the assumption coverage in systems where links
fail independently with some probability p.

Keywords: Fault-tolerant distributed systems, fault models,
link faults, consensus, Byzantine agreement, formal verification,
assumption coverage, impossibility results, lower bounds.