Even though set theorists refer to "the core model", it is not a uniquely identified mathematical object.
The first core model was Kurt Gödel's constructible universe L. Ronald Jensen proved the covering lemma for L in the 1970s under the assumption of the non-existence of zero sharp, establishing that L is the "core model below zero sharp".
The work of Solovay isolated another core model L[U], for U an ultrafilter on a measurable cardinal (and its associated "sharp", zero dagger).
Together with Tony Dodd, Jensen constructed the Dodd–Jensen core model ("the core model below a measurable cardinal") and proved the covering lemma for it and a generalized covering lemma for L[U].
An important ingredient of the construction is the comparison lemma that allows giving a wellordering of the relevant mice.
This implies that for every iterable extender model M (called a mouse), there is an elementary embedding M→N and of an initial segment of K into N, and if M is universal, the embedding is of K into M. It is conjectured that if K exists and V is closed under a sharp operator M, then K is Σ11 correct allowing real numbers in K as parameters and M as a predicate.
The core model can also be defined above a particular set of ordinals X: X belongs to K(X), but K(X) satisfies the usual properties of K above X.