Properties of IBC I think it would be helpful to formalise (e.g. in TLA+):
Packet replay prevention: given some set of chains correctly following the IBC protocol with arbitrary connections between them, and some correctly generated & authenticated IBC packet, prove that the packet can only be confirmed on one chain.
Timeout semantics: given an IBC connection between two chains which may not necessarily make progress, prove that a packet is either committed (perhaps along with its receipt) on both chains or that a timeout can be submitted to the source chain.
Masquerade prevention: given an IBC connection between two chains correctly following the IBC protocol, prove that a third malicious chain cannot masquerade (send packets from) as either of the two connected chains, including if the third chain can send messages during the handshake process.
Byzantine fault handling: given a Byzantine fault committed by a validator set on one chain connected to a set of other chains, prove that this fault cannot affect chains which are not directly connected to the Byzantine chain (particularly w.r.t. multi-hop packet relay).
Ported from https://github.com/cosmos/ics/issues/42.
Properties of IBC I think it would be helpful to formalise (e.g. in TLA+):