The Oral Messages algorithm OM(m) is an algorithm that uses m message relay rounds to solve the Byzantine Generals Problem [5]. It is a landmark result, however its original specification is informal and its correctness proof sketchy, making both hard to understand. The proof is rewritten here using a natural deduction system formulated directly from the message flows described for OM(m) in [5]. The system comprises only two inference rules which can be used to explain the original algorithm via derivations. The rules are shown complete relative to OM(m) and sound in the sense they cannot be used to derive consensus when it is impossible [8]. The completeness proof provides more details than the original correctness proof, clearly showing the role of m, the risk it creates, and why the algorithm succeeds under well-known constraints.
