The paper introduces the *input-output automaton* as a model of computation for asynchronous distributed networks, which allows for modular and hierarchical correctness proofs of distributed algorithms. The authors define the input-output automaton and demonstrate its use in constructing a hierarchical correctness proof for Schönhage's distributed arbiter algorithm. The proof involves three levels of abstraction: a high-level description of the algorithm, an intermediate-level graph-theoretic description, and a low-level implementation description. The paper also discusses the challenges of expressing algorithms in traditional languages like CCS and CSP due to their inability to handle internal and external events clearly. The input-output automaton model is shown to be more suitable for expressing asynchronous distributed algorithms, as it distinguishes between internal and external actions and supports fair computation. The paper concludes with a detailed construction of the hierarchical proof, showing that the low-level model correctly implements the high-level specification.The paper introduces the *input-output automaton* as a model of computation for asynchronous distributed networks, which allows for modular and hierarchical correctness proofs of distributed algorithms. The authors define the input-output automaton and demonstrate its use in constructing a hierarchical correctness proof for Schönhage's distributed arbiter algorithm. The proof involves three levels of abstraction: a high-level description of the algorithm, an intermediate-level graph-theoretic description, and a low-level implementation description. The paper also discusses the challenges of expressing algorithms in traditional languages like CCS and CSP due to their inability to handle internal and external events clearly. The input-output automaton model is shown to be more suitable for expressing asynchronous distributed algorithms, as it distinguishes between internal and external actions and supports fair computation. The paper concludes with a detailed construction of the hierarchical proof, showing that the low-level model correctly implements the high-level specification.