Mechanical verification of a constructive proof for FLP

Abstract

The impossibility of distributed consensus with one faulty process is; result with important consequences for real world distributed systems e.g., commits in replicated databases. Since proofs are not immune to faults and even plausible proofs with; profound formalism can conclude wrong results, we validate the fundamental result named FLP after Fischer, Lynch and Paterson by using the interactive theorem prover Isabelle/HOL. We present; formalization of distributed systems and the aforementioned consensus problem. Our proof is based on Hagen Völzer’s paper; constructive proof for FLP. In addition to the enhanced confidence in the validity of Völzer’s proof, we contribute the missing gaps to show the correctness in Isabelle/HOL. We clarify the proof details and even prove fairness of the infinite execution that contradicts consensus. Our Isabelle formalization may serve as; starting point for similar proofs of properties of distributed systems.