I'm not familiar with Spec, but what you're describing sounds like enforcing preconditions but not postconditions by default, which is what most DbC frameworks (or languages with intrinsic support) normally do. The idea being that most of the time, you're running library code, and you want to validate what you're passing in, but you trust it to do the right thing for any input that is valid.