Formal Verification of an Oral Messages Algorithm for Interactive Consistency

摘要: The formal specification and verification of an algorithm for Interactive Consistency based on the Oral Messages Byzantine Agreement is described. We compare our treatment with that Bevier Young, who presented a very similar algorithm. Unlike observed ''the invariant maintained in recursive subcases significantly more complicated than suggested by published proof'' found its ''a fairly difficult exercise mechanical theorem proving,'' close to previously analysis algorithm, are straightforward. This example illustrates how delicate choices formulation problem can have significant impact readability tractability verification.