Epistemic Logic has been shown to provide a useful abstract framework for reasoning about fault tolerant distributed algorithms. In particular, it provides a way to derive protocols that are optimal in the way that they use information. An example of this is results using notions of common knowledge to establish the optimality of consensus protocols, under a variety of failure models. Proofs in this area have, to date, been performed manually, and have consequently been error-prone. This paper addresses this weakness using formal methods. A formalization in the theorem prover Isabelle is developed of a general framework for epistemic reasoning about distributed algorithms, that can cover multiple failure models and concrete protocols. As an application of the framework, it is formally proved that for all patterns of information exchange among the agents, the implementation of a knowledge based program is optimal among protocols for simultaneous consensus that use that pattern of information exchange. Furthermore, the FloodSet protocol has been modelled in our framework and we verified knowledge properties about the protocol.