Compositionality is essential for managing complexity in verification of concurrent programs, especially when proof certificates are needed. An effective verification scheme is to divide programs into abstraction layers and verify by composing refinements between layers. However, vanilla verified layers come with \emph{global states} which severely limit their extensibility. This problem may be solved by dividing a layer into objects with \emph{encapsulated local states}. Although the idea has been successfully realized in the sequential setting, it remains unclear if it also works in a concurrent setting where function calls across layers are no longer atomic steps and foundational proofs are needed.

We propose an approach to foundational and compositional verification of concurrent objects organized into multiple layers. The central idea is to represent concurrent objects as \emph{open} labeled transition systems with \emph{encapsulated threads} and to adopt \emph{trace refinements} as a uniform notion of functional correctness which supports both \emph{vertical composition} (layered refinement) and \emph{horizontal composition} (extension of layer interfaces). Due to the operational nature of transition systems, it is straightforward to adopt traditional simulation techniques to produce foundational proof certificates. We implement this framework in the Rocq theorem prover and demonstrate its capability in foundational and compositional verification by verifying non-trivial lock-free concurrent data structures.