该论文提出了一种针对基于LLM的编码代理（coding agent）在发现跨站脚本（XSS）漏洞时的验证框架RECEIPT。由于LLM代理在探索应用时可能产生不可信的报告（例如虚假声称找到漏洞），作者首先刻画了三种奖励黑客（reward-hacking）行为：代理可能通过执行攻击脚本但并未实际触发漏洞、可能误报非漏洞、或利用验证环境的不一致来骗取奖励。针对这些问题，论文定义了理想验证器应满足的三个要求：确定性、可重现性、防篡改。RECEIPT通过四个核心机制实现可靠验证：环境隔离（每个验证任务使用独立浏览器实例）、PoC约束（要求提供确定性的攻击载荷）、角色分离（区分攻击者和受害者的浏览器上下文）、以及结论绑定（将脚本执行结果与漏洞确认强关联）。每个确认结果都证明两点：脚本在真实浏览器中运行，且攻击载荷以攻击者角色植入并在受害者角色浏览器中执行。这样的受限回放过程使得验证确定性和可重现性。实验在95个真实世界Web应用目标上进行，每个应用预算20美元内，RECEIPT发现了24个未知XSS漏洞，其中12个已得到维护者确认，并在已知漏洞恢复目标中以36%的召回率恢复了标记的CVE。与同一代理使用自我判断以及黑盒扫描器相比，RECEIPT确认了更多真实利用且无假阳性。

该论文提出并形式化了一种基于图表解析（chart parsing）的PEG（Parsing Expression Grammar）解析器解释器鲁棒性验证方法。作者定义了一个状态机，该状态机在一个脚手架（scaffold）数据结构上操作，脚手架维护一个状态矩阵，每个条目对应一对位置和非终结符。解析器解释器以惰性方式填充这些条目，记录解析是否成功、失败或陷入循环，从而支持可能左递归的PEG文法并添加循环检测。论文定义了状态上的不变量，并定义了保持这些不变量的解析步进函数。从解析的最终状态可提取独立检查的解析证明表示。作者对一系列演进的PEG形式化定义并证明了图表解析器，并在这些形式化之间进行了大量的证明重用。通过PVS证明系统中的交互与自动化混合，使得证明对特定类型的规范和设计变更具有鲁棒性。论文还讨论了如何主动构建针对解析这类重要问题的鲁棒证明。该工作为解析解释器的正确性提供了形式化保证，对安全领域中的输入验证、反混淆等场景具有理论价值。

硬件安全验证是一个多阶段流程，工程师需要处理复杂的设计分析、威胁考量与验证策略，但现有验证环境缺乏结构化的安全指导支持。虽然对话式AI可以提供按需帮助，但直接使用通用型聊天机器人（如ChatGPT、Gemini）存在风险，因为它们容易产生幻觉且依赖静态过时知识。为此，本文提出VeriChat——一个面向硬件安全验证的领域专用对话助手，旨在增强而非取代现有验证工作流。VeriChat采用检索增强的多智能体架构，包含三个专门智能体，它们协作降低幻觉，提升响应的透明性与可靠性。除问答功能外，VeriChat还集成了开源EDA工具（Icarus Verilog、Yosys、SymbiYosys），能直接对用户提供的RTL设计执行语法检查、综合分析、仿真与形式化验证。综合评估显示，VeriChat的忠实度得分为87.73%，显著优于主流商用模型。通过一个AES S-Box IP上的硬件木马检测案例，VeriChat在多次对话中自主完成木马识别、仿真与形式化证明，成功发现隐蔽的密钥泄露漏洞。

本文针对未来可能达成的国际人工智能协议，提出了一种用于AI数据中心验证的基础架构方法。核心目标是确保所有进出AI集群的数据均被加密承诺，使得秘密窃取未公开工作负载的结果变得不可行。方法是在集群与外部世界之间的所有信息承载线路上部署网络分接头（passive optical fibre splitters），计算所有数据的哈希值。审计员可以事后挑战哈希对应的原像数据，并将其发送至隐私保护的验证设施进行合规检查。为了解决事后哈希验证无法处理的隐蔽信道问题，论文设计了一种“安全网关设备”（Secure Gateway Device），其架构消除了对验证者和被验证者双方均信任的处理器的依赖，利用被动光纤分路器和抛币协议（coin-flip protocols）生成随机数。该设备负责消除模拟侧信道、时序侧信道以及网络协议头中的隐写术等隐蔽信道。论文评估了开发成本，预计演示设备的开发成本相当于一个小型工程师团队数月的工作量，物料清单相对较小。该研究为AI数据中心的透明度和可信验证提供了新思路，适合关注AI治理、安全基础设施和隐私保护的研究者和工程师阅读。

