Formal Verification of Consensus Protocols in Lean

Duration: NaN:NaN:NaN

Speaker: Roberto Saltini

Type: Workshop

Expertise: Some familiarity with the topic

Event: Devcon

Date: Nov 2026

Consensus protocols are notoriously difficult to model and verify: subtle choices in the formalization determine which assumptions are visible, which properties can be stated, and how much confidence we can place in the result. This is especially relevant as LLMs make it increasingly easy to generate Lean specifications and proofs, but syntactically valid formalization is not the same as a good model. This talk explores interactive theorem proving, model checking, and SMT-backed approaches in Lean, comparing how they support auditable specifications, explicit network and adversary assumptions, and proofs of both safety and liveness.