formal-methods

互联网最近发现了 TLA+，这是一种用于验证并发系统的正式规范语言，从而引发了关于其应用和未来影响的讨论。

本文讨论了在 TLA⁺ 中表达可达性属性的可能性，参考了 Leslie Lamport 的工作以及 TLC 模型检查器的局限性。

本文介绍了Verifpal的修订版分析引擎，Verifpal是一个符号协议验证器，详细阐述了其形式化规范、证明以及与其他工具如ProVerif和Tamarin的对比评估。

Geoffrey Irving 强调了 NDIST 关于安全形式化方法的报告，并指出规模化问题已转向硬件和软件制造商之间的市场协调。

本文探讨了对分布式系统中自稳定组合式理论的探索，批判性分析了近期关于元稳定故障的论文，以及依赖保证契约等形式化方法。

介绍了PetriBench，一个利用Petri网评估大语言模型在动态状态空间上推理能力的可扩展基准测试。研究表明，准确率随难度增加而下降，并揭示了不同模型在特定任务上的能力差异。

本文提出了一种针对代理式AI系统的独立性分级审计协议，从主体、基座和证据三个轴向对独立性进行分级，并提供了形式化基础及分析。

本文介绍了ContrAgent，一个基于合约的框架，用于对LLM代理进行符号时间监督，确保在在线和离线模式下以低延迟执行确定性安全检查。

本文讨论了扩展人类对 AI 代理的监督所面临的挑战，并展示了如何使用形式化方法结合 Z3 库来验证代理策略变更是否保持在已批准的权限范围内。

本文提出广义代理迭代（GAI）作为一个形式框架，统一了迭代策略改进和递归自我改进，将代理定义为可修改组件，并根据外部评估和内部改进区分不同案例。

本文介绍了程序综合技术，特别是针对无循环程序的反例引导迭代综合，并提供了使用 Z3 求解器在 Rust 中的实现。

本文讨论了一篇科学论文，该论文正式证明了系统中验证的边界，认为信任决策必须是明确的，并且在超出某个点后需要进行管理。

文章区分了系统设计中的两种抽象类型：模块化抽象，它隐藏内部细节；建模抽象，它将系统简化为基本行为以进行形式化推理。

本文讨论了复杂软件系统中形式化规范的缺失，通过假设情景来强调计算机科学中形式化方法的挑战与重要性。

一篇探讨有限状态模型检查在计算机科学和软件验证中演变角色的文章。

本文探讨编程语言语义及其在内存安全中的关键作用，以教育背景解释操作语义、指称语义和公理语义方法。

PANDA 是一个可扩展的系统，使用零知识证明来验证神经网络的鲁棒性和公平性，无需揭示模型参数，从而能够对具有多项式复杂度的大型网络进行认证。

本文介绍了一种用于神经符号约束求解的最小核心引导修复方法，其中语言模型利用不可满足核心中的证明来纠正翻译错误，从而减少解决方案中的虚构内容。

本文通过统一效果和共效果，形式化了一种时空可组合性的编程范式，并借助Cordis元框架实现了动态组件组合。

介绍“Training Under Challenge”（挑战下训练），这是一个可执行证书框架，利用架构有效的过程构建替代模型，并估计神经网络检查点的经验全局最优性差距，具有理论保证以及基于 ResNet-18 蒸馏和量化去噪的实验。