传统安全审计工具主要通过分析代码库中的局部代码模式来识别漏洞，但对于由自然语言规范约束的系统（如协议栈、共识实现、加密库），其安全属性（不变性、正确性条件）定义在规范中而非代码中。当漏洞源于规范要求而非编码错误时，代码级审计工具缺乏检测所需的表示词汇，且其误报难以系统诊断。本文提出 SPECA，一个基于规范锚定的安全审计框架。该框架首先从自然语言规范中提取显式、类型化的安全属性，然后针对每个属性，通过结构化证明推理的方式审计相应实现。SPECA 提供了三种超越代码驱动审计的能力：1）依赖于规范的检测，即能发现因规范违反而非代码错误导致的漏洞；2）在共享属性词汇下实现跨实现的受控比较；3）误报可分解为可解释的、可按管道阶段追踪的根源原因。实验在 Sherlock Ethereum Fusaka 审计竞赛（366 份提交，10 个实现）中，SPECA 恢复了所有 15 个范围内漏洞，并独立发现了 4 个已被开发者修复确认的 bug。在 RepoAudit C/C++ 基准测试（15 个项目）上，SPECA 达到了最佳公开精确率（88.9%），同时在已有基础真相之外发现了 12 个候选漏洞，其中两个已由上游维护者确认。多模型分析表明，更强的能力模型在属性范围内审计更忠实，从而将检测瓶颈从模型推理转向属性生成质量。所有误报可归因于三种反复出现的根源：信任边界误解、代码阅读错误和规范误解，每种都提供了可操作的改进目标。该研究适合安全审计工具开发者、协议实现者及依赖规范安全性的团队阅读。

本文提出 GoAT-X 框架，旨在解决跨链桥合约安全审计中的语义复杂性问题。跨链桥作为多链生态的关键基础设施，因实现缺陷已造成超过28亿美元损失。现有防御手段如字节码级静态分析难以处理跨链交互的语义复杂度，而基于大语言模型（LLM）的方法虽能理解源代码，但在复杂多合约依赖上容易出现幻觉推理。GoAT-X 将审计过程建模为“审计思维图”（Graph of Auditing Thoughts），模仿人类专家分解、推理和验证安全逻辑的方式。通过将LLM推理锚定在静态提取的数据流上，并将抽象安全属性显式链接到具体代码实现，该框架将语义约束在良定义的结构和状态边界内。在此受限空间中，GoAT-X 将跨链逻辑中的缺失约束和对抗绕过路径作为首要漏洞目标，动态探索推理路径以识别可被利用的语义鸿沟。在涵盖所有已知跨链代币交易攻击的综合基准测试中，GoAT-X 在细粒度审计点上达到92%的召回率，对存在漏洞的项目覆盖率达95%，并在实际场景中识别出117个经确认的风险，且运营成本较低，为可扩展的、逻辑驱动的跨链安全审计建立了新标准。