生成AI加速的TLA+挑战赛

TLA+基金会推出挑战赛，鼓励开发结合生成AI和LLM的TLA+工具。

参与者可提交项目，争夺Nvidia显卡等奖品。

提交截止日期为2025年7月3日，需符合参与条件并发布MIT许可证。

TLA+是一种用于建模和验证并发及分布式系统的形式化规范语言。

挑战赛旨在促进将生成AI和LLM的能力带入TLA+的实用和创新工具、工作流程和方法。

奖项包括：第一名获得Nvidia GeForce RTX 5090，第二名和第三名分别获得Github Copilot Pro+和Pro的订阅。

参与者可提交的项目包括智能重构TLA+规范、LLM增强的开发工具、教育中的自动评分工具等。

提交将由TLA+规范语言委员会评审，评估标准包括功能性、与TLA+生态系统的相关性和AI的合理使用。

所有提交必须在MIT许可证下发布，任何基础AI模型必须公开可用。

参与者需在TLA+社区有过先前的参与，不得为TLA+基金会董事会或规范语言委员会成员。

提交时间为公告发布后两个月内，评审将在提交期结束后一个月内进行。