Gossip in Lean

We use Lean 4 to verify results about Gossip protocols.

Standard Gossip

• The main result proven in Gossip.Sufficient is that calls are sufficient to make agents experts in a fully-connected graph.

• For the result that calls are also necessary, a proof sketch has been started in Gossip.Necessary.

• In Evaluation.lean we provide examples to verify the correctness of the Lean definitions.

Synchronous One-Error Gossip with Correction

In Gossip/Error we formalize Gossip with bit secrets and at most one transmission error. Moreover, in this setting agents self-correct by rejecting secret values they know to be wrong.

Authors

• Timo Doherty
• Andrei Mărculeşteanu
• Malvin Gattinger

The project was started as part of the following two bachelor theses.

• Timo Doherty: Efficient Information Dissemination: Formal Verification of Gossip Protocols Using Lean (2024)

• Tudor Andrei Mărculeşteanu: Formalization of Necessity Proof for Fully Connected Gossip Problems in Lean (2025)

For other references, see also the comments in Gossip.Necessary.