Protocols Made Fun

Proving completeness of an eventually perfect failure detector in Lean4

Proving consistency of two-phase commit in Lean4

Specifying and simulating two-phase commit in Lean4

The value of model checking in distributed protocols design

Model checking safety of Ben-Or’s Byzantine consensus with Apalache

Why I use TLA+ and not(TLA+): Episode 1

Specification and Model-checking of the ZKsync Governance Protocol

Specification and model checking of BFT consensus by Matter Labs

The Rise of Model Checker: Verifying Blockchain Monitors In and Near Realtime (Solarkraft #5)

The Force Awakens: Hybrid Blockchain Runtime Monitors (Solarkraft #4)