GenAI 加速的 TLA+ 挑战赛

由 TLA+ Foundation 与 NVIDIA 合作，隆重推出 GenAI-accelerated TLA+ 挑战赛——公开征集探索 TLA+ 和生成式 AI 交叉领域的作品。

本次活动旨在促进实用和创新的工具、工作流程和方法，将生成式 AI 和 LLM 的能力引入 TLA+。 邀请参与者开发面向工程的解决方案，通过集成 GenAI 来提高形式化规范的可用性、可访问性和自动化程度。

奖项

• 一等奖： Nvidia GeForce RTX 5090 (由 NVIDIA 赞助)
• 二等奖： 一年期单用户 Github Copilot Pro+ 个人订阅 (由 TLA+ Foundation 赞助)
• 三等奖： 一年期单用户 Github Copilot Pro 个人订阅 (由 TLA+ Foundation 赞助)

示例项目领域

参与者可以提交包括但不限于以下领域的工作：

• TLA+ 规范的智能重构 (例如，在添加变量时正确管理 UNCHANGED)
• LLM 增强的 linters、formatters 或其他开发工具
• LLM 驱动的自动化教育评分工具
• 规范或执行轨迹的可视化
• 为 Apalache 等工具生成类型注解
• 归纳不变式候选式的合成，通过 TLC 或 Apalache 验证
• TLAPS 证明的合成
• 从源代码和设计文档合成整个规范

评估

提交的作品将由 TLA+ Specification Language Committee (SLC) 评审。

评审团将根据作品的功能、与 TLA+ 生态系统的相关性以及对 AI 的周到使用情况来评估提交的作品。 提交的作品必须可由评审团重现。 仅被动形式（例如单独的视频）是不够的。 但是，评审团不要求完全完善的产品——原型就足够了。 所有提交的作品都必须在 MIT license 下发布，并且任何底层 AI 模型都必须公开可用。

明确鼓励使用 GenAI/LLM，前提是任何 AI 生成的内容（例如 specs、invariants、visualizations 等）都使用某种形式的验证（例如 TLA+ 工具）进行检查。

在 TLA+ Community Event 2025 上观看 live announcement!

参与标准

符合资格的参与者必须满足以下条件：

• 之前与 TLA+ 社区有过互动（例如，向 mailing lists、forums、open-source repositories、conference presentations 或 academic publications 做出贡献）
• 不得为 TLA+ Foundation Board 或 Specification Language Committee 的成员
• 不得受到任何可能妨碍参与的法律、合同、出口管制或管辖限制

提交时间表和公布

提交将与此公告同时开放。 提交参赛作品的截止日期为 2025 年 7 月 3 日公告之日起两个月。 提交的作品必须发送至 genai@tlapl.us。 评审团将在提交期结束后一个月选出获奖者。 我们欢迎创新、技术上强大且具有实际价值的贡献，这些贡献探索并扩展了 GenAI 在 TLA+ 上下文中的潜力。

对于与 TLA+ 相关的长期或基础工程和研究工作，我们鼓励您探索 TLA+ grant program。