This is the formalization for the paper A Formal Interface for Concurrent Search Structure Templates. Our implementation (in templates/implementations) and the formally verified Concurrent Search Structure Templates (in templates), verified using VST (VST) and flow interfaces (flows), are all included in Artifact.tar.gz. The file templates-artifact.tar.gz is a Docker image that contains a compiled version of Artifact.tar.gz with all dependencies installed. Detailed instructions are provided in the INSTALL.md file below or in the INSTALL.md file inside Artifact.tar.gz PAPER ABSTRACT Concurrent search structure templates simplify reasoning about concurrent data structures by dividing them into synchronization patterns and underlying sequential data structures, which can be designed and verified independently. Past work has used templates to decompose the verification of specific data structures and reuse some of their components, but has not given a general characterization of what makes a concurrency template or whether it can be applied to a given data structure. In this paper, we formally define the interface provided by search structure templates, and show that as long as a sequential data structure component and a concurrency template are proved to implement this interface, they can immediately compose into a verified concurrent data structure with no additional effort. Thus, from any m verified data structure components and n verified concurrency components, we obtain m×n verified data structures. We validate our interface by verifying two data structure instances (linked list and binary search tree) and three concurrency templates (coarse-grained locking, lock coupling, and give-up), which can be freely plugged into a top-level verified data structure whose correctness proof is parameterized by the interface.