Towards a Formal Verification of the Lightning Network with TLA+

TL;DR

This paper presents a formal verification of the Lightning Network protocol using TLA+, demonstrating that the protocol meets its security properties through a combination of model checking and formal proofs.

Contribution

It introduces a formal model of the Lightning Network and employs a chain of refinements to verify its security properties, addressing the challenge of large state spaces.

Findings

The protocol fulfills expected security properties.

A chain of refinements effectively verifies complex protocol security.

Formal verification methods are applicable to blockchain payment networks.

Abstract

Payment channel networks are an approach to improve the scalability of blockchain-based cryptocurrencies. Because payment channel networks are used for transfer of financial value, their security in the presence of adversarial participants should be verified formally. We formalize the protocol of the Lightning Network, a payment channel network built for Bitcoin, and show that the protocol fulfills the expected security properties. As the state space of a specification consisting of multiple participants is too large for model checking, we formalize intermediate specifications and use a chain of refinements to validate the security properties where each refinement is justified either by model checking or by a pen-and-paper proof.