Formal Verification in PCN

What formal verification gives you

Bug taxonomy — what can go wrong, and what catches it

Three levels of formalization

Lightning Network as TLA+ — simplified pseudospec

(* State variables *)
VARIABLES alice_balance, bob_balance, htlc_in_flight, state,
          preimage_revealed, timeout_expired

(* Initial condition: channel opened with TOTAL_FUNDS split equally *)
Init ==
  /\ alice_balance = TOTAL_FUNDS \div 2
  /\ bob_balance   = TOTAL_FUNDS \div 2
  /\ htlc_in_flight = 0
  /\ state = "open"
  /\ preimage_revealed = FALSE
  /\ timeout_expired   = FALSE

(* Action: Alice proposes an HTLC *)
HTLC_SETUP(amount) ==
  /\ state = "open"
  /\ alice_balance >= amount
  /\ htlc_in_flight' = amount
  /\ alice_balance'  = alice_balance - amount
  /\ state' = "htlc_pending"
  /\ UNCHANGED <<bob_balance, preimage_revealed, timeout_expired>>

(* Action: Bob reveals preimage, receives funds *)
HTLC_FULFILL ==
  /\ state = "htlc_pending"
  /\ preimage_revealed = TRUE
  /\ htlc_in_flight' = 0
  /\ bob_balance'    = bob_balance + htlc_in_flight
  /\ state' = "settled"
  /\ UNCHANGED <<alice_balance, preimage_revealed, timeout_expired>>

(* Action: HTLC expires, Alice reclaims funds *)
HTLC_FAIL ==
  /\ state = "htlc_pending"
  /\ timeout_expired = TRUE
  /\ htlc_in_flight'  = 0
  /\ alice_balance'   = alice_balance + htlc_in_flight
  /\ state' = "failed"
  /\ UNCHANGED <<bob_balance, preimage_revealed, timeout_expired>>

(* Safety invariant — checked after EVERY transition *)
BalanceInvariant ==
  alice_balance + bob_balance + htlc_in_flight = TOTAL_FUNDS

(* Liveness: payment must eventually resolve *)
PaymentLiveness ==
  state = "htlc_pending" ~> (state = "settled" \/ state = "failed")

Interactive state machine — click a state to explore

What they verified — click each layer for details

Proof structure — click any node to expand

Lightning channel in Promela — conceptual model

/* Message types */
mtype = { UPDATE_ADD_HTLC, COMMITMENT_SIGNED, REVOKE_AND_ACK,
          UPDATE_FULFILL_HTLC, UPDATE_FAIL_HTLC, ERROR }

/* Shared channel state */
int alice_balance = 500000;  /* satoshis */
int bob_balance   = 500000;
int htlc_amount   = 0;
byte channel_state = 0;     /* 0=open, 1=pending, 2=closed */

/* Bidirectional channel between Alice and Bob */
chan a2b = [4] of { mtype, int };
chan b2a = [4] of { mtype, int };

active proctype Alice() {
  int amount;
  do
  :: /* Initiate payment */
     amount = 10000;
     atomic {
       alice_balance >= amount;
       alice_balance = alice_balance - amount;
       htlc_amount = amount;
       channel_state = 1;
     }
     a2b!UPDATE_ADD_HTLC, amount;
     b2a?COMMITMENT_SIGNED, _;
     a2b!REVOKE_AND_ACK, 0;
     b2a?COMMITMENT_SIGNED, _;
     a2b!REVOKE_AND_ACK, 0;
     /* Await resolution */
     if
     :: b2a?UPDATE_FULFILL_HTLC, _ ->
           skip   /* payment succeeded */
     :: b2a?UPDATE_FAIL_HTLC, _ ->
           alice_balance = alice_balance + amount;
           htlc_amount = 0;
           channel_state = 0;
     fi
  :: break
  od
}

active proctype Bob() {
  int amount;
  do
  :: /* Respond to incoming HTLC */
     a2b?UPDATE_ADD_HTLC, amount;
     b2a!COMMITMENT_SIGNED, 0;
     a2b?REVOKE_AND_ACK, _;
     b2a!COMMITMENT_SIGNED, 0;
     a2b?REVOKE_AND_ACK, _;
     if
     :: /* Preimage known — fulfill */
        b2a!UPDATE_FULFILL_HTLC, 0;
        bob_balance = bob_balance + amount;
        htlc_amount = 0; channel_state = 0;
     :: /* Cannot fulfill — fail */
        b2a!UPDATE_FAIL_HTLC, 0;
     fi
  :: break
  od
}

/* Never property: Spin verifies this never becomes false */
never { /* balance sum invariant */
  do
  :: skip
  :: (alice_balance + bob_balance + htlc_amount != 1000000) -> break
  od
}

LTL Properties — hover or click for explanation

/* The "God's-eye" ideal version of LN */

On receive (OPEN, Alice, Bob, amount):
  channel[Alice,Bob] = {
    bal_a: amount / 2,
    bal_b: amount / 2,
    open: true
  }

On receive (PAY, from=Alice, to=Bob, amt):
  if channel[Alice,Bob].bal_a >= amt:
    channel[Alice,Bob].bal_a -= amt
    channel[Alice,Bob].bal_b += amt
    output (SUCCESS, Bob, amt)
  else:
    output (FAILURE, Alice)

On receive (CLOSE, Alice, Bob):
  pay channel[Alice,Bob].bal_a to Alice on-chain
  pay channel[Alice,Bob].bal_b to Bob on-chain
  channel[Alice,Bob].open = false

/* Real LN ≡_UC F_LN iff:
   for all env Z, adv A, ∃ sim S:
   EXEC[LN, A, Z] ≈ EXEC[F_LN, S, Z] */

Malavolta et al. — Concurrency and Privacy in PCN

Key security properties — click to expand

The HTLC timeout ordering constraint

Sprites solution

Collateral lockup calculator

Click any row to expand details about learning curve, strengths, limitations, and PCN papers that use each tool.

Which LN protocol components have been formally verified? Hover any cell for details.

Open problems in formal verification