It's worth pointing out the obvious, i.e. that as long as 'const' is physical const instead of logical const (which is always), invariants and contracts can't be const, because that would restrict them from calling methods that are logically but not physically const. So I think they probably shouldn't be const.