Here is a result along the lines you are requesting, which
I find beautifully paradoxical.
Theorem. Every model of ZFC has an element that is a
model of ZFC. That is, every $M\models ZFC$ has an element
$m$, which $M$ thinks is a structure in the language of set
theory, a set $m$ and a binary relation $e$ on $m$, such
that if we consider externally the set of objects $\bar
m=\{\ a\ |\ M\models a\in m\ \}$ with the relation $a\mathrel{\bar e}
b\leftrightarrow M\models a\mathrel{e} b$, then $\langle
\bar m,\bar e\rangle\models ZFC$.
Many logicians instinctively object to the theorem, on the
grounds of the Incompleteness theorem, since we know that
$M$ might model $ZFC+\neg\text{Con}(ZFC)$. And it is true
that this kind of $M$ can have no model that $M$ thinks is
a ZFC model. The paradox is resolved, however, by the kind
of issues mentioned in your question and the other answers,
that the theorem does not claim that $M$ agrees that $m$ is
a model of the ZFC of $M$, but only that it externally is a
model of the (actual) ZFC. After all, when $M$ is
nonstandard, it may be that $M$ does not agree that $m$
satisfies ZFC, even though $m$ actually is a model of ZFC,
since $M$ may have many non-standard axioms that it insists
upon.
Proof of theorem. Suppose that $M$ is a model of ZFC. Thus,
in particular, ZFC is consistent. If it happens that $M$ is
$\omega$-standard, meaning that it has only the standard
natural numbers, then $M$ has all the same proofs and
axioms in ZFC that we do in the meta-theory, and so $M$
agrees that ZFC is consistent. In this case, by the
Completeness theorem applied in $M$, it follows that there
is a model $m$ which $M$ thinks satisfies ZFC, and so it
really does.
The remaining case occurs when $M$ is not
$\omega$-standard. In this case, let $M$ enumerate the
axioms of what it thinks of as ZFC in the order of their Goedel numbers. An initial segment of
this ordering consists of the standard axioms of ZFC. Every
finite collection of those axioms is true in some
$(V_\alpha)^M$ by an instance of the Reflection theorem.
Thus, since $M$ cannot identify the standard cut of its
natural numbers, it follows (by overspill) that there is
some nonstandard initial segment of this enumeration that
$M$ thinks is true in some $m=(V_\alpha)^M$. Since this
initial segment includes all actual instances of the ZFC
axioms, it follows that $m$ really is a model of ZFC, even
if $M$ does not agree, since it may think that some
nonstandard axioms might fail in $M$. $\Box$
I first learned of this theorem from Brice Halimi, who was visiting in New York in 2011, and who subsequently published his argument in:
Halimi, Brice, Models as universes, Notre Dame J. Formal Logic 58, No. 1, 47-78 (2017). ZBL06686417.
Note that in the case that $M$ is $\omega$-nonstandard, then we actually get that a rank initial segment $(V_\alpha)^M$ is a model of ZFC. This is a very nice transitive set from $M$'s perspective.
There are other paradoxical situations that occur with countable computably saturated models of ZFC. First, every such M contains rank initial segment $(V_\alpha)^M$, such that externally, $M$ is isomorphic to $(V_\alpha)^M$. Second, every such $M$ contains an element $m$ which $M$ thinks is an $\omega$-nonstandard model of a fragment of set theory, but externally, we can see that $M\cong m$. Switching perspectives, every such $M$ can be placed into another model $N$, to which it is isomorphic, but which thinks $M$ is nonstandard.
$\def\zfc{\mathrm{ZFC}}\def\pr{\operatorname{Prov}\nolimits}$The statement
$\zfc\vdash\pr_\zfc(\ulcorner\varphi\urcorner)$ implies $\zfc\vdash\varphi$ for every sentence $\varphi$ in the language of $\zfc$
is equivalent to the statement that $\zfc$ is either inconsistent or $\Sigma^0_1$-sound: the latter means that every $\Sigma^0_1$-sentence provable in $\zfc$ is true in standard integers. One direction is obvious as $\pr_\zfc(\ulcorner\varphi\urcorner)$ is a $\Sigma^0_1$-sentence, and its truth in $\mathbb N$ says exactly that $\varphi$ is provable in $\zfc$. The converse follows from the Friedman–Goldfarb–Harrington principle: if $T$ is a recursively axiomatized theory containing Robinson’s arithmetic and $\sigma$ a $\Sigma^0_1$-sentence, there exists a sentence $\varphi$ (that can also be taken $\Sigma^0_1$) such that
$$I\Delta_0+\mathit{EXP}\vdash\pr_T(\ulcorner\varphi\urcorner)\leftrightarrow(\sigma\lor\pr_T(\ulcorner0=1\urcorner)).$$
$\Sigma^0_1$-soundness is stronger than consistency, but weaker than $\omega$-consistency. If you are wondering about foundational issues, it is best to consider it as a separate assumption on its own.
Best Answer
It seems that the Feferman-style description of PA will exhibit your requirements.
Specifically, consider the theory $P$ defined as follows. Begin to enumerate the usual PA axioms, but include the next axiom in $P$ only if doing so keeps $P$ consistent. Never add an axiom to $P$ that would make it inconsistent.
Since PA proves of every finite subset of PA that it is consistent, it follows that PA proves of any particular axiom of PA, that it is in $P$. In this sense, this theory $P$ is the same as PA, just described in a different way.
But because of how it is described, it follows that PA proves $\text{Con}(P)$. We never include an axiom in $P$ that would enable it to prove a contradiction.
Therefore, there is no model $M\models PA+\neg\text{Con}(P)$, and so the theory vacuously has your desired property.
Of course, notice that all instances of your requested property must be vacuous like this, because if the proof of a contradiction inside $M$ were somehow forced to be standard, then it would be actual proof of a contradiction, and so $M$ couldn't exist in the first place, if it is a model of this theory. So it seems to me that the only way to get your situation is in the vacuous way that the Feferman theory achieves it.