WebGPU 是浏览器中面向 Web 应用暴露现代 GPU 能力的低层图形与计算 API，其正确性与安全性直接影响浏览器渲染进程。官方 WebGPU 一致性测试套件（CTS）主要验证“良构用法”是否符合规范，并不以语义边界情况或对抗性输入去压测实现；而通用型模糊测试器又因 WebGPU 依赖复杂图形栈、多进程架构与异步管线而难以有效触达。论文提出 LANTERN——一个规范引导的动态一致性测试框架，其核心思路是“以规范为种子”对 CTS 测试进行定向变异。LANTERN 先从 WebIDL 定义中抽取显式的语法层 API 规则（参数类型、枚举取值、必选/可选项等），再从规范的自然语言文本中恢复语义约束，例如命令提交顺序、资源依赖与对象生命周期等难以从接口签名中得到的规则。随后，被选中的规则驱动基于 AST 定位的文本变换，对 CTS 用例做有目标的最小改动，从而同时生成合法变体与刻意违规的变体；前者用于扩大覆盖，后者用于检验实现是否在非法用法下仍保持内存安全与状态一致。作者将生成的测试在启用 AddressSanitizer 的 Chromium 上大规模执行，最终发现三个可复现缺陷，其中包含一处堆破坏（heap corruption），且均存在于研究进行时的 Chromium 版本中。该工作表明，语法播种加语义感知的一致性测试变异，是一种在 WebGPU 测试阶段发现浏览器实现缺陷的可行路径，也说明现有 CTS 与通用 fuzzer 之间存在明显的覆盖空白，可被规范驱动的定向变异所填补。

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