${}$Hi Ioanna,
**I.**
The answer probably depends on how we define core model. At the level of "there are no Woodin cardinals in any inner model", we can finally show that core models exist, provably in $\mathsf{ZFC}$. The result was known before, of course, but we needed extra assumptions (such as: There is a measurable cardinal $\kappa$) that allowed us to build the model, but only locally (say, in $V_\kappa$). That $\mathsf{ZFC}$ suffices has recently been established by Jensen and Steel, in [*$K$ without the measurable*][1].
This paper also contains an axiomatization of what we mean by a core model (see their Theorem 1.1).
Past one Woodin cardinal, the theory turns complicated for a variety of reasons, the first of which being that iterability is no longer an absolute notion, so additional assumptions on the universe of sets are needed to establish the appropriate results. The idea is simple, but making it rigorous takes work: We can relativize the construction of $K$ to $K_x$ where, instead of considering premice, we look at $x$-premice, that are just like premice but have $x$ as an additional object "added at the bottom". If $x$ is itself a mouse, what we are doing is building mice that extend $x$, but now we only look at iterations that do not require us going back to the extenders of $x$. This way, we can then build appropriate versions of the core model for any finite number of Woodin cardinals, inductively (we start with $x$ having one Woodin cardinal, and build $K$ over $x$, establish somehow that weak covering is violated so the construction actually reaches a Woodin cardinal, so now we have models with two Woodin cardinals, we can use these models $y$ to build $K$ on top, etc.
Making this precise requires that we be able to "patch" together local structures into global ones, which is typically why we need additional assumptions (such as, $V$ is closed under sharps). The precise nature of these assumptions obviously ends up depending on the setting we work with, but we can axiomatize the whole process. This leads to the core model induction which, finally, we can truly describe as an induction, The specific requirement on $V$ then becomes closure under appropriate "mice operators". An excellent description of this approach, and how far it can get, can be seen in the Schindler-Steel monograph [**The core model induction**][2].
As explained in the book, how far the induction can reach (that is, how strong can we obtain a core model) is intimately tied up with how much determinacy we can prove (and so, measuring the strength of the core models becomes a problem of the strength of determinacy assumptions). This is because to obtain closure under the appropriate operators requires that we prove different instances of "mice capturing", for which determinacy appears essential. Nowadays, we understand that the relevant descriptive set theory and inner model theory are so intimately related, that we talk of [*Descriptive inner model theory*][3].
We can reach far beyond what is described in the Schindler-Steel book, and the theory keeps advancing rapidly, so a precise statement of how far we are at is hard to locate. The strongest results are due to Sargsyan, and the strongest *written* accounts are due to him. See *On the strength of $\mathsf{PFA}$. I* and the page on *hod mice* on his [website][4].
Part of what Sargsyan did was to identify what seems to be the right hierarchy of mice within models of determinacy. From earlier work of Woodin we knew that the relevant $\mathsf{ZFC}$ models to study where the $\mathsf{HOD}$ of the models of determinacy. The appropriate hierarchy of *hybrid* mice we now call *hod mice*. Their "hybrid" nature
means that they are not pure mice, but add fragments of the relevant iteration strategies to them. Their strength is then measured via the *Solovay sequence* of the determinacy models we consider. In turn, we use these mice to prove determinacy of stronger models, so the process is truly inductive. Here, the Solovay sequence is the sequence of "local" $\theta$ ordinals: $\theta_0$ is the smallest non-zero ordinal not the surjective image of $\mathbb R$ via an ordinal definable map. We can then define $\theta_1$ as the smallest non-zero ordinal not the surjective image of $\mathbb R$ via maps that are ordinal definable in $A$, where $A$ is any set of reals of Wadge degree $\theta_0$, etc. The hierarchy stops once we reach (true) $\Theta$, the first non-zero ordinal not the surjective image of $\mathbb R$.
The expectation Sargsyan has is that the Solovay hierarchy should at least reach as far as the large cardinal hierarchy. The core models we build this way would have strength measured in terms of the Solovay sequence, and to identify their strength in traditional large cardinal terms would then require a further translation. This is described in some detail in the specific case of his results on the strength of failures of square, see his $\mathsf{PFA}$ paper. As you see there, the final translation (in this case, from "there is an inner model $M$ containing $\mathbb R$ and satisfying "$\mathsf{AD}_{\mathbb R}+\Theta$ is regular" to something past "there is an inner model of $\mathsf{ZFC}$ where there is a proper class of Woodin cardinals and a proper class of strong cardinals") requires a non-trivial amount of work. It usually builds on results of Neeman (on models with a Woodin limit of Woodin cardinals) and Jensen-Schimmerling-Schindler-Steel on [*Stacking mice*][5].
From the above, you probably see that we can currently produce core models essentially in the neighborhood of "There is a Woodin limit of Woodin cardinals". There are natural benchmarks to go from here, say: Models with a measurable Woodin cardinal, or with a subcompact cardinal. This is still significantly below supercompact cardinals, and there are many technical obstacles to overcome before reaching that far.
**II.**
Independently of the line of developments outlined above, Woodin has a program that attempts to identify what should be the ultimate core model, for all large cardinal assumptions. It is this programs and his current results that are described on his papers on [*Ultimate $L$*][6] and what he calls *suitable extender models*. Woodin's high level program has two parts: First, we identify the coarse features of appropriate models of strong large cardinals, in particular, we identify what their extender sequences should look like, and what the appropriate comparison process and iterability assumptions should be. (This is akin to the isolation of Martin-Steel models for Woodin cardinals, that predated the development of their fine-structure by Mitchell-Steel). This part has had reasonable success. Of course, we do not have proofs yet of the appropriate iterability assumptions, but have instead identified what seem to be the relevant conjectures to pursue in this area.
The success of the second part seems to be still far away (even assuming the truth of the relevant conjectures). Woodin has started working on the fine structure of suitable extender models, but I do not know the current state of his results. (You may want to ask him for a draft of his paper.)
[1]: http://math.berkeley.edu/~steel/papers/knombljune2013.pdf
[2]: http://wwwmath.uni-muenster.de/logik/Personen/rds/core_model_induction.pdf
[3]: http://math.rutgers.edu/~gs481/bsl.pdf
[4]: http://math.rutgers.edu/~gs481/papers.html
[5]: http://wwwmath.uni-muenster.de/logik/Personen/rds/stacking_mice.pdf
[6]: http://mathoverflow.net/a/46920/6085