把并发问题说清楚
莱斯利·兰波特（Leslie Lamport）研究多个计算进程如何协调，以及怎样证明它们遵守预期规则。他于1960年获麻省理工学院数学学士学位，1972年获布兰代斯大学数学博士学位，先后在SRI、DEC及微软研究院等机构工作，并获得2013年度图灵奖。
他的研究强调区分要实现的性质与实现步骤。并发系统中，一个看似无害的延迟或动作交错可能改变结果，因此不能只用正常运行时的直觉判断协议。不同问题还具有不同失败模型：他与Robert Shostak、Marshall Pease合作的1982年《拜占庭将军问题》，就不能与其个人署名的逻辑时钟或Paxos论文混为同一成果。
参考：[1]
消息先后与逻辑时钟
1978年论文以“先发生于”关系描述分布式事件：同一进程中的先后顺序、消息发送先于接收，以及这些关系的传递共同形成偏序。若两个事件之间没有这样的联系，系统未必能给出因果先后；为它们强加一个排列，并不等于发现了真实的全局时间。
例如甲把逻辑时间戳5附在消息上发给乙，乙接收前的计数为2，便可把接收事件记为6。每个进程在相邻事件间递增计数，接收消息时使新计数大于消息时间戳，就能保证有先发生关系的事件得到递增标记。反过来，时间戳较小不证明存在因果关系。再用进程编号打破相同时间戳，可构造与偏序兼容的全序，但它不是物理时钟同步。
参考：[2]
一致决定与继续运行是两件事
Paxos关注的是参与者可能停止、恢复或失去消息时，如何仍不作出互相矛盾的决定。《兼职议会》于1998年发表，以虚构议会记录法令的故事解释协议。相交的表决法定集合与对既有表决记录的约束，使后来的成功表决不能随意推翻已经选定的值；把这类决定组织为命令序列，可用于复制状态机。
安全性要求不出现冲突决定，活性则要求最终能够作出决定。原协议在其非拜占庭故障及持久记录等假设下维持一致性，但并不保证任意失联状态下都能继续工作。推进还需要足够长的稳定时期、多数参与者可用并及时处理消息。它也不容忍任意恶意行为，更不承诺固定响应时限。逻辑时钟能够帮助排序，却不会自动提供这些共识保证。
参考：[3]
规范、证明与另一种软件成果
动作时态逻辑（TLA）把系统行为及其应满足的性质写在同一种逻辑中。状态给变量赋值，动作描述状态之间的变化，时态表达式则用于讨论随执行持续成立或最终成立的性质。于是，证明实现满足规范可以表述为逻辑蕴含，而不是仅靠逐条阅读源代码或枚举几个成功样例。
兰波特后来以TLA+发展系统规范语言，2002年出版《Specifying Systems》。这种高层描述不等同于可执行产品本身，结论也取决于模型和假设。另一个广为人知的成果LaTeX源于他在TeX上编写的文档宏，属于排版系统；它与分布式算法研究共享作者，却处理不同问题。区分这些工作，才能准确理解兰波特的研究范围。