Predictable verification using intrinsic definitions