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:

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