> Rust has Design by Contract capabilities via the contracts crate

And C++ has reflection using boost ;)

Contracts for C++ have been proposed:

https://www.reddit.com/r/cpp/comments/cmk7ek/what_happened_t...

Not sure if / when they will land:

https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2022/p05...

You might be interested in the Prusti project, which statically checks for absence of reachable panics, overflows etc. It also allows user-defined specifications such as pre and post-conditions, loop body invariants, termination checking and so on.

https://github.com/viperproject/prusti-dev

In Eiffel at least, the contracts are checked at run time, whereas in Dafny it seems that it's verified at compile time.

I think (but I'm not sure) that Eiffel disables recursive contract checking (so checking a contract of a function used for checking the contract), so you could put the check for the inverse in each of the function's post conditions, but it would be quite the performance hit to verify it at each call.

Yeah, SPARK/Ada is a comparable system to Dafny. I agree with that! Also, Frama-C and a bunch of other more esoteric research languages as well.