The internet discovers TLA+. Now what?
6 hours ago
- TLA+是一种用于描述系统行为和时序属性的形式化建模语言，最近通过Boris Cherny的推文在智能体编程中流行起来。
- 它用状态和动作建模迁移系统，以及安全性（不发生坏事）和活性（好事最终发生）等时序属性。
- TLA+模型检查（TLC）探索有限状态空间；它无法验证任意系统规模，也无法确保实现与模型一致。
- 局限性包括规范与实现之间的差距、TLA+证明器的自动化程度有限，以及无法表达超越LTL的分支时间或策略属性。
- 现代证明系统如Lean和Verus可以将TLA+模型扩展到机器验证的证明；Verus将规范与证明嵌入到Rust代码中。
- Reasonable构建了一个管道，将16,459个TLA+规范/属性对翻译成3,000多个机器验证的Verus证明，使用了带有反作弊检查的证明者-审查者循环。
- 这项工作旨在通过精化证明、程序合成、协议搜索以及更丰富的多智能体系统逻辑来缩小形式化模型与真实软件之间的差距。
- 未来的文章将详细介绍该管道、数据集以及AI模型在时序证明生成上的评估。