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