From 76c601a5e36ab732451c136eb23b55ce4fff6912 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 11 Aug 2026 09:45:04 -0700 Subject: [PATCH 1/2] Create AI usage policy for TLA Examples Added a comprehensive AI usage policy for the TLA Examples project, outlining rules for AI contributions, human oversight, and the responsibilities of contributors. Adopted from https://github.com/apalache-mc/apalache/blob/main/AI_POLICY.md (with the help of Opus 5). Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- AI_POLICY.md | 101 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 101 insertions(+) create mode 100644 AI_POLICY.md diff --git a/AI_POLICY.md b/AI_POLICY.md new file mode 100644 index 00000000..ebd32abe --- /dev/null +++ b/AI_POLICY.md @@ -0,0 +1,101 @@ +# TLA+ Examples AI Usage Policy + +The TLA+ Examples project has strict rules for AI usage: + +- **All AI usage in any form must be disclosed.** You must state the tool you +used (e.g. Codex, Claude Code, Cursor, Copilot) along with the extent that the +work was AI-assisted. + +- **The human-in-the-loop must fully understand all TLA+ they contribute.** If +you can't explain what your specification does and how it models the system +without the aid of AI tools, do not contribute it to this project. + + In particular, if you are new to TLA+, you must be able to explain all TLA+ + constructs in your contribution. AI tools are great helpers for learning. Use + them to understand your specification. + +- **Issues and discussions must be written by humans.** AI tools are good at +producing lengthy prose, but this prose is hard to read for humans. We prefer +text that demonstrates human reasoning. It is okay to have spelling and grammar +mistakes, as long as you have put some thinking into your writing. + + If you use AI to do research, you may quote the results of that research in a + clearly marked blockquote. However, you must verify the results before quoting + them, and you must trim the results down to the relevant information. + +- **Descriptions of Pull Requests must be written by humans.** Pull requests +should specify: the intent of the change, the key design decisions, the parts of +the specification or repository affected, and the key changes (briefly). The +size of the PR text must be proportional to the size of the change. A small +change does not need a 5-page description. + +- **No AI-generated media is allowed (art, images, videos, audio, etc.).** Text, +TLA+ specifications, and code are the only acceptable AI-generated content, per +the other rules in this policy. + +- **The number of active Pull Requests is limited.** It takes effort to open a +high-quality Pull Request. You have to prioritize your contributions and submit +the important ones first. + +- **Signed-off-by and Developer Certificate of Origin.** AI agents MUST NOT add +Signed-off-by tags. Only humans can legally certify the Developer Certificate of +Origin (DCO). The human submitter is responsible for: + + - Reviewing all AI-generated content + + - Ensuring compliance with licensing requirements + + - Adding their own Signed-off-by tag to certify the DCO + + - Taking full responsibility for the contribution + + Moreover, read the [LF Guidance on Generative AI][lf-generative-ai] to + understand the copyright and licensing implications of using AI tools. + +**The above rules apply only to outside contributions to TLA+ Examples**. Maintainers +are exempt from these rules and may use AI tools at their discretion. They have +proven themselves trustworthy to apply good judgment. + +## There are Humans Here + +Please remember that TLA+ Examples is maintained by humans. The specifications in this +repository have been written and curated by humans. This means that many specification, +modeling, and repository decisions do not follow the canned recipes of the AI tools. +Due to that, the AI tools may fail to understand the intent behind a specification. + +Every discussion, issue, and pull request is read and reviewed by humans (and +sometimes machines, too). It is a boundary point at which people interact with +each other and the work done. It is rude and disrespectful to approach this +boundary with low-effort, unqualified work, since it puts the burden of +validation on the maintainers. Most of the time, the maintainers are not paid +for doing this work, and they aim at improving the project quality, not reading +the inference of AI tools. + +## AI is Welcome Here + +The maintainers of TLA+ Examples embrace the use of AI. We are careful about +the specifications in this repository, as they have been written and curated by +humans, who put plenty of their thought into them. + +**Our reason for the strict AI policy is not due to an anti-AI stance**. We +understand that many external contributors are trying to help the project. We +also know that it is tempting to shoot an AI tool at a problem and see it +"solved". Unfortunately, the AI tools do not have understanding of the impact +of their output. We may see TLA+ that appears to solve the problem or correctly +specify a system, but is not properly understood by the contributor, integrated +into the repository, or tested. As a result, the maintainers can have to spend +hours of their time validating or fixing work that was generated in minutes. + +## References + +This policy is adapted from the [Apalache AI Usage Policy][apalache-ai-policy], +which derives from the following AI policies and guidelines: + + - Large parts of the [Ghostty AI Policy][ghostty-ai-policy] + - [Linux Foundation Generative AI Policy][lf-generative-ai] + - [Kernel Coding Assistants][kernel-coding-assistants] + +[apalache-ai-policy]: https://github.com/apalache-mc/apalache/blob/main/AI_POLICY.md +[ghostty-ai-policy]: https://github.com/ghostty-org/ghostty/blob/main/AI_POLICY.md +[lf-generative-ai]: https://www.linuxfoundation.org/legal/generative-ai +[kernel-coding-assistants]: https://kernel.org/doc/html/next/process/coding-assistants.html From 3aacb57873ee7d5e1a08072461c2e96e84c9e542 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 12 Aug 2026 19:35:02 -0700 Subject: [PATCH 2/2] Address review feedback about PR limits Signed-off-by: Markus Alexander Kuppe --- AI_POLICY.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/AI_POLICY.md b/AI_POLICY.md index ebd32abe..99206ce3 100644 --- a/AI_POLICY.md +++ b/AI_POLICY.md @@ -33,9 +33,10 @@ change does not need a 5-page description. TLA+ specifications, and code are the only acceptable AI-generated content, per the other rules in this policy. -- **The number of active Pull Requests is limited.** It takes effort to open a -high-quality Pull Request. You have to prioritize your contributions and submit -the important ones first. +- **Review capacity is the bottleneck of this project.** Do not assume your Pull +Request will be reviewed, however sound it is. It has to be compelling enough +that a maintainer chooses to spend their time on it, so open the contributions +that matter most, not everything you can produce. - **Signed-off-by and Developer Certificate of Origin.** AI agents MUST NOT add Signed-off-by tags. Only humans can legally certify the Developer Certificate of