Assurance

Formal verification

The rules the covenant enforces are proved correct in Lean 4: 72 machine-checked theorems, no unfinished proofs, about 4,500 lines with no external libraries. The central one says that anyone holding a leaf and its path can always build an accepted exit that pays the leaf's amount, without anyone's help and without touching another leaf. The off-chain protocol, where the risks are orderings and timing, has a P model designed but not yet built.

Three layers, three kinds of check

A proof about the rules says nothing about whether the scripts implement them, and a test of the scripts says nothing about every possible tree. So each layer is checked by the method that fits it, and the layers are tied together by shared data.

The headline theorem

Section 10.2 of the specification argues that a member can always leave. In Lean that argument is payable: for any tree and any position holding a leaf, the honest witness is a valid step from the current root to the root of the tree without that leaf, the sum drops by exactly the leaf's amount, and no other position changes.

theorem payable {d : Nat} (t : Tree d) (p : Pos d 0) (l : Leaf)
    (hl : t.get p = some l) :
    (leafStep (t.path p) (some l) none).valid t.root (t.set p none).root ∧
    (t.set p none).root.sum + l.amount = t.root.sum ∧
    ∀ q, q ≠ p → (t.set p none).get q = t.get q

Paired with ExitK.no_inflation, which says no exit pays out more than the tree holds, and exit_available, which says the exit pays the leaf's own exit key, this is the property the whole design exists for. chain_state lifts it to histories: every root that ever appears on-chain is the root of a tree reachable by the rules, its committed sum is that tree's total, and every leaf in it has an accepted exit.

What is proved

Conservation

Steps.sum: for any sequence of steps, the new root's sum plus what was removed equals the old root's sum plus what was added. It needs no assumption about the nodes, so the covenant conserves value even against a prover who invents nodes. Reachable.ledger states the same over a whole history.

Binding

fold_sound: any node and path that fold to the committed root are a real subtree and its real path. A forged leaf or a stale root cannot pass. This is the only theorem that uses the hash assumptions. witness_root_binds and output_binds tie the root to the output key, and CCVTweak.binding proves the same for the CCV tier's key from its two tweak stages.

Every transition

Exit, join, update, claim and split, merge and reclaim, the cohort sweep, the cohort rewrite and the detach each have a soundness theorem: what the old tree held, what output 0 commits to, and how the amounts balance. For example rewrite_payout_conservation covers a rewrite that mixes exits, joins, resizes and unchanged positions.

Vouchers

voucher_no_replay: once redeemed, a voucher's message never verifies against the tree again, under three stated hypotheses about issuers. voucher_survives_topup: an operator raising the leaf's amount does not void a voucher. voucher_survives_detach: a voucher follows its leaf into a detached tree.

The pending-leaf receive

The merge claim, the reclaim and the reclaim form of the cohort rewrite (payments) each have a soundness theorem: merge_sound says a merge moves value only from the source into the sibling it exits to, reclaim_sound that a reclaim removes one reclaimable leaf past its deadline and no other, and rewrite_transfer_sound that a rewrite can lower a reclaimable leaf only into its own sibling. reclaim_only_flagged says every leaf that is not flagged reclaimable stays in the tree, and a tree without a reclaim key accepts no reclaim at all. merge_body_preserved: a merge changes no leaf's body, so it voids no voucher. merge_target_monotone and merge_stale_rejected: a merge raises its target exactly to the voucher's level, and once the target holds that level, replaying the voucher or redeeming an older, lower one moves nothing. merge_no_overpay bounds what merges into one leaf can pay, along any history, by the largest level ever signed for it. rewrite_reclaimable_change: a reclaimable leaf changes without its owner only by an amount increase, an exactly absorbed transfer, or after its deadline.

Histories

Accepts.sound and Chain.sound bridge the chain and the model: every root a chain of accepted spends reaches is the root of a tree reachable by the transition records. Reachable.ledger keeps the books across those records, merges moving nothing and reclaims removing exactly the reclaimed amount. Reachable.dust and Reachable.evictable carry the dust floor and eviction through a whole history.

Eviction cannot be escaped

claim_evictable and Reachable.evictable: no sequence of carves produces a leaf the cohort's sweep cannot remove.

Path maintenance

path_maintenance: after any transition, every other member's path changes in exactly one entry, which they can compute from the published witness. Staying ready to exit needs no one's help.

Encodings

