> Also, what about Clojure? That runs on the JVM but how
  > does it fare on the "correctness" claim of Haskell, i.e.,
  > "If it compiles it's close to what the programmer
  > intended".

Clojure's a dynamic language, so fairly different in character and strengths. Save for a couple of statically typed Lisp dialects, provability/correctness/etc. is not really what that language family is all about.

If you want JVM and reasonably advanced type systems (given that Haskell's claim to correctness essentially boils down to this), try Scala.