主要观点：

• 作者 Igor Konnov 分享了在 TLA+ 生态系统中的经历和思考，包括使用 TLA+ 的原因、从 Informal Systems 和 Cosmos 区块链项目中获得的经验教训以及关于概念和思维模型的见解。
• 强调 TLA+ 与作者之前的模型检查知识相契合，具有明确的语义、方便的原语、灵活的逻辑和良好的自动化分析水平。
• 介绍了 Informal Systems 在使用 TLA+ 和 Apalache 过程中的改进，如类型检查器、随机符号执行、折叠/减少替代递归以及提高稳定性等。
• 指出在与工程师的交流中，存在对 TLA+ 语法、过度编程和语言转换等方面的问题，同时介绍了相关的工具和概念，如 JSON 格式的跟踪输出和 mental models 等。

关键信息：

• 作者自 2016 年开始从事 TLA+ 相关工作，曾在 Informal Systems 工作，现已离职。
• TLA+ 易于理解和使用，与模型检查算法相关知识有良好的结合，具有明确的数学语义和方便的原语。
• Apalache 在类型检查、随机符号执行、折叠/减少等方面进行了改进，提高了稳定性和效率。
• 与工程师的交流中发现对 TLA+ 语法、编程方式和语言转换的需求，以及通过 mental models 来理解和学习 TLA+ 的重要性。

重要细节：

• Leslie Lamport 发布了关于 TLA+ 未来的文档，Andrew Helwer 撰写了相关博客，prestonph 询问了关于 Quint 的意见。
• TLA+ 可以轻松表达并发算法、智能合约等，与针对特定编程语言的验证工具相比具有优势。
• Apalache 的类型检查器在 2021 年和 2022 年进行了重写和改进，引入了精确的记录类型推断。
• 随机符号执行命令 apalache-mc simulate 效率高但牺牲了完整性，在某些情况下能比有界模型检查更快地找到反例。
• 递归运算符在有界模型检查中存在问题，Apalache 已改为使用折叠/减少操作。
• 在与工程师的交流中，存在对 TLA+ 语法的误解和过度编程的情况，以及对语言转换的需求。
• 通过阅读《The Design of Everyday Things》等书籍，理解了 conceptual models 和 mental models 在 TLA+ 中的重要性，TLC 是学习 TLA+ 的快速反馈方式。