TLA+
----

<!--
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.

SPDX-License-Identifier: CC0-1.0
-->

[(Up)](../../README.md#topics) | _Wikipedia: [TLA+](https://en.wikipedia.org/wiki/TLA+)_ | _See also: [Formal Specification](../Formal%20Specification/README.md#formal-specification), [Model Checking](../Model%20Checking/README.md#model-checking)_

- - - -

Works regarding the specification language TLA+ and its underlying logic.

### Web resources

[The TLA+ Home Page](https://lamport.azurewebsites.net/tla/tla.html) ★

[Learn TLA+ --- Learn TLA+](https://www.learntla.com/) ★

[Practical TLA+ by Hillel Wayne](https://lamport.azurewebsites.net/tla/practical-tla.html) ★

[A liveness example in TLA+ -- Surfing Complexity](https://surfingcomplexity.blog/2024/10/16/a-liveness-example-in-tla/) ★★


### Repositories

[tlaplus/PlusPy: Python interpreter for TLA+ specifications](https://github.com/tlaplus/PlusPy) ★★ [💭](commentary/cpressey.md#tlaplus-pluspy-python-interpreter-for-tla-specifications)


### Papers

[The Temporal Logic of Actions](https://archive.org/details/bitsavers_dectechrep_507277) 🏛️ [💭](commentary/cpressey.md#the-temporal-logic-of-actions)

_(in [Software Engineering](../Software%20Engineering/README.md#software-engineering))_ Use of Formal Methods at Amazon Web Services (online @ [lamport.azurewebsites.net](https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf)) ★★★ [💭](commentary/cpressey.md#use-of-formal-methods-at-amazon-web-services)