[NEWEST EDIT] This a try to salvage this method, addressing the two objections that was raised by Noah. So I'll re-exposite this approach:
EXPOSITION
A theory $T$ is to be labeled as "proxi-finite" (i.e. in proximity with the world $HF$ of all well founded hereditarily finite sets) if and only if each axiom of $T$ OTHER than the axioms needed to define $V$ (the class of all sets) and $HF$ which are Extensionality, Class comprehension (of MK), empty set, closure of $V$ under singleton and Boolean union, and of course Infinity; must satisfy the following two conditions:
- Is of form $\psi^V$, where $\psi^V$ is a sentence obtained by bounding by $V$ of all quantifiers in an unbounded first order set theoretic sentence $\psi$, using bounding relation symbols $\in, \subseteq$; and each variable in $\psi$ must be written as $x_i$, where $i$ is the order of quantification of that variable in $\psi$; such that for every subformula $\phi$ of $\psi$, the following is provable from the rest of axioms of $T$:
$$\phi^{*^V} \to \phi^{*^{HF}}$$
Where $\phi^{*^X}$ is the sentence defined as:
$$[\mathcal Q_1 x_{i_1} \ b_1 \ X ,...,\mathcal Q_n x_{i_n} \ b_n \ X (\phi)] $$
where $i_j = 1,..,k$, for $j=1,..,n$; where $k$ is the total number of variables in $\psi$. Now $n$ is the total number of free variables in $\phi$. Each $\mathcal Q_i$ is a quantifier symbol, i.e. either $\forall$ or $\exists$; and each $b_i$ is a bounding relation symbol which is either $\in$ or $\subseteq$; the string $x_{i_1},..,x_{i_n}$ is the string of all free variables appearing in $\phi$ ordered after their quantificational sequence in $\psi$; that is: $j<l$ if and only if $i_j < i_l$ . Also we must have each $\mathcal Q_j x_{i_j} \ b_j \ X$ being the same as how it appears in $\psi$; more precisely: each $\mathcal Q_j x_{i_j} \ b_j \ X $ in $\phi^{*^X}$ is exactly the same as $\mathcal Q_m x_m \ b_m \ X$ in $\psi^X$ if $i_j=m$.
- $\psi^{HF} \to \psi^V $ is not provable from the rest of axioms of $T$.
I think the above can be simplified if we require $\psi$ to be in prenex normal form; now for any subformula $\phi$ of the matrix of $\psi$, we can easily define the sentence $\phi^*$ as $\phi$ preceded by the string of quantifiers over all free variables in $\phi$ that is a substring of the prefix of $\psi$.
Also I think we can change the second requirement to demand that $\psi^{HF}$ is provable from the basic sub-theory of $T$ that defined the world of hereditarily finite sets.
To show how this blocks the earlier trivialities. lets take $\psi$ to be the formula $``\forall x (finite(x)) \lor \theta"$ where $\theta$ is any axiom that is consistent with $ZF$ but false in $HF$. What happened in the earlier attempt which only demanded $\psi^V \to \psi^{HF}$ is that $\psi$ is "trivially" true of the hereditarily finite set world, this came to effect through bounding the quantifiers in the first subformula $\forall x (finite(x))$ by $HF$, but when generalized over the whole set world $V$, it was true because of $\theta$ and not because of the first subformula, actually the first subformula was false in $V$. Such an argument would be blocked here because $\theta$ is true in $V$ but not in $HF$.
To show that it blocks the un-limited consistency strength argument, we'll see that any arithmetical formula $p$ is bounded by the predicate $natural \ number$, which would bypass the first requirement above, but not the second requirement! Also it doesn't bypass the alternative form of the second requirement.
[EDIT] since the line of thought presented below did fail as Noah showed. I think its time to present it informally. What I'm seeing is that known theories like ZFC and MK are what I would label here informally as proxi-finite, this means that all of its axioms other than infinity are rules coming from the well founded hereditarily finite set world, i.e. $V_\omega$. I tried to define that by requiring that those axioms be of the form $\psi^V$ such that $\psi^V \to \psi^{HF}$; unfortunately that failed. However, the informal idea is there, even though it badly fails formally, for example an axiom saying that every set having many members, there is a set whose cardinality is strictly bigger than the cardinality of it and strictly smaller than that of its power. However, we can trivially also arrange for the opposite of that by having the formula "every set is finite or the negation of the above statement", and this would work to the opposite of what is intended. I think there must be some formal technique that ensure our informal notion. As examples :the general violation of the continuum hypothesis (for many membered sets) is proxi-finite, while the generalized continuum hypothesis is NOT. There are many other possible extensions of the former that are also proxi-finite. Also Choice is proxi-finite, while its negation is not.
This is the older post:
Let's label a theory $T$ as proxi-finite (i.e. in proximity with the world $HF$ of all well founded hereditarily finite sets) if and only if every axiom of $T$ other than the axiom of infinity is of the form $\psi^V$, that is a sentence that is $\in, \subset$-bounded by the class $V$ of all sets, such that: $$\psi^V \to \psi^{HF}$$ where $\psi$ is an sentence in the language of set theory, and $\psi^b$ is the formula obtained by merely $\in or \subset$ bounding every quantifier in $\psi$ by the set $b$.
For example Morse-kelley set theory is proxi-finite!
What is the strongest known proxi-finite theory?
Is there a limit to the consistency strength of proxi-finite theories?
Proxi-finite theories can be very strong! For example take MK and add to it the failure of the continuum hypothesis for all sets having many members. Which goes way beyond measurable cardinals! Yet I'm not sure if this is the furthest one can go? I suspect not!
There is no limit to the consistency strength of proxi-finite theories. If $T$ is a proxi-finite theory capable of talking about HF in an appropriate way - say, $T=$ MK for massive overkill - then $T+p$ is also proxi-finite for any arithmetical sentence$^1$ $p$. So just take $p=Con(S)$ for your favorite theory $S$. E.g. the theory $$\mbox{MK + Con("ZF + "There is a Reinhardt cardinal"")}$$ is proxi-finite, and has the same consistency strength as ZF + "There is a Reinhardt cardinal."
Note that whether or not $S$ is proxi-finite doesn't enter into the proxi-finiteness of $T+Con(S)$.
$^1$Or more precisely, the appropriate reformulation of an arithmetical sentence in the language of set theory; the "appropriate way" bit in the first half of that sentence is just to ensure that such reformulation can be done.