A. Rowstron, P. Druschel. Pastry: scalable, decentralized object location and routing for large-scale peer-to-peer systems. Proc. IFIP/ACM Intl. Conf. Distributed System Platforms (Middleware'01), LNCS 2218, pp. 329-350 (2001). Springer link.As part of his PhD thesis, Tianxiang Lu modeled published versions of Pastry in TLA+ and verified his specifications using TLC, the TLA+ model checker. He discovered that the Pastry ring could become permanently disconnected when new nodes joined the ring, even in the absence of node failures. He then designed a version of Pastry that avoided this problem. The main idea was to allow any
Readynode (i.e., a node that is fully integrated into the Pastry ring) to help only one new node at a time join the ring. He reduced the correctness property to key invariants and developed a proof using TLAPS, the TLA+ Proof System.
The low-level theory underlying the Pastry ring involves reasoning about (modulus) arithmetic, and arithmetic reasoning was poorly supported at the time of Tianxiang Lu's work. His TLA+ proof therefore assumed many facts about arithmetic, as well as other data structures, notably Pastry's leaf sets representing the neighborhood of a node. During her PhD thesis, Noran Azmy revisited the Pastry proof and discovered that many of these assumptions were actually wrong, essentially because they overlooked certain corner cases. Worse, at least one of Lu's invariants did not hold, and its proof had succeeded only because of unjustified assumptions. This was a harsh reminder that you should avoid using axioms in interactive proofs.
Subsequently, Noran Azmy rewrote the entire proof. She not only corrected (and proved!) the necessary low-level facts, but also introduced certain higher-level abstractions that simplified reasoning about the operations used in Pastry, and she rewrote the higher-level invariants. This led to a completely formal and machine-checked of Lu's variant of Pastry, still in a pure-join model, i.e. without nodes leaving the ring or failing.
Analyzing the proof, we realized that the final lease exchange phase of the join protocol was actually not needed for correctness. This phase was not present in the original Pastry protocol, but had been introduced in a subsequent technical report, presumably for ensuring more accurate information about the neighborhood of nodes. Lu had already shown that this additional step did not prevent the ring from disintegrating in the presence of node departures. Azmy ported her existing proof to a simplified version of the protocol, where lease exchange is replaced by a simple notification from the newly joined node to its helper node about the end of the join protocol.
The formal proofs are not for the faint of heart, consisting of some 30,000 lines of proof (for a few hundred lines of specification). They are made available here in order to document this effort. If you use them as a starting point for your own project, I'd love to hear from you.