The current state of TLA⁺ development
a year ago
- #Model Checking
- #TLA+
- #Software Development
- 2025年TLA+社区大会在加拿大安大略省汉密尔顿市的麦克马斯特大学举行。
- 活动期间举办了题为《编写TLA+工具从未如此简单！》的讲座，探讨了TLA+开发现状。
- 核心议题包括：现有TLA+语言工具概览、遗留代码挑战应对策略以及未来发展构想。
- 现有工具链涵盖解析器（SANY、TLAPM、tree-sitter-tlaplus）、解释器（TLC、Spectacle）和模型检测器（TLC、Apalache、Spectacle）。
- 其他重要工具包括TLAPM、Snowcat类型检查器、TLA+格式化工具、LSP服务器、TLAUC及VS Code扩展插件。
- 当前挑战主要来自SANY和TLC等遗留代码维护，这些庞大的Java旧代码库现存知识体系有限。
- 应对策略包括建立完整测试套件、优化开发者入门流程，以及提供开发补助金和津贴支持。
- 未来方向涉及TLA+工具的生成式测试、语法简化方案以及SANY接口优化。
- 『每分钟十亿状态计划』旨在通过开发字节码解释器，大幅提升TLC模型检测器的吞吐量。
- TLA+基金会持续支持工具开发，并积极寻求更多贡献者加入。