PeopleofSuperintelligence

Researcher

Leslie Lamport

Leslie Lamport is a computer scientist whose TLA+ formal language now appears in AI-assisted specification work. He earned mathematics degrees at MIT and Brandeis, then built a career in industrial research and published work on logical clocks, Byzantine failures, LaTeX, TLA, and Paxos. The ACM named him the 2013 Turing Award winner for his contributions to distributed computing. As of October 2026, he is an Emeritus Researcher at Microsoft Research.

Works
375
Citations
51,766
h-index
70

Publication numbers from OpenAlex, as of 15 October 2026.

Timeline

  1. 1960–1972

    Mathematics degrees

    He earns a mathematics bachelor's degree at MIT in 1960, a master's degree at Brandeis in 1963, and a doctorate there in 1972.

  2. 1970–1985

    Logical clocks and Byzantine failures

    He begins at Massachusetts Computer Associates in 1970 and joins SRI International in 1977, where he coauthors papers on Byzantine failures. His 1978 paper Time, Clocks and the Ordering of Events in a Distributed System describes the synchronization of logical clocks.

  3. 1980s

    Creating LaTeX

    Lamport begins LaTeX as a set of TeX macros in the early 1980s. Addison-Wesley publishes LaTeX: A Document Preparation System in 1986.

  4. 1994

    The Temporal Logic of Actions

    In 1994, he publishes TLA, a formalism for describing and reasoning about concurrent systems through mathematical specifications.

  5. 1998–2001

    Paxos consensus

    His 1998 paper The Part-Time Parliament presents Paxos as a consensus protocol. In 2001, he writes Paxos Made Simple to explain the algorithm.

  6. 2013

    An ACM Turing Award

    The ACM names him the 2013 Turing Award winner for his work on distributed systems.

  7. By 2026

    TLA+ in AI engineering

    By 2026, a Northern Arizona University AI project uses his TLA+ language to convert natural-language requirements into formal specifications checked by the TLC model checker.

  8. As of October 2026

    Emeritus researcher at Microsoft

    As of October 2026, he is a computer scientist and an Emeritus Researcher at Microsoft Research.

Sources and credits

Photo: We have no published photo of Leslie Lamport yet. Send us a free-licensed photo.

  1. Leslie Lamport computerhistory.org. Checked 14 October 2026.
  2. The Writings of Leslie Lamport lamport.azurewebsites.net. Checked 14 October 2026.
  3. Leslie Lamport Receives Turing Award microsoft.com. Checked 14 October 2026.
  4. The Temporal Logic of Actions microsoft.com. Checked 14 October 2026.
  5. Leslie Lamport at Microsoft Research microsoft.com. Checked 14 October 2026.
  6. LegitCode | LeGIT/AI Project ceias.nau.edu. Checked 14 October 2026.