Closed
Description
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