本文提出了一种面向自主智能体（agent）商业交易的结算完整性协议 RAILS（Real-Time Agent Integrity & Ledger Settlement）。当前，智能体可以自主谈判、购买、部署代码和转账，但缺乏一个中立机制来确定它们是否履行了委托义务、在未履行时谁应负责、以及后续的结算动作是什么。作者将这一问题定义为“智能体结算问题”（agentic clearing problem）。现有工具协议（如 MCP）、智能体间通信（A2A）、支付轨道（x402）、授权协议（AP2、Visa、Mastercard）以及结算风险标准均假设存在此类判定机制，但实际并未提供。结算（clearing）是缺失的原语：支付不是结算，授权不是结算，LLM 作为裁判的评估不是结算，结算风险托管也不是结算——它消耗结算决策。RAILS 作为智能体商业的完整性与结算层，包含三个组件：每个输出的可靠性评分、发布的可靠性记录、以及消耗这些信息的结算函数。其核心清算协议由七个原语构成：义务对象（Obligation Object）、证据信封（Evidence Envelope）、验证网格（Verification Mesh）、结算决策（Clearing Decision）、结算指令（Settlement Instruction）、结算护照（Clearing Passport）和最终性规则（Finality Rules）。这些原语受一个基于可接纳性分级验证的形式模型约束，最终产生一个可靠性属性：任何具有财务重要性的结算必须由满足义务可接纳性下限的证据支持。该属性在规范上是可伪证（falsifiable）的。作者声称，此前未发现任何智能体商业验证机制声明过此类属性。最接近的方法仅输出通过/未通过、交付保证、单一评分或均衡状态。本文详细规定了该清算协议。适合对 autonomous commerce、agent integrity、verification 感兴趣的安全架构师和研究者阅读。

本研究探讨社交媒体平台验证政策变化（如Twitter（现X）在2022年后调整的蓝色验证标记政策）如何影响用户对已验证账户的感知和信任。传统上，蓝色验证标记被视为可信机构认证的权威标识，但平台将验证开放给付费订阅者后，验证标记的可靠性受到质疑。研究人员通过在线实验，招募参与者对不同类型账户（如名人、记者、普通用户）在政策变化前后的可信度、权威性和真实性进行评分。实验还考察了验证标记与用户关注状态、账户类型之间的交互效应。结果表明，政策变化显著降低了用户对已验证账户的整体信任，尤其是对低知名度账户；用户更倾向于依赖其他信号（如粉丝数、内容质量）而非验证标记。研究还发现，用户对验证标准的理解存在混乱，许多人误以为验证仍代表官方认证。该研究对社交媒体平台的安全设计、用户隐私保护及虚假信息对抗具有重要启示。

该论文研究了AI推理验证中的关键问题：在GPU浮点运算的非确定性环境下，如何实现比特精确的推理结果验证，而无需牺牲性能。现有方法依赖近似匹配，这可能被隐蔽对手利用未验证的自由度进行攻击，如通过隐写术、未报告的软件修改或隐藏的批处理元素执行恶意计算。作者分析了现代推理引擎（如vLLM、Hugging Face Transformers）在未设置确定性标志的情况下，通过提供正确的重计算所需信息且后端不调用原子函数，实际输出具有确定性但非不变性。他们提出一种仅通过软件仿真的方法，在多种NVIDIA GPU变体上实现了大语言模型推理的逐位精确重计算，无需相同硬件。实验表明，累积舍入误差可作为推理所用软件和硬件设置的审计签名，而非验证性的约束。该方法为AI治理中的隐蔽恶意行为检测提供了新途径，尤其适用于验证模型推理的完整性和一致性。

内存安全错误是低级软件中零日漏洞的持续根源，尤其在嵌入式系统中，硬件保护有限且动态分析难以有效应用。内存安全验证可以通过证明不存在此类错误或暴露违规来提供更强保证，但当前验证工作流主要依赖手动操作，需要大量专业知识，限制了实际采用。本文提出 AutoSOUP，一种通过安全导向单元证明实现组件级内存安全验证自动化的系统。作者形式化定义了单元证明，将其编码为包含验证选择（作用域、循环边界和环境模型）的工件，用于验证安全属性，并引入三种自动推导技术。为克服现有自动化方法的局限，进一步提出 LLM-As-Function-Call 混合架构，结合确定性程序合成与大语言模型自动执行这些技术，生成可解释的单元证明。通过评估 AutoSOUP 自动化内存安全验证的能力、在已验证组件中暴露漏洞的效果，并刻画了所得证明的假设和保证。实验表明，AutoSOUP 能有效降低验证专业门槛，提升验证效率，尤其适用于资源受限的嵌入式安全场景。