Concurrent and distributed systems are pervasive, yet verifying their correctness remains challenging. A core difficulty is heterogeneity: verification techniques developed for one computational model rarely transfer to others. In this talk, I present compositional linearizability, a framework that reconstructs linearizability through a compositional lens. This perspective yields a general theory from which correctness criteria for specific domains can be systematically derived, as demonstrated in work on crash-aware systems and systems with liveness requirements. The framework leads to novel verification techniques that enable modular reasoning about complex concurrent objects, mechanized in the Rocq proof assistant. These results open promising new paths toward trustworthy distributed systems.