The Tendermint algorithm shares state by message exchange.
However, we are defining the state gossiped as tuples in a tuple space, implemented as something like a 2P-Set CRDT.
Tuples correspond to messages, but thinking in terms of state makes it easier to compare nodes state and gossip to converge.
However, the consensus algorithm itself does not specify when messages can be not delivered, which corresponds tuples being dropped from the space.

This task aims at providing a definition of when to drop entries from the tuple space. It shall produce specification in English and Quint, and include Quint tests to check the behavior.

Depending on the tooling, model checking may be used.