Improve TLA+ README

README.md

@@ -2,11 +2,13 @@
 
 My monorepo for formalization.
 
-[![Lean 4 CI](https://github.com/utensil/formal-land/actions/workflows/lean4.yml/badge.svg)](https://github.com/utensil/formal-land/actions/workflows/lean4.yml) [![TLA+ CI](https://github.com/utensil/formal-land/actions/workflows/tla.yml/badge.svg)](https://github.com/utensil/formal-land/actions/workflows/tla.yml) [![Aya CI](https://github.com/utensil/formal-land/actions/workflows/aya.yml/badge.svg)](https://github.com/utensil/formal-land/actions/workflows/aya.yml)
+[![Lean 4 CI](https://github.com/utensil/formal-land/actions/workflows/lean4.yml/badge.svg)](https://github.com/utensil/formal-land/actions/workflows/lean4.yml) [![Aya CI](https://github.com/utensil/formal-land/actions/workflows/aya.yml/badge.svg)](https://github.com/utensil/formal-land/actions/workflows/aya.yml) [![TLA+ CI](https://github.com/utensil/formal-land/actions/workflows/tla.yml/badge.svg)](https://github.com/utensil/formal-land/actions/workflows/tla.yml)
 
 - [Lean 4 Playground](./lean4/README.md)
   - [example index](https://utensil.github.io/formal-land/lean4/)
-- [Aya Playground](https://utensil.github.io/formal-land/aya/literate.aya.html)
+- [Aya Playground](./aya/README.md)
   - [haskeller-tutorial](https://utensil.github.io/formal-land/aya/haskeller-tutorial.html)
   - [prover-tutorial](https://utensil.github.io/formal-land/aya/prover-tutorial.html)
   - [literate](https://utensil.github.io/formal-land/aya/literate.html)
+- [TLA+ Playground](./tla/README.md)
+  - [pluscal.pdf](https://utensil.github.io/formal-land/tla/pluscal.pdf)

tla/README.md

@@ -0,0 +1,19 @@
+# TLA+ Playground
+
+[![TLA+ CI](https://github.com/utensil/formal-land/actions/workflows/tla.yml/badge.svg)](https://github.com/utensil/formal-land/actions/workflows/tla.yml)
+
+Experiments with [TLA+](https://lamport.azurewebsites.net/tla/tla.html).
+
+Some readings:
+
+- [The Future of TLA+](https://lamport.azurewebsites.net/tla/future.pdf)
+- [TLA⁺ is more than a DSL for breadth-first search](https://ahelwer.ca/post/2024-09-18-tla-bfs-dsl/)
+- [Why I use TLA+ and not(TLA+)](https://protocols-made-fun.com/specification/modelchecking/tlaplus/quint/2024/10/05/tla-and-not-tla.html)
+- [Learn TLA+](https://www.learntla.com/) with a focus on PlusCal
+- [TLA+ Examples](https://github.com/tlaplus/Examples)
+
+Related tech stack:
+
+- [Quint](https://quint-lang.org/): A modern and executable specification language based on TLA+, developed by 
+- [PlusCal](https://en.wikipedia.org/wiki/PlusCal): a gateway language to TLA+
+- [Apalache](https://apalache-mc.org/): A symbolic model checker for TLA+ specifications, via translation to SMT solvers such as Microsoft Z3