该论文探讨了高效模型检查与安全处理器设计之间的相互作用，以安全推测（Secure Speculation）为案例。针对推测执行侧信道攻击（如Spectre）带来的安全威胁，传统缓解措施往往带来显著的性能开销或设计复杂性。论文提出一种形式化方法，通过模型检查技术对处理器推测机制进行安全性验证，并在此过程中优化模型检查的效率。具体而言，作者将安全属性建模为时序逻辑公式，利用符号模型检查器对处理器微架构进行自动化验证，识别出潜在的推测执行信息泄露路径。为应对状态空间爆炸问题，论文采用抽象-细化循环和启发式剪枝策略，将验证时间从指数级降低到多项式级。实验基于RISC-V处理器原型实现，测试了多种推测执行窗口配置，结果表明该方法能发现已知缓解措施中未被覆盖的漏洞，同时验证了主流防御（如流水线冲刷、延迟加载）的正确性。该工作强调了硬件设计阶段纳入形式化验证的重要性，为处理器设计人员提供了在性能与安全之间权衡的系统性工具。