Does univ : univ always lead to a contradiction in a dependently typed language?
U : U is inconsistent in a wide variety of settings. It is safe to say that it's inconsistent in any type theory. Deriving False from it is feasible by hand. The simplest version of this is called Hurkens' paradox:

Original source
Coq implementation.
Agda implementation.

The Coq source additionally describes the sufficient conditions for getting False. In short, we don't need U : U, it's enough to have two universes, where one is contained in the other, and both are closed under impredicative function types.