一句话：提出 Scope，以规范为唯一真值，用 Verus/SMT 自动检测 Arm CCA RMM 规范不一致，发现 35 个新缺陷。
形式验证虽能提供强正确性保证，但其可靠性取决于规范本身的正确性；规范中的细微错误即可使证明失效并引入安全漏洞。本文提出 Scope，一个以规范为唯一真值、不依赖实现的自动化不一致检测系统。Scope 将 Arm CCA 的 Realm Management Monitor（RMM）规范翻译为 Verus 可验证模型，并借助 SMT 求解器，对成功/失败条件、依赖规则和状态转换进行基于规则的一致性检查。在 RMM 规范上，Scope 发现 35 个此前未知缺陷，包括 ABI 语义中的安全关键问题与缺失状态转换，均获 Arm 确认；与基于 LLM 的工具相比，检测精度较 GPT-o1 提升 7 倍，较 LLaMA 3.1、GPT-4o、Claude 3.7 最高提升 40 倍。
Formal verification offers strong guarantees of correctness, robustness, and security. However, these guarantees depend on specification correctness, and even minor flaws can invalidate proofs and introduce critical vulnerabilities. We present Scope, an automated system that identifies specification inconsistencies by combining formal modeling with rule-based consistency checking. Unlike traditional approaches that rely on implementations, Scope treats the specification as the sole ground truth. It translates the specification into a machine-verifiable model using Verus and SMT solvers, then detects inconsistencies in success/failure conditions, dependency rules, and state transitions. We apply Scope to the Realm Management Monitor (RMM) specifications for Arm's Confidential Compute Architecture (CCA), uncovering 35 previously unknown bugs—including security-critical flaws in ABI semantics and missing state transitions—all confirmed by Arm. Compared to modern LLM-based tools, Scope improves inconsistency-detection precision by 7x over GPT-o1 and up to 40× over leading chat models (LLaMA 3.1, GPT-4o, Claude 3.7).