diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index cb46f39..78c87cc 100644
--- 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
new file mode 100644
index 0000000..ab1b48c
--- /dev/null
+++ 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/