Add reference to ai linter

FedericoPonzi · Jul 14, 2024 · 92a8be9 · 92a8be9
1 parent ae3e797
commit 92a8be9
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
@@ -33,6 +33,7 @@
     - [Generating Animations of State Changes](./using/generating-animation.md)
     - [(Github) CI for your specifications](./using/ci-for-specs.md)
     - [Generating GO from pluscal specs](./using/pgo-generating-go-from-pluscal.md)
+    - [AI Linter](./using/ai-linter.md)
     - [Known limitations](./using/limitations.md)
 - [TLA+ Tools Codebase](./codebase/intro.md)
     - [Contributing](./codebase/contributing.md)

diff --git a/src/using/ai-linter.md b/src/using/ai-linter.md
@@ -0,0 +1,4 @@
+# AI Linter
+TLA+ does not come with a traditional linter or formatter. The TLA+ AI Linter is a GenAI script that uses LLMs to lint TLA+ files.
+
+Find more info on: https://microsoft.github.io/genaiscript/case-studies/tla-ai-linter/