标签
TLA+是一个模型检查工具，它通过探索所有状态交错来查找分布式系统中的缺陷；通过形式化验证，它帮助在Depot Registry的垃圾回收器中识别了一个遗漏的缺陷，从而提升了安全性。
Specula是一个代理系统，能够自动从代码推导TLA+规范，运行模型检查以发现并发错误，并通过集成测试复现这些错误。它在48个开源分布式和并发系统中发现了249个错误，展示了形式化验证的显著扩展。
Canonical 的 dqlite 团队使用 TLA+ 对 WAL 检查点机制中一个存在16年之久、可能导致数据库损坏的 SQLite 漏洞进行建模和理解，随后验证了 dqlite 是否受其影响。
本文形式化了多智能体LLM系统中的四种并发异常，机械验证了一个一致性层次结构，并提供了带有有界预防成本的经过验证的Rust运行时，包括对字节跳动deer-flow的修复以及LangGraph中的工具效应重排序的修复。
讨论了多智能体系统中共享状态的两个故障模式——并发丢失更新和僵尸写入者，并提出了一种带有栅栏写入者和模型验证保证的解决方案。
Specula 团队的研究人员创建了 SysMoBench 基准测试，用于评估大语言模型能否准确建模实际计算系统的 TLA+ 规范，还是仅仅照本宣科地背诵教材内容。该基准测试涵盖四个阶段共 11 个系统，揭示了当前大语言模型在准确建模系统实现与参考论文方面的系统性差距。
TLA+ 语义保证无序更新，但 TLC 模型检查器通过要求有序赋值并添加如 PrintT 等有副作用的运算符来破坏这些保证，导致初学者感到困惑。
Hillel Wayne 基于对社区项目的分析，讨论了尽管 LLM 在编写 TLA+ 和 Alloy 等形式化规范方面很受欢迎，但它们经常生成浅显、同义反复的属性，无法捕捉微妙的缺陷。