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