Formal Verification of Consensus Protocols in Lean

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.

Speakers: Roberto Saltini

Track: Core Protocol