Safe Owner List Invariants

The Safe smart account manages its owners using a singly-linked list stored in a mapping owners: address → address. The first node of the list is called SENTINEL and anchors the list at address key 0x1.

The list is updated by four operations: setupOwners builds it from an address array, addOwner inserts at the head, removeOwner unlinks a node, and swapOwner replaces one owner with another in a single step.

Why this matters

Safe is the most widely used multi-signature wallet on Ethereum, securing billions of dollars. If the owners list in OwnerManager were malformed, approval checks could skip a real owner or treat the signer set differently than what is expected.

How this was proven

The ownership operations are modeled in Verity from the Solidity OwnerManager.sol implementation in safe-smart-account; the Verity contract slice is in Contract.lean. Each function mutates the linked list differently:

• setupOwners: constructs the initial linked list from a list of addresses (base case)
• addOwner: head insertion. The new owner is placed between SENTINEL and the old head
• removeOwner: chain excision. The previous owner's pointer is redirected past the removed node
• swapOwner: atomic replacement. The old owner is unlinked and the new owner spliced into its position

How do you prove an owner is in the list? You show a concrete path: start at SENTINEL, follow the owners mapping one hop at a time, and arrive at that owner. If such a path exists, the owner is reachable. If no path exists, the owner is not in the list.

Beyond reachability, each function must preserve the full structural invariant: every node has exactly one incoming edge (unique predecessor), the list has no internal cycles, and isOwner changes exactly the intended addresses. The unique predecessor property is what makes removeOwner and swapOwner work: if you re-route a pointer, you need to know that nothing else was pointing to the old target. Because each node has exactly one incoming edge, that guarantee holds. An earlier draft assumed antisymmetry of reachability (matching Certora's spec), but that property is false on circular lists. Unique predecessor captures the same “no branching” truth without breaking on the cycle.

All proofs are verified by Lean 4's kernel and are provided in Proofs.lean. If any step were wrong, the code would not compile.

git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
lake build Benchmark.Cases.Safe.OwnerManagerReach.Compile

Proof status

All 16 theorems are proven. Proofs.lean is sorry-free.

Assumptions

The proofs use zero axioms. The only assumptions are the Solidity require guards the contract already enforces, and a three-field inductive invariant that is proven preserved by every mutation. Properties like noSelfLoops, freshInList, and acyclic are derived inside the proofs, not assumed.

• Solidity require guardsowner != 0, owner != SENTINEL, owners[owner] == 0, owners[prevOwner] == owner

  OwnerManager.sol (GS203–GS205)

  Every ownership-mutating function begins with require checks on its arguments. The proofs consume these in exactly the form the contract enforces, so no additional trust is needed.

• SafeOwnerInvariant (inductive)ownerListInvariant + uniquePredecessor + zeroInert

  Proven preserved by every mutation

  The proof is inductive: it assumes this bundled invariant holds before a function executes and proves it still holds after. The bundle contains three fields: the owner-list biconditional (membership equals reachability), unique predecessors (no branching), and zero-address inertness. setupOwners establishes it from clean storage (base case); addOwner, removeOwner, and swapOwner each preserve it (inductive step). Because preservation is proven, the invariant is a theorem, not a blind assumption.

View specs in LeanView proofs in Lean

Learn more

Certora OwnerReach.spec, the original specification this work is based on.

What is a formal proof? A short explanation for non-specialists.