From b7a48ce25907457a7bf294137de1c1770d6b73fc Mon Sep 17 00:00:00 2001
From: Dane Sabo <dane.sabo@pitt.edu>
Date: Mon, 10 Feb 2025 15:36:19 -0500
Subject: [PATCH] vault backup: 2025-02-10 15:36:19

---
 3-99 Research/TLA/TLA Canvas.canvas        | 2 +-
 3-99 Research/TLA/What is TLA good for?.md | 0
 3-99 Research/TLA/What is TLA?.md          | 5 +++--
 3 files changed, 4 insertions(+), 3 deletions(-)
 create mode 100644 3-99 Research/TLA/What is TLA good for?.md

diff --git a/3-99 Research/TLA/TLA Canvas.canvas b/3-99 Research/TLA/TLA Canvas.canvas
index 4f88bea7..69a8289c 100644
--- a/3-99 Research/TLA/TLA Canvas.canvas	
+++ b/3-99 Research/TLA/TLA Canvas.canvas	
@@ -1,6 +1,6 @@
 {
 	"nodes":[
-		{"id":"167f0f0792ba9aa0","x":-300,"y":-500,"width":540,"height":180,"type":"text","text":"What the hell is TLA+?\n\nApparently, it's a formal specification language by Leslie Lamport, who legendarily made $\\LaTeX$. \n\nAlso, apparently it is TLA$^+$. It stands for Three Letter Acronym."}
+		{"id":"7c5e7263708dba1b","x":-720,"y":-880,"width":520,"height":440,"type":"file","file":"3-99 Research/TLA/What is TLA?.md"}
 	],
 	"edges":[]
 }
\ No newline at end of file
diff --git a/3-99 Research/TLA/What is TLA good for?.md b/3-99 Research/TLA/What is TLA good for?.md
new file mode 100644
index 00000000..e69de29b
diff --git a/3-99 Research/TLA/What is TLA?.md b/3-99 Research/TLA/What is TLA?.md
index 8e1ebe3b..86f726e4 100644
--- a/3-99 Research/TLA/What is TLA?.md	
+++ b/3-99 Research/TLA/What is TLA?.md	
@@ -3,5 +3,6 @@ TLA$^+$ stands for Three Letter acronym. It was invented by Leslie Lamport, who
 
 There is a nice [learntla](https://learntla.com/intro/faq.html#what-s-tla) website set up by the community, mostly by Hillel Wayne
 
-TLA stands for 'Temporal Logic of Actions'.
-## What's TLA+ good at?
+TLA stands for 'Temporal Logic of Actions'. It's a formal specification language.
+
+TLA mainly works with a tool called TLC, which is a model checker. TLC is exhaustive, and will check every possible case.