> Have you tried the contracts module? I am aware of it, but I haven't tried it. That said, it's very incomplete, and Eiffel has had that much since the 80s. I think that was Eiffel's main selling point for a couple of decades.
However (a) I am interested in more than just that (e.g., void / null safety) and (b) what makes Ada / SPARK 2014 more interesting is that a prover is built into it. It doesn't just let you specify contracts, compile a debug version, run the debug version to test that contracts are satisfied, then compile and release a version where the contracts aren't tested. SPARK 2014 applies static analysis to prove that the code satisfies the specified contracts, using the [Why 3 solver](http://why3.lri.fr) solver. It isn't perfect; I've found (& reported) a bug in their system, which they said they fixed. But, it's much further along than anything I've seen anywhere else. (Anecdotal, but my sample set includes C, C++, Nim, Java, Kotlin, Modula-x, Oberon, and quite a few others. I don't think even Eiffel performs a static analysis, though it's been a while so I could be wrong about that.)
