This model was put to use in many ways. Computability
and complexity results were proven: new algorithms for consensus
in the original paper by Charron-Bost and Schiper [1]};
characterizations for consensus solvability by
Coulouma et al. [2]} and Nowak et
al. [3]}; a characterization
for approximate consensus solvability by Charron-Bost et
al. [4]}; a study of \(k\)  set-agreement
by Biely et al. [5]}; and more.
The clean mathematical abstraction of the Heard-Of model also
works well with formal verification. The rounds provide
structure, and the reasoning can be less operational than
in many distributed computing abstractions. We have
a proof assistant verification of consensus algorithms
in Charron-Bost et al. [6]}; cutoff
bounds for the model checking of consensus algorithms
by Marić et al. [7]};
a DSL to write code following the structure of the Heard-Of model
and verify it with inductive invariants by Drăgoi et
al. [8]}; and more.
