这是 TLA⁺ 基金会每月开发更新的创刊版。作者为Andrew Helwer，总结了过去一个月的开发情况，包括非编码相关和编码相关的社区发展，以及作者自己的工作。

• 非编码相关发展与公告：

  • Leslie Lamport出版新书《A Science of Concurrent Programs》，可免费下载，实体版正在筹备中。
  • 宣布 2025 年 TLA⁺ 社区活动，与 2025 年 ETAPS 联合举办，演讲提案提交截止日期为 2025 年 2 月 7 日。
  • 东大西洋地区的 ABZ 2025 将在 2025 年 6 月 10 日至 13 日于德国杜塞尔多夫举行，欢迎提交 TLA⁺ 相关论文，摘要提交截止日期为 2025 年 2 月 3 日。
  • Jack Vanlighty写了一篇关于使用 TLA⁺ 获取分布式系统设计统计属性的博客文章。
  • Lorin Hochstein发表了三篇关于在 TLA⁺ 中指定序列化和多版本并发控制等内容的优秀博客文章。
  • 在 11 月的虚拟社区会议上，Feng Wenhan展示了使用 TLC 状态图导出功能进行基于模型的测试的工作，并提出设计稳健状态图导出格式的提案。
  • Leslie Lamport 宣布年底退休，享年 83 岁。

• 编码相关社区发展：

  • Federico Ponzi正在原型化 TLA⁺ 格式化程序，包括确定默认设置。
  • Julia Ferraioli为 TLA⁺ 基金会网站添加了博客功能。
  • William Schultz发布了 Scimitar，一种基于 TLA⁺ 中归纳证明分解技术的分布式协议安全性验证工具。
  • Hillel Wayne开始为 TLA⁺ VS Code 插件做出贡献，为 PlusCal 添加了一些诊断消息。
  • Ioannis Filippidis为 TLA⁺ 证明管理器 (TLAPM) 添加了对绑定元组量化的支持。
  • 欢迎 Mathieu Borderé成为新贡献者，他提交了第一个 PR，改进了解析器的命令行帮助输出。
  • 长期的 TLA⁺ 工具维护者 Markus Kuppe提交了许多更改，包括针对 TLA⁺ 调试器、杂项错误修复和一些设计层面的工作。
  • Finn Hackett发现 TLC 存在一个问题，即从磁盘读取非 ASCII 字符串会导致崩溃，一个修复正在等待审查。

• 作者自己的工作：

  • 改编 TLA⁺ 语法测试语料库用于 TLAPM，在解析器中发现了一些问题，并编写了约 50 个额外的语法测试，这些测试被回溯到 TLA⁺ Java 工具和 tree-sitter-tlaplus 语法。
  • 研究将 TLAPM 的解析器转换为使用 SANY，提交了一些修复以清理 XML 导出器，并在 OCaml 中编写了一个 XML 输出的原型消费者，但认为该项目风险较高。
  • 扮演 TLAPM 维护者的角色，进行了一些开发基础设施的更改，如修复不稳定的 CI 构建、添加开发文档、寻找减少发布大小的方法以及设置 TLAPM 的滚动预发布。
  • 为 Java 基础的 TLA⁺ 工具提交了一些一次性的错误修复和增强功能。
  • 提出了关于标准化人类可读错误代码的提案。
• 新手角落：本月的新手友好问题是 TLA⁺ 解析器无法处理字符串中的反引号，这是一个很好的入门问题，因为所需的更改很局部，且代码库的语法解析器部分经过了良好的测试，有标准的 TLA⁺ 语法测试语料库可供参考。希望有人在 12 月接手这个问题。