该论文提出了一种全新的方法，用于形式化规范指令集架构（ISA）的安全保证。传统上，ISA的规范仅限于功能方面，且通常以非形式化的散文形式描述，缺乏对安全保证的精确刻画。作者引入了通用契约（universal contracts）的概念——这是一种软件契约，能够表达任意不可信代码的权限边界。通用契约独立于软件抽象层次，既能为软件推理提供必要的细节，又保留了ISA设计者和CPU实现者的实现自由度。论文的核心贡献包括：（1）提出了一种通用的、可平衡硬件实现与软件客户端需求的形式化安全保证规范方法；（2）开发了Katamaran工具——一个半自动化的分离逻辑验证器，用于Sail语言描述的ISA语义，能够生成机器可检查的证明；（3）通过两个差异显著的ISA实例验证了方法的通用性：自定义能力机ISA（MinimalCaps）和带有物理内存保护（PMP）的简化RISC-V。此外，作者还利用为RISC-V with PMP形式化的安全保证验证了一个femtokernel。实验结果表明，该方法能够支持在存在对抗代码的情况下对安全关键软件进行非形式化和形式化推理，同时确保硬件实现与安全契约的一致性。该工作为建立高置信度的处理器安全基础提供了形式化工具和方法论。