Rank-into-rank axioms were initially thought to be close to inconsistency, but over time evidence accumulated that in a sense they are just one point in a natural hierarchy of symmetry principles. Kunen's inconsistency does not work without the axiom of choice (AC), while the impact of AC on the strengths of I3-I0 appears modest. This leads to a tension in that we believe in the axiom of choice (or at least use it), but the most natural known formulations of the stronger principles work in ZF without AC.
One option for studying principles at the consistency strengths of Reinhardt and Berkeley cardinals is to just work in ZF. Large Cardinals Beyond Choice (Bagaria, Koellner, Woodin 2019) is a good reading (but I disagree with its claim that the cardinals are unlikely to admit a reasonable inner model theory).
Finding a natural $Σ^V_2$ statement in ZFC that roughly corresponds to (say) a Berkeley cardinal in ZF is an open problem. However, we have some leads and alternatives.
One is to consider $Π^V_2$ axioms rather than $Σ^V_2$ axioms. Here we can state: "For every $κ$, there is a model of ZF + Berkeley Cardinal that is closed under $κ$-sequences". The use of "ZF" seems arbitrary, but I expect there is a natural combinatorial equivalent to the axiom (and likely not "0=1"). The reason is that the strength of Berkeley Cardinals likely increases with the degree of dependent choice $\mathrm{DC}_κ$, and the quantification over all $κ$ likely gives a natural closure point. Whether we use ZF or "ZF with just $Σ_2$ replacement" should not matter, and neither perhaps replacement of "Berkeley" with $κ$-fold iteration of having a nontrivial elementary embedding $V→V$, each time requiring the elementarity (and the replacement schema) to apply to the structure with the previously used embeddings.
Another way might be a model $M$ of ZF without AC that in some sense corresponds to $V$, so one can translate between statements about $M$ and statements above $V$. For example, at the level of many Woodin cardinals, we often have a pure extender model, a strategic extender model (HOD-like), and an AD model, with statements translatable between the three. And forcing can be viewed as a translation between different models.
We can also use inner models of ZF and/or HOD analogues of the choice-less cardinals. For example, we can ask for a nontrivial elementary self-embedding $j$ of $HOD(V_{λ+1})$ with $\operatorname{crit}(j)<λ$. (Technically, that uses second-order set theory, but we can also make similar statements about rank initial segments of $V$.) The consistency strength of just a nontrivial elementary self-embedding of HOD is unclear.
It is also possible that with rank-into-rank embeddings, we kind of exhausted natural (for $(V,∈)$) consistency strengths, in that (without disparaging the naturalness of going further) almost all current true conjectures/hypotheses about sets have a lower consistency strength. For example, Peano Arithmetic is reasonably complete, with natural arithmetic incompleteness hard to find (but they exist); and ideas implying Con(PA) tend to lead to infinite sets. Now, infinite sets of integers, low levels of the cumulative hierarchy, and elementary embeddings express progressively higher levels of symmetry, and increasing the level further might lead us to extend the language of set theory to study certain symmetry-based structures. My paper Reflective Cardinals (and its precursor Extending the Language of Set Theory) uses symmetry to extend the language of set theory, though it does not have much about very high consistency strengths (which is separate from defining cardinals larger than all $(V,∈)$ definable ones).
