Voevodsky left us far too early :( I share his concerns completely and have started studying the Lean theorem prover as a practical means for verification; although the theoretical basis for Lean is the Calculus of Inductive Constructions which is, as I understand it, incompatible with the univalence axiom.<p>At the end of the day, using whichever foundations you prefer, I encourage young mathematicians to look into proof assistants, and interested computer scientists to develop them; the more independent verifiers we have, the better.
I have never managed to understand why you need univalent foundations as opposed to just using some dependent type theory like Lean. As far as I see Lean could do all the mathematics I could imagine. I can only imagine that univalent foundations could help make things cleaner, but for now Lean seems good enough.