标签
该论文提出有界续写分析（BCA），通过概率模型检查量化自回归语言模型中隐藏的有害生成概率，以补充传统的攻击成功率（ASR）指标，更好地揭示表面拒绝之下的分布脆弱性。
ASMC 是一个将 Ghidra 的 p-code 汇编语义提升到 CBMC GOTO IR 的开源工具，用于对 x86-64 汇编进行有界模型检查，支持汇编验证、翻译验证与 C 级规格断言等多种用途。
Hillel Wayne 解释了 TLA+ 能验证哪些性质（安全不变式、动作性质、活性），以及仍存在哪些局限。在 Boris Cherny 提到 Claude 的 Opus 曾用 TLA+ 找出竞态条件之后，这篇文章为形式化方法的热度降降温。
本文讨论了在 TLA⁺ 中表达可达性属性的可能性，参考了 Leslie Lamport 的工作以及 TLC 模型检查器的局限性。
这篇综述论文回顾了38项关于安全LLM代理的研究，强调了关键挑战，如规范翻译瓶颈、运行时监控等执行方法的不完全安全保障，以及阻碍安全任务完成的验证者税。
TLA+是一个模型检查工具，它通过探索所有状态交错来查找分布式系统中的缺陷；通过形式化验证，它帮助在Depot Registry的垃圾回收器中识别了一个遗漏的缺陷，从而提升了安全性。
Specula是一个代理系统，能够自动从代码推导TLA+规范，运行模型检查以发现并发错误，并通过集成测试复现这些错误。它在48个开源分布式和并发系统中发现了249个错误，展示了形式化验证的显著扩展。
Kani是一个开源的Rust模型检查器，它利用对MIR的有界模型检查来验证安全属性和功能正确性，并配备一种用于无界验证的规范语言。该论文报告了在工业Rust项目上的案例研究，其中Kani发现了六个先前未知的缺陷，并在生产CI中大规模运行。
介绍如何结合TLA+与Claude等LLM编写形式化规约，展示LLM如何在语法上提供帮助，同时专注于正确性。
本文提出了一种新颖框架，通过整合采样、自动机学习和模型检测，为部分可观察马尔可夫决策过程（POMDPs）合成有限状态控制器。该方法为现有形式化合成工具难以解决的阈值安全问题提供了形式化保证。
Specula 团队的研究人员创建了 SysMoBench 基准测试，用于评估大语言模型能否准确建模实际计算系统的 TLA+ 规范，还是仅仅照本宣科地背诵教材内容。该基准测试涵盖四个阶段共 11 个系统，揭示了当前大语言模型在准确建模系统实现与参考论文方面的系统性差距。
TLA+ 语义保证无序更新，但 TLC 模型检查器通过要求有序赋值并添加如 PrintT 等有副作用的运算符来破坏这些保证，导致初学者感到困惑。