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

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.