I'm not familiar enough with Idris to know exactly how state is handled, but yes, Idris is a prover, since it has dependent types.

If you want to verify your programs (and in 99.9% of programs you probably don't as you get it sufficiently correct by more lightweight techniques such as testing and code-reviews), then purity is fine, since you have to track effects explicitly anyway to prove non-trivial results, and doing this in a pure functional way or say with auxiliary variables in a Hoare-logic are kind-of/sort-of notational variants.

Dependent types aren't only useful in languages that prove theorems, so I think a better qualification for "provers" might be termination checking.

If "prover" just means "has dependent types" then that's a much larger class than it sounds like. I write a lot of Scala, which has dependent types, but most of the code I write is just ordinary web services.

I meant dependent types a la Agda, Coq etc that you can use for proving essentially arbitrary properties. Scala and Haskell do not have this.

I don't understand the distinction you're drawing. Idris' type level functions are easier to write than Scala's but they don't seem to be able to do anything that Scala ones can't.

To be clear, Haskell "has dependent types" to various degrees as well.