1. Kaustuv C. Chaudhuri, Damien Doligez, Leslie Lamport & Stephan Merz (2008): A TLA+ Proof System. arXiv:0811.1914 [cs]. Available at
  2. Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts & Hernán Vanzetto (2012): TLA+ Proofs. arXiv:1208.5933 [cs], doi:10/dgpd. Available at
  3. Igor Konnov, Jure Kukovec & Thanh-Hai Tran (2019): TLA+ Model Checking Made Symbolic. Proceedings of the ACM on Programming Languages 3(OOPSLA), pp. 1–30, doi:10.1145/3360549. Available at
  4. Markus Alexander Kuppe (2014): Distributed TLC. Available at (Accessed 2016-09-06).
  5. Markus Alexander Kuppe (2019): Visualizing TLA+ Toolbox Error Traces with ShiViz. Available at
  6. Leslie Lamport (1994): The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems 16(3), pp. 872–923, doi:10.1145/177492.177726. Available at
  7. Leslie Lamport (1995): How to Write a Proof. The American mathematical monthly 102(7), pp. 600–608, doi:10.2307/2974556. Available at
  8. Leslie Lamport (2003): Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston.
  9. Leslie Lamport (2009): The PlusCal Algorithm Language. In: Martin Leucker & Carroll Morgan: Theoretical Aspects of Computing - ICTAC 2009 5684. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 36–60, doi:10/dcd6gv. Available at
  10. Leslie Lamport (2012): How to Write a 21st Century Proof. Journal of Fixed Point Theory and Applications 11(1), pp. 43–63, doi:10.1007/s11784-012-0071-6. Available at
  11. Leslie Lamport (2018): Using TLC to Check Inductive Invariance. Available at (Accessed 2018-08-16).
  12. Leslie Lamport (2019): Proving Safety Properties. Available at
  13. Leslie Lamport & Lawrence C. Paulson (1999): Should Your Specification Language Be Typed. ACM Transactions on Programming Languages and Systems 21(3), pp. 502–526, doi:10.1145/319301.319317. Available at
  14. D. Marples & P. Kriens (Dec./2001): The Open Services Gateway Initiative: An Introductory Overview. IEEE Communications Magazine 39(12), pp. 110–114, doi:10.1109/35.968820. Available at
  15. Jeff McAffer, Jean-Michel Lemieux & Chris Aniszczyk (2010): Eclipse Rich Client Platform, 2nd ed edition, The Eclipse Series. Addison-Wesley, Upper Saddle River, NJ. OCLC: ocn262433527.
  16. Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker & Michael Deardeuff (2015): How Amazon Web Services Uses Formal Methods. Communications of the ACM 58(4), pp. 66–73, doi:10.1145/2699417. Available at
  17. J. Steven Perry (2002): Java Management Extensions, 1st ed edition. O'Reilly, Beijing ; Cambridge [Mass.].
  18. Amir Pnueli (1977): The Temporal Logic of Programs. IEEE, pp. 46–57, doi:10.1109/SFCS.1977.32. Available at
  19. William Schultz (2018): An Animation Module for TLA+. Available at
  20. P. Shannon (2003): Cytoscape: A Software Environment for Integrated Models of Biomolecular Interaction Networks. Genome Research 13(11), pp. 2498–2504, doi:10.1101/gr.1239303. Available at
  21. Yuan Yu, Panagiotis Manolios & Leslie Lamport (1999): Model Checking TLA+ Specifications. In: Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, Laurence Pierre & Thomas Kropf: Correct Hardware Design and Verification Methods 1703. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 54–66, doi:10/fr3fsd. Available at

Comments and questions to:
For website issues: