Explore using Apalache to verify contract

[0xekez]

Informal has a CosmWasm Apalache example here: https://github.com/informalsystems/atomkraft/blob/dev/examples/cosmwasm/counter/models/counter.tla

We should explore what we can formally verify about this contract using Apalache. This learning will be very useful for our other IBC work. Some ideas for invariants for this contract:

1. Counterparty count should be the same as the number of times Increment {} has been called.
2. Closing a channel should reset the count to zero.

It might be good to keep things simple like this for our first try.