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 It 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 Modeled and 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.

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

Hypotheses

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.

• inputs pass the contract's require checks

  OwnerManager.sol (GS203–GS205)

  Every ownership-mutating function begins with require checks on its arguments, drawn from owner != 0, owner != SENTINEL, owners[owner] == 0, and owners[prevOwner] == owner. The proofs consume these in exactly the form the contract enforces, so no additional trust is needed.

• owner list is well formed before each call

  Proven preserved by every mutation

  Before a function executes, the bundled invariant SafeOwnerInvariant holds. Its three fields are ownerListInvariant (membership equals reachability), uniquePredecessor (no branching), and zeroInert (the zero address is inert). The proof is inductive: 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.