该论文针对形式化验证程序中的一个关键盲区：即便程序通过了形式化验证，其正确性仍受限于规范（SPEC）的完整性。若规范本身存在漏洞或不完整，验证结果将失去意义。作者提出了一种名为 Fast（Fuzzing-Assisted Specification Testing）的自动化方法，利用同一代码库中规范、实现和测试套件均由同一业务需求派生出的冗余性和多样性进行交叉验证。核心思想是：如果某个意图在实现和测试用例中有所体现，却未被规范捕获，则强烈暗示规范存在盲点。Fast 首先通过变异测试定位规范缺口，即检查代码变体是否仍然符合原始规范；若符合，则进一步利用测试套件推断该缺口是有意引入还是疏忽所致。针对不同规模的代码库，Fast 可选择枚举式或进化式方式生成代码变体。作者在两个具有形式化验证的开源代码库上应用 Fast，分别确认了 13 个和 21 个规范盲点，证明规范不完整在真实应用中普遍存在。该研究为提升形式化验证的可信度提供了一种辅助手段，适合形式化方法、软件测试和安全研究人员阅读。

以太坊的共识安全依赖于多个独立实现的共识客户端在每个状态转换上保持一致。若实现差异导致分歧，网络可能分叉、最终性停滞，并引发严重攻击。为防止此类共识分歧，以太坊提供了 Python 参考实现（consensus-spec）作为规范，并附带手工制作的标准测试套件（spectests）。然而，作为可执行实现，以太坊规范通过运行时行为隐式定义有效性，缺乏系统性方法来确保所有有效性条件被充分测试。本文提出 SpecTrum 框架，分三个阶段解决该问题。首先，引入 Consensus-SpecTec——以太坊共识算法的机械化规范，将有效性条件显式化为 if 前提。其次，定义前提覆盖率指标，衡量 spectests 中哪些 if 前提被评估为真/假。第三，开发基于规范的测试生成器，提取未被 spectests 评估为假的前提约束，并生成输入以覆盖这些前提。在五个主流以太坊共识客户端上应用 SpecTrum，识别出 27 个跨客户端分歧案例，其中 22 个在未插入机械化前提时无法发现。所有 27 个案例在不同分叉版本上均可复现，且将机械化规范扩展到新分叉所需的工作量与规范差异成正比。该研究提出了一种系统化的共识一致性测试方法，通过机械化规范和前提覆盖率指导差分模糊测试，显著提高了以太坊共识客户端之间的一致性和安全性。适合共识协议开发者、区块链安全研究人员以及关注系统验证的软件工程师阅读。

这篇研究报告探讨了在智能合约（如 Diem 支付网络）中推广形式化验证时，开发人员对“规范（specifications）”角色的不同理解如何影响形式化验证的整体效果。作者指出，初次接触形式化验证的软件开发者，往往对规范在操作层面上的意义持有微妙但不同的解释，这些解释会直接影响他们编写的规范类型，进而导致保证效果碎片化，削弱验证工作的整体效力。论文基于在一个金融敏感的智能合约环境中部署形式化验证系统的实际经验，总结了工业界资深开发者（但对形式化方法尚属新手）中常见的三种观点：1）规范是与最终用户沟通的实现与功能之间的契约；2）规范是类型系统的扩展；3）规范是高层状态机的定义。作者认为，虽然哪种解释更接近规范的真正目的尚无定论，但一个重要区分被忽略了：某些规范是“抽象规范（abstracting specs）”，用于锁定需求或意图，因此越多越好；另一些规范是“证明辅助（proof assistance）”，旨在促进实现与抽象规范之间的精化证明，因此应仅在需要时编写；还有一些规范是“指称规范（denotational specs）”，从形式化方法角度看并不增加额外的保证。若缺乏这一区分，形式化验证很容易陷入“规范累积但整体保证并未增加”的陷阱。论文作为一种经验报告，核心贡献在于提出应当明确区分不同类型的规范，并强调抽象规范在保证整体验证有效性中的关键作用。适合正在或计划在智能合约、区块链或高安全性系统中引入形式化验证的团队阅读，尤其对安全工程师和验证工程师具有实践指导意义。

本文提出 NEBULA，一个针对 OAuth 2.0 刷新令牌（refresh token）的、与编程语言无关的精确规格说明，旨在解决 RFC 9700（OAuth 2.0 安全最佳当前实践）中只规定策略而未规定机制的问题。刷新令牌是现代认证系统中极其敏感的凭证：它们长期有效、采用 Bearer 风格，且足以在数天或数周内持续铸造访问令牌。RFC 9700 要求公共客户端签发的刷新令牌必须在每次使用时轮换并具备重放（重用）检测，或采用发送方约束，但该 BCP 并未规定线上格式、存储模式、验证步骤顺序、并发契约，也未定义丢失响应重试或密钥轮换等边界情况的语义。因此，不同实现恰恰会在决定安全结果的关键边界情况上产生分歧。NEBULA 提供了 RFC 9700 刷新令牌模型的精确、语言无关规格，并附带十个符合性参考实现（TypeScript、Python、Go、Rust、Java、PHP、C#、Ruby、Elixir、Dart）。NEBULA 令牌是不透明的——包含 128 位公共选择器和 256 位秘密验证器，两者均由 CSPRNG 输出，不携带声明也不含签名，因此令牌有效性是服务器端状态的属性，而非密码学验证的属性。其一致性方法将行为套件作为数据而非散文发布：38 个场景存储在一个机器可读文件中，每个实现通过一个轻量级语言运行器执行，从而在结构上排除因转录导致的行为漂移。论文描述了该规格，包括一个比较并交换（compare-and-set）的轮换契约，它关闭了并发刷新下重放检测的一个可复现绕过；分析了其安全属性，包括后量子姿态；并报告了跨语言一致性作为多实现安全规格的方法。规格、实现和一致性工件均在 Apache License 2.0 下开源。本文适合身份认证协议设计者、OAuth/OIDC 实现者、安全工程师以及关注安全关键系统形式化与多语言一致性保障的研究人员阅读。

该论文识别了AI安全领域中一个关键的缺失环节：规范基础设施（Specification Infrastructure）。尽管可解释性、形式化方法、安全工程、评估方法和强化学习安全等领域各自产出了大量工作，但这些成果无法组合成可部署的监督方案。每个部署自主智能体系统的团队都不得不自行构建审计模式、策略方言、监控栈和升级路径，大部分是在重复发明已有模式。作者诊断这是一个协调缺口而非研究缺口，并提出了一个二维分类法：五个技术层（可读性、规范、调解、评估、升级）与六个关注点（对齐、鲁棒性、对抗防御、安全、治理、问责）交叉，将现有工作填充到5x6矩阵中。第2层（规范）是人类将意图转化为机器可验证制品的层面，是所有其他层依赖的连接组织，但它缺乏成熟工程学科的四个标志：共享词汇、设计原则、可组合性标准和治理实践。作者提出了第2层的六项设计原则（可激发性、可组合性、对抗感知、可追溯性、可治理性等），并通过工作示例和参考架构使其具体化，该架构将规范转化为运行时执行、评估和升级。现有系统如Cedar、Constitutional AI和Open Policy Agent各自只处理了第2层的一个片段，而矩阵的处理也不完整；将它们视为共享层中的片段使得组合变得可行。作为证据，作者介绍了CARMA，一个用于自主ETL智能体的第2层原型，其中单一规范驱动执行、评估和升级，每个决策都可追溯至版本化的规范。该论文命名了AI监督缺失的内容，并为独立团队提供了构建可组合缺失部分的原则。