The leaf and node serialisations are injective, the 8-byte sum encoding is the minimal one the scripts compute, and the PADZ gadget of the MID and MIN tiers accepts exactly one pad and caps sums below 2³¹.

What the proofs changed

Writing the proofs found places where the specification was wrong, imprecise or relying on something it did not say. Each became a fix, a stated requirement or a test.

• Grafted cohorts. Conservation holds for any node, but exits hold only for nodes with a real tree behind them. A cohort graft whose node has no preimage freezes its value forever. The specification's rule that joiners check their own paths before funding was already there; the proof shows the rule is necessary, and the model carries it as an explicit hypothesis.
• The self-voucher. The specification said a redeemed source leaf never recurs. self_voucher_fixed is a counterexample: a voucher whose claim leaf is its source leaf leaves the tree unchanged and verifies again. No value moves, but the sentence was false, and the non-replay theorem now names the hypothesis that excludes it.
• Different SEQ_FINAL per tier. Why the final sequence number is 0xFFFFFFFF in FULL but 0x7FFFFFFF in MID is a theorem about number encodings: ff ff ff ff is a negative number in MID's numerics with a four-byte successor, so it could still be claimed.
• A fix that reached only the model. The rule stopping the operator from changing a finalised channel leaf's amount alone was in the Lean model but not yet in the specification or scripts. An audit probe found the gap, and the fix landed everywhere (review finding F34).
• Vouchers bound to the leaf without its amount. Spec 0.13.0 changed what a voucher signs so that an operator top-up does not void it. voucher_survives_topup proves the new rule, and its proviso exposed the one remaining case: a top-up smaller than the dust floor blocks, but does not void, a voucher for the whole balance.
• The merge target and the transfer sibling. The first rules for the pending-leaf receive required a merge's target to be owned by the source's exit key but not to exit to it. The model found two consequences: value could leave a key's exits through a merge into a leaf it owned that exits elsewhere, and two leaves each owned by the other's exit key could merge back and forth, so a replayed voucher moved value across keys. Both the merge claim and the reclaim-form rewrite now require equal exit keys (MergeOk.exit_eq, Tree.Transfer). After that Reachable.exit_value holds: along any history of merges and reclaims, the amount held in leaves that are not reclaimable and exit to one key never decreases. The only cycles left are within one key (merge_cycle_overpays), which the bound merge_no_overpay counts. That bound needs the operator to advance a landing leaf's seq in any decrease it co-signs, a rule the scripts do not check.
• Unconditional facts made explicit. A claim's position must be empty after the source step, not before, so a drained source can be reused in the same transaction. Published cohorts are grounded by construction, so a cohort admitted by rewrite carries none of the graft caveat.

What it assumes

What it does not prove

• The bytecode. The model states the rules as relations on nodes and paths. That the tapscript implements them is shown by running it, not by proof. A verified interpreter for the tapscript subset would close the gap; it is a separate project.
• Signatures and timelocks. Authorisation decides who may act, not what the action does to the tree, so it is an opaque proposition. Conservation does not depend on it.
• Obligations the scripts do not check. Unique (owner_key, nonce) pairs, positive amounts on admitted leaves, valid curve points and grounded grafts are taken as hypotheses, because they are requirements on creators, not covenant guarantees. The formal/README.md lists each one.
• Mempool, reorgs, timing and channels. These belong to the off-chain protocol, below.

The off-chain protocol: a P model, designed

The off-chain failures are interleavings: an eviction landing between an HTLC's acceptance and its expiry, an operator's transaction replacing an owner's exit one block before a deadline, a reorg reverting an exit after a channel's update chain started. A model checker explores those orderings; no theorem about hash trees reaches them. design/p-model.md designs a model in P with seven machine types, among them the chain, an honest and a Byzantine operator, owners, channel parties and a watchtower, and these properties:

The design includes six adversarial scenarios, one of them a fee-reserve exhaustion that is expected to fail, and a requirement that the model's covenant check is differentially tested against the Python reference so it cannot drift into checking a protocol nobody wrote. It is estimated at about seven weeks of work and has not been started. There is no TLA+ or PlusCal model.

Running it

cd formal
lake build    # compiles every module, then prints the axiom audit

The toolchain is pinned (Lean 4.24.0), there are no dependencies to fetch, and the build takes a few seconds. The audit prints the axioms each headline theorem depends on; only Lean's standard ones appear, and any line naming sorryAx would mean an unfinished proof. CI runs the build on every push.