One of the main devs of Z3, Leonardo de Moura, is acutally working on a new, dependently typed, theorem prover called "Lean": http://leanprover.github.io/
Is Lean an LCF system or Curry-Howard based? It seems to be the latter, but if so, what's it's main advantage over the many other Curry-Howard based systems?