Microarchitectural attacks are side/covert channel attacks which enable leakage/communication as a direct result of hardware optimizations. Secure computation on modern hardware thus requires hardware-software contracts which include in their definition of software-visible state any microarchitectural state that can be exposed via microarchitectural attacks. Defining such contracts has become an active area of research. In this talk, we will present leakage containment models (LCMs)—novel axiomatic hardware-software contracts which support formally reasoning about the security guarantees of programs when they run on particular microarchitectures. Our first contribution is an axiomatic vocabulary for formally defining LCMs, derived from the established axiomatic vocabulary used to formalize processor memory consistency models. Using this vocabulary, we formalize microarchitectural leakage—focusing on leakage through hardware memory systems—so that it can be automatically detected in programs. To illustrate the efficacy of LCMs, we first demonstrate that our leakage definition faithfully captures a sampling of (transient and non-transient) microarchitectural attacks from the literature. Next, we develop a static analysis tool, called Clou, which automatically identifies microarchitectural vulnerabilities in programs given a specific LCM. We use Clou to search for Spectre gadgets in benchmark programs as well as real-world crypto-libraries (OpenSSL and Libsodium), finding new instances of leakage. To promote research on LCMs, we design the Subrosa toolkit for formally defining and automatically evaluating/comparing LCM specifications.