Leslie Lamport's 1979 definition of sequential consistency gave shared-memory programmers a precise contract: concurrent execution should look like one interleaving that preserves each processor's program order.
Leslie Lamport's 1974 bakery algorithm showed that mutual exclusion could be achieved using ordinary shared reads and writes, even under surprisingly weak assumptions about overlapping memory operations.
TLA+ combines state-transition modeling, temporal logic and model checking so engineers can find concurrency and distributed-system design errors before implementation.
Leslie Lamport's 1978 work showed that distributed programs can reason about causal order without pretending every machine shares a perfectly synchronized physical clock, establishing logical clocks and the happened-before relation as foundational distributed-systems abstractions.
Research by Marshall Pease, Robert Shostak, Leslie Lamport, and the SIFT team exposed a hard boundary in distributed agreement: a faulty participant may send different lies to different peers, so redundancy alone is not enough unless the protocol accounts for adversarially inconsistent behavior.
Leslie Lamport's Paxos algorithm gave crash-fault-tolerant distributed systems a rigorous way to agree on values despite delays and failures, but its unusual original presentation also created a second history: decades of work translating the proof into systems engineers could confidently implement.