Granite is a paper on modular leakage-contract proofs for RTL CPUs, with speculation and interrupts, because side channels were too easy.