From 92a8be9291f6693339722367581825dfd12f8505 Mon Sep 17 00:00:00 2001 From: Federico Ponzi Date: Sun, 14 Jul 2024 21:21:53 +0100 Subject: [PATCH] Add reference to ai linter --- src/SUMMARY.md | 1 + src/using/ai-linter.md | 4 ++++ 2 files changed, 5 insertions(+) create mode 100644 src/using/ai-linter.md 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/