This book collects materials used in the formalization of an important distributed algorithm, by Schneider and van Renesse, called Chain Replication. The chain replication algorithm provides a fault-tolerant distributed storage system and guarantees a strong consistency property. The material here includes: the original Schneider and van Renesse paper; a summary of the formalization method, by Bickford & Guaspari; a detailed outline of the formalization by Bickford; and a Nuprl library providing a formal account based on the Logic of Events described by Bickford and Constable.

• Formalizing Chain Replication [pdf], Bickford and Guaspari, explains the formalization and its relation to the original informal algorithm of van Renesse and Schneider.
• Chain Replication for Supporting High Throughput and Availability [pdf] [html], van Renesse and Schneider, is the original work being formalized and reformulated here.
• Verifying Chain Replication using Events [pdf], Bickford, is an exposition of the formalization. It is a pdf file with links to html renditions of formal material.
• Event Systems is library of formal material containing the work described. The previous document ("Verifying...") with its links can be considered an expository entry point to the material.
• Logic of Events, Bickford and Constable, is a technical report describing a logic for distributed computing that has the explanatory and technical power of constructive logics of computation.