Tasks

• Refined properties required/provided by Gossip from/to P2P are specified in English
• Refined properties required/provided by P2P from/to Gossip are specified in English
• Refined properties required/provided by State from/to Gossip are specified in English
• Refined properties required/provided by Gossip from/to State are specified in English

DoD:

• There exists a formal specification of the Gossip/P2P interactions and mismatches between requirements and provisions are identified.
• There exists a formal specification of the State/Gossip interactions and mismatches between requirements and provisions are identified.

Stretch goals:

• TNT is used to specify the properties.