In this task we refine the output of #16 to provide lower level specifications, updated GOSSIP-I and P2P-I (in collaboration with other spec work) and data types.

Tasks:

• Refine GOSSIP-I, in english
• Refine GOSSIP-I, in Quint
• Refine P2P-I, in English (collaboration with other spec work)
• Refine P2P-I, in Quint (collaboration with other spec work)
• Update Quint tests.

DoD:

• Lower level specifications are provided in English and Quint. Specifications are tested and possibly formally checked.