Sy Friedman's "Inner Model Hypothesis" (IMH) asserts that every first-order parameter-free sentence in the language of arithmetic that holds in some outer model of V already holds in some definable inner model. In collaboration with Philip Welch and Hugh Woodin, he has shown that the IMH is consistent from a Woodin cardinal with an inaccessible above and has consistency strength at least that of measurable cardinals of arbitrarily high Mitchell order.
The IMH itself is incompatible with large cardinals and implies that the universe is minimal: By a theorem of Beller and Jensen, there exists a real x in any model of the IMH such that L_alpha[x] does not satisfy ZFC, for all alpha. For this same reason the IMH cannot be extended to sentences with arbitrary real parameters. (Consider "omega_1 of L[x] is countable".)
We consider a variant of the IMH that is compatible with large cardinals, allows real parameters, and does not imply that the universe is minimal. Indeed, if the universe is sufficiently non-minimal, then this variant has a first-order formulation.