diff --git a/tlaplus/README.md b/tlaplus/README.md
new file mode 100644
index 0000000..c7cfdb1
--- /dev/null
+++ b/tlaplus/README.md
@@ -0,0 +1,47 @@
+# TLA+ Specifications
+
+This directory contains TLA+ formal specifications for the GithubWorkflowTool project.
+
+## About TLA+
+
+TLA+ is a formal specification language developed by Leslie Lamport for designing, modeling, documenting, and verifying concurrent systems and algorithms. It's particularly useful for:
+
+- Modeling distributed systems and concurrent processes
+- Verifying correctness properties
+- Finding subtle bugs in system designs
+- Documenting system behavior formally
+
+## Purpose
+
+The TLA+ specifications in this directory formally model key components of the GithubWorkflowTool, including:
+
+- Workflow execution semantics
+- Job dependency resolution
+- Concurrent job execution
+- State transitions in the workflow engine
+- Cache and artifact management
+
+## Tools
+
+To work with TLA+ specifications, you'll need:
+
+- **TLA+ Toolbox**: The IDE for TLA+ (https://lamport.azurewebsites.net/tla/toolbox.html)
+- **TLC Model Checker**: For checking specifications (included with the Toolbox)
+- **TLAPS**: The TLA+ Proof System (optional, for formal proofs)
+
+## File Structure
+
+TLA+ specification files typically have the `.tla` extension. Each specification may include:
+
+- Module definitions
+- Constants and variables
+- Initial state predicates
+- Next-state actions
+- Invariants and temporal properties
+
+## Resources
+
+- [TLA+ Homepage](https://lamport.azurewebsites.net/tla/tla.html)
+- [Learn TLA+](https://learntla.com/)
+- [TLA+ Examples](https://github.com/tlaplus/Examples)
+- [Specifying Systems Book](https://lamport.azurewebsites.net/tla/book.html)