A formal specification of the transaction propagation protocol in the mempool would allow to identify problems in the current implementation, propose optimizations, and help design a future implementation.

Tasks

• spec/mempool: First formal spec of the mempool implementation #614
  • When the formal spec is properly documented, there should not be a need of an informal spec.
• spec/mempool: Define safety and liveness properties #615
  • Checked with Apalache if/when possible