Leslie Lamport

Computer scientist. This spoke holds two of his papers and ../research-wiki holds tla-plus, the specification language he later built.

• byzantine-generals-problem (with Robert Shostak and Marshall Pease, ACM TOPLAS, July 1982), written at SRI International — the price of tolerating arbitrary failure, and the f < n/3 bound.
• part-time-parliament (ACM TOCS, May 1998), written at Digital Equipment Corporation — Paxos, which declines to pay that price and says so.
• paxos-made-simple (2001) — the same algorithm again, in plain English, because the first telling did not land: “the original presentation was Greek to many readers.” The rare case of an author publishing a rewrite of his own paper with the content unchanged and only the exposition fixed.

The two are one argument, and they arrived here an hour apart. The 1982 paper ends by saying the only way to make arbitrary-fault tolerance affordable is to assume something about how components fail. The 1998 paper assumes benign failure, gets consistency under failure of any number of nodes and links, and states plainly what it gave up: no defence against malicious failure, no bounded-time response. Reading either alone loses the trade.

TLA+ is the same instinct at a third stage. Both papers reason about protocols by proving theorems about them on paper; TLA+ is machinery for doing that to systems whose proofs nobody would finish by hand. And what both papers keep circling — that the hard part is the assumptions rather than the algorithm — is what a specification language exists to make explicit.

Canonical node for Lamport across the hub. Add claims here as sources land rather than restating them in the spokes.