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:
-
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