A Formally Verified Lightning Network

TL;DR

The paper addresses the question of whether the Lightning Network can guarantee funds safety for honest users. It builds a formal, Why3-based implementation of a two-party LN fragment over a simplified Bitcoin model and proves a machine-checkable funds-security property under a worst-case adversarial model, using idealized digital signatures and a modular, invariant-driven proof. Key contributions include a complete LN-focused implementation in Why3, a formal definition of funds ownership via an Evaluator, and a blueprint for extending the verification to more realistic LN features like HTLCs and multi-hop networks. The work provides a rigorous, end-to-end correctness argument for LN funds safety and offers a reusable framework for formal verification of blockchain-based protocols with clear separation between implementation details and security properties, potentially guiding production LN deployments.

Abstract

In this work we use formal verification to prove that the Lightning Network (LN), the most prominent scaling technique for Bitcoin, always safeguards the funds of honest users. We provide a custom implementation of (a simplification of) LN, express the desired security goals and, for the first time, we provide a machine checkable proof that they are upheld under every scenario, all in an integrated fashion. We build our system using the Why3 platform.

Figures (4)

• Figure 1: Conflicting transactions. $\textsf{tx}_{1}$ pays $2$ coins from $\textit{pk}_{1}$ to $\textit{pk}_{2}$, whereas $\textsf{tx}_{2}$ pays $1$ coin from $\textit{pk}_{1}$ to $\textit{pk}_{2}$. Since they spend the same output, at most one can be included on-chain. Funds ownership takes into account that the two transactions are mutually exclusive and only considers the maximum payout, $2$, concluding that $\textit{pk}_{1}$ owns $8$ coins. In contrast, the Evaluator considers the sum of the two payouts, $1+2=3$, concluding that $\textit{pk}_{1}$ owns $7$ coins.
• Figure 2: $\textsf{tx}_{2}$ is reachable, since $\textsf{tx}_{1}$ is signed. Both funds ownership and the Evaluator agree that $\textit{pk}_{1}$ has $0$ coins.
• Figure 3: $\textsf{tx}_{2}$ is unreachable, since $\textsf{tx}_{1}$ is unsigned. Both definitions do not take the payout of the invalid $\textsf{tx}_{1}$ into account. Nevertheless, according to funds ownership, $\textit{pk}_{1}$ has $10$ coins, but the Evaluator ignores the unreachability of $\textsf{tx}_{2}$ and thus decides that $\textit{pk}_{1}$ has $10-9=1$ coin.
• Figure :

Theorems & Definitions (1)

• definition thmcounterdefinition: Funds Security