[CPP'26] Towards composable proofs of cache coherence protocols

Towards Composable Proofs of Cache Coherence Protocols (Video, CPP 2026) Martina Camaioni, Yann Herklotz, Tz-Ching Yu, Thomas Bourgeat (EPFL, Switzerland; EPFL, Switzerland; EPFL, Switzerland; EPFL, Switzerland) Abstract: Verifying cache coherence protocols is a notoriously difficult problem. At the intersection between distributed protocol and computer architecture, it has long served as a premier target for formal methods. Current verification approaches hinge on the challenging discovery of large global inductive invariants. This paper introduces an alternative proof strategy that tames the complexity through two main contributions: protocol decomposition and a framework of local invariants. We prove the correctness of the standard MSI protocol compositionally by independently verifying the simpler MI and SI subprotocols and proving MSI behaves as their combination. This decomposition revealed a useful insight: the invariants necessary in these proofs can be established using a small set of simple local invariants: invariants between a single cache and the parent and memory, eliminating complex global reasoning across children caches. We demonstrate how our approach reduces the number of required invariants from several dozens to hundreds in prior work to a small, structured and manageable set, simplifying the proof of correctness. The entire development is formalized in Lean 4. Article: https://doi.org/10.1145/3779031.3779106 Supplementary archive: https://doi.org/10.5281/zenodo.17805558 (Badges: Artifacts Available) ORCID: https://orcid.org/0009-0000-8106-4732, https://orcid.org/0000-0002-2329-1029, https://orcid.org/0009-0000-9856-6835, https://orcid.org/0000-0002-8468-8409 Video Tags: Lean, cache coherency, MSI, formal verification, theorem proving, doi:10.1145/3779031.3779106, doi:10.5281/zenodo.17805558, orcid:0009-0000-8106-4732, orcid:0000-0002-2329-1029, orcid:0009-0000-9856-6835, orcid:0000-0002-8468-8409, Artifacts Available Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ Sponsored by ACM SIGPLAN.