Preprint
Jul 2026
LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean
This work formalizes SegWit-style blockchain primitives in LeanDY and demonstrates its expressiveness by carrying out an in-depth formalization of payment channels on top of this blockchain model, verifying punishment mechanisms and properties that depend on chain liveness.
Simon Jeanteur, Lorenzo Veronese, Magdalena Solitro et al.
· 0 citations