I asked this question on MathOverflow a few months ago, but received no answers.
There are some mathematicians who are comfortable with ZFC but uneasy with large cardinals. For them, it may be unsettling that Mizar assumes infinitely many inaccessibles, and that Lean's dependent type theory makes a similar tacit assumption. Basically, this is because they appeal to Grothendieck universes.
Now, there is an alternative: Feferman's universes. (For a brief explanation of Feferman's universes, see pages 24–25 of Mike Shulman's paper, Set theory for category theory.) Feferman's universes achieve most of what a "practicing mathematician" wants from Grothendieck's universes, but has the advantage of being conservative over ZFC. So here's my question:
Suppose we wanted a proof assistant to avoid going beyond the consistency strength of ZFC, while retaining essentially all the functionality of something like Mizar or Lean. Could this be done using the Feferman-universe idea? How difficult would this be to implement and what would be the tradeoffs?
I see that there is a somewhat related question here on the Proof Assistants Stack Exchange, Alternatives to universe levels, but as of this writing, that question has no answers either.