People
Leslie Lamport
is the inventor of TLA+ and PlusCal and the initiator of the TLA+ project . Contact him if you have any comments about the languages or tools, if you find a bug in the TLA+ tools, or if you find a mistake in the book not already described in the errata.
Damien Doligez
is a member of the Inria formal methods project, working on the Zenon prover that he developed. He participated in the design of the TLA+ proof language.
Denis Cousineau
is a member of the Inria formal methods project, working on the TLA proof manager.
Daniel Ricketts
is a member of the Inria formal methods project. He is working on the TLA Toolbox, for which he developed the Trace Explorer and did the TLATeX integration).
Simon Zambrovski
was the initial developer of the TLA Toolbox and did most of the implementation of the initial release. He continues to work on the toolbox. He is also responsible for this web page, doing the hosting, page layout, design, and realization.
Stephan Merz
is a member of the Inria formal methods project. He participated in the design of the TLA+ proof language, and is responsible for integrating Isabelle into the TLA Proof System as a back end prover.
Yuan Yu
developed the TLA+ Model Chcker (TLC) and implemented part of the TLA+ Parser (SANY) .
Kaustuv Chaudhuri
was a member of the Inria formal methods project, where he designed and implemented the TLA Proof System’s Proof Manager. He also participated in the design of the TLA+ proof language. He continues to maintain and develop the Proof Manager.
Jean-Charles Grégoire
implemented the initial version of the TLA parser.
David Jefferson
implemented most of the initial version of SANY.
Georges Gonthier
helped design the TLA+ proof language and developed the semantics of recursive operator definitions.
