A Correctness Proof for a Practical Byzantine-Fault-Tolerant Replication Algorithm
Miguel Castro, Barbara H. Liskov · DSpace@MIT (Massachusetts Institute of Technology) · 1999
This paper presents a formal specification for the unoptimized version of our algorithm presented in Section 4 of [4] and proves its safety (but not its liveness.) The specification uses the I/O automaton formalism of Tuttle an Lynch [8] and the proof is based on invariant assertions and simulation relations