I also think that not having executable contracts by default (and defining whether you want them in your final program or not - see ghost code) is going to be a pain point in the future. I don't know nim enough to see if the syntax for provable properties is different from nim's ordinary syntax but I feel that it can also be a trap, to have your users learn yet another language for proof.
I'm hoping for the best here, and I must say, I'm quite happy to see other languages/environment jump in !
Some years ago you had only industrial support for Frama-C, Spark, and some academic success around JML? I don't know Eiffel's Eve enough to say whether I would consider it 'mature'. Nowadays with the work on Rust by Alastair Reid we're getting some new energy in the domain. Great!
If you mean having a hard dependency on z3 at compile time or something similar - no, it's not. :)
I can write a type that only handles integers 0-10, or floats [0...1], but it is more of a lift than I'd like to do in most cases, inefficient, and so I don't, even though it would be a boon for correctness and avoiding idiot bugs.