本文提出 Granite，一种用于对 RTL 级处理器设计进行模块化形式验证的方法论，旨在同时验证功能正确性和非泄漏性（nonleakage）。基于 ISA 泄漏契约，Granite 证明了带有推测执行、精确中断和 I/O 的流水线 RISC 设计的逐周期时序行为完全由契约中可观测的接口决定。对于遵循密码学常数时间纪律的程序（即不将秘密值影响任何可观测量的程序），该结果能够排除经已知或未知时序侧信道的信息泄漏。Granite 的规格仅约束功能正确性和信息流依赖，不规定指令的周期数、中断处理位置或子模块（如乘法器、内存）的具体延迟。其核心技术是'基于确定性的泄漏感知精化'，将正确性和机密性统一表示为与一族周期级确定性规格机器的轨迹等价。对于与秘密无关的非确定性，Granite 通过存在性参数化规格，使用仅作用于公开数据的不可信确定性函数来处理。子模块分别被证明满足其自身的泄漏感知规格，而这些证明组合成整体设计保证，因此适用于广泛的实现空间。作者声称这是首项在指令集级泄漏契约与微架构级逐周期执行（带线级观测）之间建立模块化和基础连接的工作。此外，该证明与一个认证静态分析相结合，可识别密码学常数时间代码，进而推导出关于硬件-软件密码实现的逐周期机密性的单一 Rocq 定理，从而从可信计算基（TCB）中消除了包括 ISA 契约在内的所有中间规格。