LeanDA: Distributed Algorithms in Lean 4

This repository contains my experiments with Lean 4. The main purpose is to see how Lean's features match the features of TLA⁺.

Available specifications:

• Two-phase commit in Lean. See the blog post 1 on specification and blog post 2 on proofs with Lean4:

  • Functional specification
  • System specification
  • Propositional specification
  • Functional-propositional refinement proofs
  • Safety proofs via inductive invariants

• EPFD in Lean: An eventually perfect failure detector under partial synchrony, accompanied with the blog post:

  • Propositional specification
  • Temporal proofs by induction:
    • strong completeness
    • strong accuracy is work in progress

• Ben-Or in Lean: Byzantine consensus with an agreement proof over generated Wunderspec definitions, accompanied with the blog post:

  • Ben-Or specification in Lean generated from ben_or.py
  • Inductiveness and agreement proof

• Single-height Tendermint in Lean: Byzantine consensus with generated Wunderspec definitions and Lean proofs transferred from TLAPS by Codex GPT 5.6, accompanied with the blog post:

  • Protocol and inductive-invariant definitions generated from tendermint_single_indinv.py
  • InitInd and NextInd inductiveness proofs transferred from tendermint_single_indinv_proofs.tla
  • Lock lemma and agreement proof