Consider the claim:
(C) There is a transitive set $S \in V$ such that the structure $(S, \in)$ is an elementary submodel of $(V, \in)$.
Obviously, this claim cannot be a theoreom of ZFC, by Godel's 2nd Incompleteness Theorem. But does (C) follow from ZFC+CON(ZFC)? Or are large cardinals needed to prove (C)? More generally (and vaguely), what is the weakest assumption needed to prove (C)?
A cardinal $\delta$ is correct if the theory $V_\delta\prec V$ holds, that is, if $V_\delta$ is an elementary substructure of $V$. This theory is expressible as a scheme in first order logic in the language of set theory augmented by a constant symbol for $\delta$ as the following scheme of statements:
$$\forall \vec a\in V_\delta\ \ (\ \varphi(\vec a)\quad\iff\quad V_\delta\models\varphi[\vec a]\ \ ).$$
Note that any set $\langle S,{\in}\rangle$ such as you desire must have the form $S=V_\delta$ for some $\delta$, since it will the union of the $V_\alpha$ for $\alpha<\delta$ because by elementarity it will be right about these $V_\alpha$, and so this is your main case.
The property of being correct is not expressible as a single assertion in ZFC, unless inconsistent, since otherwise there could be no least reflecting cardinal, since if $\delta$ is the least reflecting cardinal and this were expressible, then $V$ would have a reflecting cardinal, but $V_\delta$ would not. A similar argument applies directly to the existence of a set $\langle S,{\in}\rangle$ as in your question, showing that $S\prec V$ is not expressible as a single assertion in the language of set theory.
Meanwhile, as a scheme, the existence of a reflecting cardinal is equiconsistent with ZFC, and in particular it does not imply Con(ZFC). To see this, observe that if there is a model of ZFC, then by the reflection theorem, we may easily produce models of any given finite subset of the theory. So by compactness the theory $V_\delta\prec V$ is also consistent.
One may easily extend this theory to have a unbounded closed proper class $C$ of cardinals $\delta$ for which $V_\delta\prec V$, a theory known as the Feferman theory, and this also is equiconsistent with ZFC, with no increase of consistency strength, by the same argument. Feferman propsed this theory as a natural background set theory in which to undertake category theory, because it provides a robust universe concept (more robust than Grothendieck universes in that the universes all cohere into an elementary chain), but without the large cardinal commitment.
If one adds to the theory $V_\delta\prec V$ that $\delta$ is inaccessible, then $\delta$ is a reflecting cardinal, whose existence is equiconsistent with Ord is Mahlo.
If one desires a purely first-order concept, expressible as a single property in the language of set theory, then one may restrict to a less severe form of elementarity. For example, a cardinal $\delta$ is $\Sigma_2$-correct if $V_\delta\prec_{\Sigma_2} V$, that is, $V_\delta$ is elementary for formulas of complexity $\Sigma_2$, and $\Sigma_2$-reflecting if $\delta$ is also inaccessible. For example, the $\Sigma_2$-reflecting cardinals commonly arise in large cardinal arguments, and this is expressible in the language of set theory. More generally, one has the concept of a $\Gamma$-reflecting cardinal for any class $\Gamma$ of formulas, and if these have bounded complexity, then these also will be expressible.
For many purposes, the $\Sigma_2$-correct cardinals carry much of the useful power of what you want from $V_\delta\prec V$, since one of the equivalent formulations is that $\delta$ is $\Sigma_2$ correct if and only if whenever there is $\theta$ with $V_\theta\models\sigma$ for any assertion $\sigma$, using parameters in $V_\delta$, then there is $\theta\lt\delta$ with $V_\theta\models\sigma$. In other words, any thing that happens in a $V_\theta$ above $\delta$ also happens below $\delta$.
Two comments on this:
First, it's not clear that one can formulate "there exists a transitive set $S\in V$ such that $S\prec V$" in first-order logic, so it's a bit tricky to phrase your question precisely.
More importantly, I claim that no theory $T$ can have the property you desire. Basically, suppose there were such a $T$. Then $T$ must prove "there exists a transitive model of $T$:" by elementarity, if $V\models T$ then $S\models T$. But then $T\models Con(T)$, which contradicts Goedel's theorem.
(One can also prove a weaker version of this without using Goedel: any theory $T$ containing Choice [EDIT: As Francois points out, Choice is unnecessary here] and Foundation cannot have the property you desire. Otherwise, $T$ would prove "there exists a transitive model of $T$." Now using Choice, we can build a sequence $S_1, S_2, . . . $ such that $S_i\models T$ and $S_{i+1}\in S_i$ for all $i$. But this contradicts Foundation.)
