A HOL Theory for Voting

Central to fault-tolerant computing is redundancy management, and common to proofs of fault-tolerance is a maximum fault assumption. Typically a maximum fault assumption is rather restrictive. Usually, this is necessary to avoid assumptions about the behavior of faulty channels. A maximum fault assumption is useful because it allows reasoning about fault tolerance in the presence of arbitrarily malicious fault behavior. However, analysis of the architecture may establish certain scenarios in which the assumption may be weakened. Proofs comparing majority and plurality and proofs of simple reconfiguration strategies are presented in viewgraph form.