For example, [these](https://github.com/runtimeverification/verified-smart-contracts/blob/master/gnosis/verification.k#L12-L25). Also, there are some duplicate ones.