The cycle treats AI as infrastructure—something that already runs beneath the decisions of daily life and that will run more deeply still. Distributed systems are the engineering substrate of that infrastructure, and their properties determine what “reliable,” “consistent,” and “available” can mean when a model is deployed at planetary scale. The CAP theorem's core trade-off—that you cannot have both perfect consistency and perfect availability when the network can partition—is a fundamental constraint on how AI systems behave under failure, and it is a constraint whose existence most users of AI systems are unaware of.
The alignment implications are direct. A large language model deployed across hundreds of replicas may return different responses from different nodes due to replica lag, software version skew, or the stochastic sampling that makes responses non-deterministic. Users experience this as inconsistency without understanding its source. Lamport's safety-and-liveness framework gives the vocabulary for specifying what an AI system must guarantee across these conditions: which properties must hold of every response (safety), and which properties must eventually hold of the system as a whole (liveness). Without formal specifications of this kind, “reliability” is a marketing claim rather than an engineering property.
Distributed systems emerged as a distinct field from the convergence of time-sharing operating systems, ARPANET, and the recognition in the 1970s that networks of machines posed problems qualitatively different from single-machine concurrency. Lamport's 1978 clock paper was foundational; the subsequent decade saw the formalization of failure models (crash-fail, fail-stop, Byzantine) and the discovery of fundamental impossibility results. Fischer, Lynch, and Paterson's 1985 FLP impossibility theorem proved that no deterministic consensus algorithm can tolerate even a single process failure in an asynchronous system—a result that clarified why Paxos and related protocols require synchrony assumptions to achieve liveness.
The field matured with the internet boom of the 1990s and 2000s, as Google, Amazon, and others built systems at scales that required fresh theoretical and engineering work. Brewer's 2000 conjecture (proved by Lynch and Gilbert in 2002) became the field's most consequential design constraint. The NoSQL movement of the 2000s was largely a practical response to the CAP theorem: choosing partition tolerance and availability over strict consistency, and designing applications to tolerate eventual consistency. AI serving systems inherit this entire history: they are built on top of distributed key-value stores, consensus protocols, and load balancers whose design trade-offs were established by Lamport and his successors.
Happens-before and causal order. Lamport defined the happens-before relation: event A happens before event B if A precedes B in the same process, or A sends a message that B receives, or there is a chain of such relations. This partial order is the correct notion of time in a distributed system. Logical clocks assign integers to events in a way that respects happens-before; vector clocks (Fidge and Mattern, 1988) capture it exactly, allowing causal ordering without physical synchronization.
The CAP theorem. A distributed system can provide at most two of: consistency (all nodes see the same data at the same time), availability (every request receives a response), and partition tolerance (the system continues operating when network partitions split nodes). Since real networks do partition, the practical trade-off is between consistency and availability. Modern AI inference infrastructure typically prioritizes availability—returning a response even if replica state is stale—with consistency achieved eventually.
Byzantine fault tolerance. The Byzantine Generals Problem, formalized by Lamport, Shostak, and Pease (1982), asks how processes can reach consensus when some of them may behave arbitrarily—sending conflicting messages, lying about their state, or colluding. The result: consensus is achievable with Byzantine faults if and only if fewer than one-third of participants are faulty, and requires at least 3f+1 processes to tolerate f failures. This is directly relevant to federated AI systems, where some participants may be adversarial, and to multi-agent AI architectures where trust cannot be assumed.
Formal specification of distributed protocols. Lamport's TLA+ allows engineers to write formal specifications of distributed protocols and check all possible executions using a model checker. The safety and liveness properties of Paxos, Raft, and other consensus algorithms can be stated and verified in TLA+ before a line of implementation code is written. The technique has caught bugs in production cloud systems that years of testing missed. It is the practical implementation of the provable correctness ideal for distributed programs.