标签
John Regehr 描述了使用 tis-interpreter 在 SQLite 中搜索未定义行为，发现了其他工具遗漏的错误，如悬空指针使用和未初始化读取。
一场关于形式化方法的演讲，以“做事器”三步流程为例，说明如何在尚不存在的系统中寻找 bug。开场因硬件故障延迟了 8 分钟。
本文提出了两种可靠的编码（MIP和SMT），用于在STL-GO表达的时空与拓扑约束下进行多智能体路径规划，并在多无人机搜索与救援基准上进行了评估。
Hillel Wayne 分析了阻碍形式化方法在软件工程中广泛采用的历史和实践障碍，区分了在代码和设计领域中的形式化规范与验证。
一位研究者描述了一个项目，旨在以数学形式化AI生成声明的真实性、合理性和可信度，并寻求关于形式化方法、逻辑和概率论的意见，以构建一个“信任引擎”。
Antithesis发布了一篇博客文章，详细介绍了在多个开源Raft共识实现（包括HashiCorp Raft和OpenRaft）中发现的Bug，强调了测试分布式系统的困难以及对更好工具的需求。
本文介绍了生成式编译，一种在AI生成代码过程中获取部分程序编译器反馈的方法，利用“sealor”变换使得标准编译器能够诊断不完整的代码。在Rust编码任务上的评估表明，该方法通过及早捕获错误，减少了无法编译的输出并提高了功能正确性。
作者分享了自己构建原型以验证AI生成的财务声明的经验，重点关注系统与工程挑战，如证据对账和确定性验证，并邀请志同道合的工程师进行交流。
Theoria 是一种验证架构，将 AI 解决方案重写为可审计的状态转换，在 HLE 问题上实现了高精度，并能检测隐藏前提、虚假引用等细微错误。
一种基于合约的组合式防护方法，无需集中式运行时控制即可确保多智能体强化学习中的全局安全性，利用局部LTL义务和多臂老虎机优化团队奖励。
Jane Street，此前对形式化方法持怀疑态度，现宣布转变观点，计划组建专注于形式化方法的团队。这一转变源于代理编程（agentic coding）的出现，它通过降低验证成本并增加对可靠代码的需求，改变了成本/效益计算。
Jane Street，此前对形式化方法持怀疑态度，现在正在组建团队使用它们，这得益于人工智能和智能体式编码，它们降低了成本并增加了软件验证的收益。
本文形式化了现代AI后训练流程中训练内核与推理内核之间的数值差异，提出了一种内核合约规范以及一系列Lipschitz风格的界限，以减轻离策略偏差、切片级回归和可重复性问题。
一篇新论文，调查了形式化方法从业者对AI安全应用的重要性与可行性，并附带一项对软件验证应更具雄心的广泛呼吁。
Strabo 是一项研究成果，将 Google 的通用商务协议（UCP）建模为声明式 Langshaw 协议，并使用 Peach 编程模型实现智能体，展示了形式化规范智能体与 Google UCP 智能体之间在智能体 AI 电商交互场景下的互操作性。
本文提出了一种基于树结构的形式化框架，用于对多智能体人机交互中的互补性进行建模，并证明了在自然条件下，互补性在回归任务中可以实现，但在分类任务中受到阻碍——这些条件涉及局部聚合规则和损失函数。
这篇1996年的论文探讨了尽管缺乏形式化证明，软件可靠性却日益提高的原因，讨论了非正式方法和工程实践。
Hillel Wayne 为其著作《Logic for Programmers》发布补充章节，涵盖并发进程、一阶逻辑、Liskov 历史规则及排序等主题。