Modular Verification of RTL Processors Against ISA Contracts (MIT, Google, UW)

Researchers from MIT, Google, and University of Washington published a technical paper titled “Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts.”

Abstract Excerpt: “Granite is a methodology for modular verification of both functional correctness and nonleakage of RTL processors against ISA contracts. We prove that the cycle-by-cycle timing of a pipelined RISC design–with speculation, precise interrupts, and I/O–is determined solely by observables specified in an ISA leakage contract. For programs that keep observables independent of secrets (i.e., following the cryptographic-constant-time discipline), this result rules out information leakage through known and unknown timing side channels.”

Find the technical paper here. July 2026.

Lau, Stella, Andres Erbsen, and Adam Chlipala. “Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts.” arXiv, July 2026. doi.org/10.48550/arXiv.2607.27480.