tla-plus

Specula 团队的研究人员创建了 SysMoBench 基准测试，用于评估大语言模型能否准确建模实际计算系统的 TLA+ 规范，还是仅仅照本宣科地背诵教材内容。该基准测试涵盖四个阶段共 11 个系统，揭示了当前大语言模型在准确建模系统实现与参考论文方面的系统性差距。

TLA+ 语义保证无序更新，但 TLC 模型检查器通过要求有序赋值并添加如 PrintT 等有副作用的运算符来破坏这些保证，导致初学者感到困惑。

Hillel Wayne 基于对社区项目的分析，讨论了尽管 LLM 在编写 TLA+ 和 Alloy 等形式化规范方面很受欢迎，但它们经常生成浅显、同义反复的属性，无法捕捉微妙的缺陷。