From 4526bad5549ac610363d4443c991b2ea8f0d681d Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 9 Apr 2026 08:51:53 +0200 Subject: [PATCH 01/13] Add Safe owner list reachability invariant research page New case study page for the formally verified inListReachable invariant of the Safe OwnerManager linked list, proven using Verity and Lean 4. Co-Authored-By: Claude Opus 4.6 --- components/research/SafeGuarantee.jsx | 92 ++++++ data/research.js | 10 + pages/research/safe-owner-reachability.jsx | 323 +++++++++++++++++++++ 3 files changed, 425 insertions(+) create mode 100644 components/research/SafeGuarantee.jsx create mode 100644 pages/research/safe-owner-reachability.jsx diff --git a/components/research/SafeGuarantee.jsx b/components/research/SafeGuarantee.jsx new file mode 100644 index 0000000..554e66f --- /dev/null +++ b/components/research/SafeGuarantee.jsx @@ -0,0 +1,92 @@ +import { useState, useEffect, useRef } from 'react' +import { ExternalLinkIcon } from './ExternalLink' + +export default function SafeGuarantee() { + const [showEnglish, setShowEnglish] = useState(true) + const timerRef = useRef(null) + + useEffect(() => { + timerRef.current = setTimeout(() => setShowEnglish(false), 5000) + return () => clearTimeout(timerRef.current) + }, []) + + const handleToggle = () => { + if (timerRef.current) { + clearTimeout(timerRef.current) + timerRef.current = null + } + setShowEnglish((prev) => !prev) + } + + return ( +
+ + +
+
+ 
+            {'-- for every address in the list'}
+            {'\n'}
+            {'next(SENTINEL) \u2260 0  \u2227'}
+            {'\n'}
+            
+              {'\u2200 key, next(key) \u2260 0 \u2192 reachable(SENTINEL, key)'}
+            
+
+
+
+

+ Every owner in the Safe can be reached by walking the list from the sentinel node. +

+
+
+ +
+ + View Lean + + +
+
+ ) +} diff --git a/data/research.js b/data/research.js index e793009..16c84f0 100644 --- a/data/research.js +++ b/data/research.js @@ -38,6 +38,16 @@ export const research = [ date: '2025-06-01', tag: 'Explainer' }, + { + slug: 'safe-owner-reachability', + title: 'Safe Owner List Reachability Invariant', + subtitle: + 'A formally verified linked list invariant of the Safe smart account.', + description: + 'How we proved that addOwner preserves reachability in the Safe OwnerManager linked list using Verity and Lean 4.', + date: '2026-04-09', + tag: 'Case study' + }, { slug: 'lido-vault-solvency', title: 'Lido V3 Vault Solvency Guarantee', diff --git a/pages/research/safe-owner-reachability.jsx b/pages/research/safe-owner-reachability.jsx new file mode 100644 index 0000000..7970f6a --- /dev/null +++ b/pages/research/safe-owner-reachability.jsx @@ -0,0 +1,323 @@ +import Head from 'next/head' +import Link from 'next/link' +import PageLayout from '../../components/PageLayout' +import ResearchCard from '../../components/ResearchCard' +import SafeGuarantee from '../../components/research/SafeGuarantee' +import Disclosure from '../../components/research/Disclosure' +import CodeBlock from '../../components/research/CodeBlock' +import ExternalLink from '../../components/research/ExternalLink' +import { research } from '../../data/research' + +function Hypothesis({ name, constraint, source, children, border = true }) { + return ( +
  • +
    + + + + + {name} + {constraint} + +
    +

    + + {source} + +

    +

    {children}

    +
    +
    +
    • + ) +} + +const VERIFY_COMMAND = `git clone https://github.com/lfglabs-dev/verity-benchmark +cd verity-benchmark +lake build Benchmark.Cases.Safe.OwnerManagerReach.Compile` + +export default function SafeOwnerReachabilityPage() { + const otherResearch = research.filter( + (r) => r.slug !== 'safe-owner-reachability' + ) + + return ( + <> + + + Safe Owner List Reachability Invariant | Research | LFG Labs + + + + +
    + + +
    +

    + Safe Owner List Reachability Invariant +

    +
    + + {/* The Guarantee */} +
    + +

    + The{' '} + + Safe smart account + {' '} + manages its owners using a singly-linked list stored in a + mapping{' '} + + owners: address → address + + . A sentinel node at address{' '} + 0x1 anchors + the list. When an owner is added, it is inserted at the head: +

    + 
    +              {'SENTINEL \u2192 ownerA \u2192 ownerB \u2192 SENTINEL\n'}
+              {'SENTINEL \u2192 NEW \u2192 ownerA \u2192 ownerB \u2192 SENTINEL'}
+
    +
    + + {/* Why this matters */} +
    +

    + Why this matters +

    +

    + The Safe is the most widely used multi-signature wallet on + Ethereum, securing billions of dollars. Its{' '} + OwnerManager{' '} + contract maintains the set of signers as a linked list. If{' '} + addOwnerWithThreshold{' '} + could leave a node unreachable from the sentinel, the owner + would exist in storage but be invisible to the signing logic, + breaking the integrity of the multisig. +

    + +

    + This proof covers the{' '} + inListReachable{' '} + invariant from Certora's{' '} + OwnerReach.spec: + after{' '} + addOwner{' '} + executes, every node with a non-zero successor in the{' '} + owners mapping + is reachable from SENTINEL by following next-pointers. +

    +

    + It does not cover{' '} + removeOwner,{' '} + swapOwner, or the + initial{' '} + setupOwners{' '} + call. Threshold management is also elided as it does not + affect the owners mapping. +

    +     +
    + + {/* How this was proven */} +
    +

    + How this was proven +

    +

    + The{' '} + addOwnerWithThreshold{' '} + function performs a head insertion into the linked list. Proving + reachability is preserved requires showing that: the new + owner is reachable (via{' '} + + SENTINEL → owner + + ), and all previously reachable nodes remain reachable through + the updated path ( + + SENTINEL → owner → old head → ... + + ). +

    +

    + Reachability is expressed using witness chains: a + concrete list of addresses where each consecutive pair follows + the{' '} + owners{' '} + mapping. This turns the transitive closure into induction on + list indices, making the proof mechanically checkable. +

    +

    + The contract logic was modeled in{' '} + + Verity + + . The proof first characterizes the post-state (which + next-pointers changed), then lifts pre-state chains to the + post-state and prepends the new path. A reference proof is + provided in{' '} + + Proofs.lean + + . +

    +

    + The proof is checked by Lean 4's kernel, a small program + that accepts or rejects proofs deterministically. If the proof + were wrong, it would not compile. +

    + + {VERIFY_COMMAND} +

    + If the build succeeds, the proof is correct.{' '} + + Source repository + +

    +     +
    + + {/* Hypotheses */} +
    +

    + Hypotheses +

    +

    + The proof uses zero axioms. The theorem requires these + hypotheses, which encode the function's preconditions and + structural assumptions about the linked list: +

    +
      + + The new owner cannot be the zero address. Enforced by the{' '} + require guard + in{' '} + + addOwnerWithThreshold + + . + + + The sentinel address is reserved as the list anchor and + cannot be used as an owner. Adding it would corrupt the list + structure. + + + The owner must not already be in the list. A zero mapping + value means the address is not yet a node. This prevents + duplicate insertion which would create cycles. + + + The proof is inductive: it assumes the reachability invariant + holds before{' '} + addOwner and + shows it holds after. The base case (initial setup via{' '} + setupOwners) + is not covered. + + + The linked list does not cycle back to SENTINEL before + reaching its natural end. Without this, lifting pre-state + chains to the post-state would be unsound, because + SENTINEL's next-pointer changes during insertion. + + + Strengthens{' '} + hFresh: the + new owner address must not appear anywhere in the existing + chain, not just have a zero mapping value. This ensures that + the owner's next-pointer (which changes during + insertion) does not affect any existing chain. + +
    +

    + + View specs in Lean + + + View proof in Lean + +

    +
    + + {/* Learn more */} +
    +

    + Learn more +

    +

    + + What is a formal proof? + {' '} + A short explanation for non-specialists. +

    +
    + + {otherResearch.length > 0 && ( +
    +

    + More research +

    +
    + {otherResearch.map((r) => ( + + ))} +
    +
    + )} +
    +     + + ) +} From 934c77ebc0f181e1532c66f47ed3aacc38256a2e Mon Sep 17 00:00:00 2001 From: "Thomas Marchand (agent)" Date: Thu, 9 Apr 2026 09:02:43 +0200 Subject: [PATCH 02/13] Fix research ordering and shared hypothesis UI --- components/research/Hypothesis.jsx | 39 +++++++++++++++++++ lib/getSortedResearch.js | 5 +++ ...formalizing-transaction-interpretation.jsx | 4 +- pages/research/index.jsx | 4 +- pages/research/lido-vault-solvency.jsx | 39 ++----------------- pages/research/safe-owner-reachability.jsx | 39 ++----------------- pages/research/verity-benchmark.jsx | 6 ++- pages/research/verity.jsx | 4 +- pages/research/what-is-a-formal-proof.jsx | 4 +- 9 files changed, 63 insertions(+), 81 deletions(-) create mode 100644 components/research/Hypothesis.jsx create mode 100644 lib/getSortedResearch.js diff --git a/components/research/Hypothesis.jsx b/components/research/Hypothesis.jsx new file mode 100644 index 0000000..cc573e1 --- /dev/null +++ b/components/research/Hypothesis.jsx @@ -0,0 +1,39 @@ +export default function Hypothesis({ + name, + constraint, + source, + children, + border = true +}) { + return ( +
  • +
    + + + + + {name} + {constraint} + +
    +

    + + {source} + +

    +

    {children}

    +
    +
    +
    • + ) +} diff --git a/lib/getSortedResearch.js b/lib/getSortedResearch.js new file mode 100644 index 0000000..c0ca933 --- /dev/null +++ b/lib/getSortedResearch.js @@ -0,0 +1,5 @@ +import { research } from '../data/research' + +export function getSortedResearch() { + return [...research].sort((a, b) => b.date.localeCompare(a.date)) +} diff --git a/pages/research/formalizing-transaction-interpretation.jsx b/pages/research/formalizing-transaction-interpretation.jsx index 14ee33b..9d7debb 100644 --- a/pages/research/formalizing-transaction-interpretation.jsx +++ b/pages/research/formalizing-transaction-interpretation.jsx @@ -6,7 +6,7 @@ import CodeBlock from '../../components/research/CodeBlock' import Disclosure from '../../components/research/Disclosure' import ExternalLink from '../../components/research/ExternalLink' import HighlightedDSL from '../../components/research/HighlightedDSL' -import { research } from '../../data/research' +import { getSortedResearch } from '../../lib/getSortedResearch' export default function WhyClearSigningShouldNotRequireTrustPage() { const canonicalUrl = @@ -36,7 +36,7 @@ export default function WhyClearSigningShouldNotRequireTrustPage() { }, mainEntityOfPage: canonicalUrl } - const otherResearch = research.filter( + const otherResearch = getSortedResearch().filter( (r) => r.slug !== 'formalizing-transaction-interpretation' ) diff --git a/pages/research/index.jsx b/pages/research/index.jsx index 82f6e28..2afee6f 100644 --- a/pages/research/index.jsx +++ b/pages/research/index.jsx @@ -2,9 +2,11 @@ import Head from 'next/head' import PageLayout from '../../components/PageLayout' import ResearchCard from '../../components/ResearchCard' import SectionHeader from '../../components/ui/SectionHeader' -import { research } from '../../data/research' +import { getSortedResearch } from '../../lib/getSortedResearch' export default function ResearchPage() { + const research = getSortedResearch() + return ( <> diff --git a/pages/research/lido-vault-solvency.jsx b/pages/research/lido-vault-solvency.jsx index d760266..2990cb0 100644 --- a/pages/research/lido-vault-solvency.jsx +++ b/pages/research/lido-vault-solvency.jsx @@ -6,48 +6,15 @@ import Guarantee from '../../components/research/Guarantee' import Disclosure from '../../components/research/Disclosure' import CodeBlock from '../../components/research/CodeBlock' import ExternalLink from '../../components/research/ExternalLink' -import { research } from '../../data/research' - -function Hypothesis({ name, constraint, source, children, border = true }) { - return ( -
  • -
    - - - - - {name} - {constraint} - -
    -

    - - {source} - -

    -

    {children}

    -
    -
    -
    • - ) -} +import Hypothesis from '../../components/research/Hypothesis' +import { getSortedResearch } from '../../lib/getSortedResearch' const VERIFY_COMMAND = `git clone https://github.com/lfglabs-dev/verity-benchmark cd verity-benchmark ./scripts/run_default_agent.sh lido/vaulthub_locked/locked_funds_solvency` export default function LidoVaultSolvencyPage() { - const otherResearch = research.filter( + const otherResearch = getSortedResearch().filter( (r) => r.slug !== 'lido-vault-solvency' ) diff --git a/pages/research/safe-owner-reachability.jsx b/pages/research/safe-owner-reachability.jsx index 7970f6a..6e51118 100644 --- a/pages/research/safe-owner-reachability.jsx +++ b/pages/research/safe-owner-reachability.jsx @@ -6,48 +6,15 @@ import SafeGuarantee from '../../components/research/SafeGuarantee' import Disclosure from '../../components/research/Disclosure' import CodeBlock from '../../components/research/CodeBlock' import ExternalLink from '../../components/research/ExternalLink' -import { research } from '../../data/research' - -function Hypothesis({ name, constraint, source, children, border = true }) { - return ( -
  • -
    - - - - - {name} - {constraint} - -
    -

    - - {source} - -

    -

    {children}

    -
    -
    -
    • - ) -} +import Hypothesis from '../../components/research/Hypothesis' +import { getSortedResearch } from '../../lib/getSortedResearch' const VERIFY_COMMAND = `git clone https://github.com/lfglabs-dev/verity-benchmark cd verity-benchmark lake build Benchmark.Cases.Safe.OwnerManagerReach.Compile` export default function SafeOwnerReachabilityPage() { - const otherResearch = research.filter( + const otherResearch = getSortedResearch().filter( (r) => r.slug !== 'safe-owner-reachability' ) diff --git a/pages/research/verity-benchmark.jsx b/pages/research/verity-benchmark.jsx index b539f66..7b86169 100644 --- a/pages/research/verity-benchmark.jsx +++ b/pages/research/verity-benchmark.jsx @@ -3,10 +3,12 @@ import Link from 'next/link' import PageLayout from '../../components/PageLayout' import ResearchCard from '../../components/ResearchCard' import ExternalLink from '../../components/research/ExternalLink' -import { research } from '../../data/research' +import { getSortedResearch } from '../../lib/getSortedResearch' export default function VerityBenchmarkPage() { - const otherResearch = research.filter((r) => r.slug !== 'verity-benchmark') + const otherResearch = getSortedResearch().filter( + (r) => r.slug !== 'verity-benchmark' + ) return ( <> diff --git a/pages/research/verity.jsx b/pages/research/verity.jsx index fab151b..c6e2a40 100644 --- a/pages/research/verity.jsx +++ b/pages/research/verity.jsx @@ -3,10 +3,10 @@ import Link from 'next/link' import PageLayout from '../../components/PageLayout' import ResearchCard from '../../components/ResearchCard' import ExternalLink from '../../components/research/ExternalLink' -import { research } from '../../data/research' +import { getSortedResearch } from '../../lib/getSortedResearch' export default function VerityPage() { - const otherResearch = research.filter((r) => r.slug !== 'verity') + const otherResearch = getSortedResearch().filter((r) => r.slug !== 'verity') return ( <> diff --git a/pages/research/what-is-a-formal-proof.jsx b/pages/research/what-is-a-formal-proof.jsx index 1483546..1056dd0 100644 --- a/pages/research/what-is-a-formal-proof.jsx +++ b/pages/research/what-is-a-formal-proof.jsx @@ -2,10 +2,10 @@ import Head from 'next/head' import Link from 'next/link' import PageLayout from '../../components/PageLayout' import ResearchCard from '../../components/ResearchCard' -import { research } from '../../data/research' +import { getSortedResearch } from '../../lib/getSortedResearch' export default function WhatIsAFormalProofPage() { - const otherResearch = research.filter( + const otherResearch = getSortedResearch().filter( (r) => r.slug !== 'what-is-a-formal-proof' ) From 87f4a99e6c41228737df47d094a0c6ea36caa8aa Mon Sep 17 00:00:00 2001 From: "Thomas Marchand (agent)" Date: Thu, 9 Apr 2026 09:07:04 +0200 Subject: [PATCH 03/13] Add Bun-based CI workflow --- .github/workflows/ci.yml | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 .github/workflows/ci.yml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 0000000..bfdf348 --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,35 @@ +name: CI + +on: + pull_request: + push: + branches: + - main + +jobs: + build: + runs-on: ubuntu-latest + timeout-minutes: 10 + + steps: + - name: Checkout + uses: actions/checkout@v4 + + - name: Setup Bun + uses: oven-sh/setup-bun@v2 + with: + bun-version: 1.3.9 + + - name: Restore Next.js cache + uses: actions/cache@v4 + with: + path: .next/cache + key: ${{ runner.os }}-nextjs-${{ hashFiles('bun.lock', 'package.json') }}-${{ hashFiles('pages/**/*', 'components/**/*', 'lib/**/*', 'data/**/*', 'styles/**/*', 'content/**/*', 'public/**/*', 'next.config.js', 'postcss.config.js', 'tailwind.config.js') }} + restore-keys: | + ${{ runner.os }}-nextjs-${{ hashFiles('bun.lock', 'package.json') }}- + + - name: Install dependencies + run: bun install --frozen-lockfile + + - name: Build site + run: bun run build From e77b63554a1a334463733845407fb08ff896df7b Mon Sep 17 00:00:00 2001 From: "Thomas Marchand (agent)" Date: Thu, 9 Apr 2026 09:08:14 +0200 Subject: [PATCH 04/13] Pin GitHub Actions to Node 24 runtime --- .github/workflows/ci.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index bfdf348..1717781 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -6,6 +6,9 @@ on: branches: - main +env: + FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: true + jobs: build: runs-on: ubuntu-latest From 5a6392ded37311d7a048b354e46cce7d0a4325a7 Mon Sep 17 00:00:00 2001 From: "Thomas Marchand (agent)" Date: Thu, 9 Apr 2026 09:09:36 +0200 Subject: [PATCH 05/13] Update GitHub Actions to current major versions --- .github/workflows/ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1717781..2b90f6d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -16,7 +16,7 @@ jobs: steps: - name: Checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 - name: Setup Bun uses: oven-sh/setup-bun@v2 @@ -24,7 +24,7 @@ jobs: bun-version: 1.3.9 - name: Restore Next.js cache - uses: actions/cache@v4 + uses: actions/cache@v5 with: path: .next/cache key: ${{ runner.os }}-nextjs-${{ hashFiles('bun.lock', 'package.json') }}-${{ hashFiles('pages/**/*', 'components/**/*', 'lib/**/*', 'data/**/*', 'styles/**/*', 'content/**/*', 'public/**/*', 'next.config.js', 'postcss.config.js', 'tailwind.config.js') }} From 0cc0c5a4bb3beb66cb76c8ac6945d9b040790e83 Mon Sep 17 00:00:00 2001 From: "Thomas Marchand (agent)" Date: Thu, 9 Apr 2026 09:17:26 +0200 Subject: [PATCH 06/13] Optimize CI workflow execution --- .github/workflows/ci.yml | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2b90f6d..8836ac9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -2,12 +2,25 @@ name: CI on: pull_request: + paths-ignore: + - 'README.md' + - 'CLAUDE.md' + - 'agent.md' push: branches: - main + paths-ignore: + - 'README.md' + - 'CLAUDE.md' + - 'agent.md' env: FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: true + NEXT_TELEMETRY_DISABLED: 1 + +concurrency: + group: ci-${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true jobs: build: From c9afafb541dd940babc467a1e377eb84ab94bdfc Mon Sep 17 00:00:00 2001 From: Claude Code Date: Thu, 9 Apr 2026 17:38:52 +0200 Subject: [PATCH 07/13] Update Safe research page for expanded OwnerManager benchmark Reflects verity-benchmark PR #18 which extends the Safe case from addOwner-only to all four ownership-mutating functions (setupOwners, addOwner, removeOwner, swapOwner) and three invariant families (inListReachable, ownerListInvariant, acyclicity). Key changes: - Title broadened to "Safe Owner List Invariants" - SafeGuarantee now shows the ownerListInvariant biconditional - "What these invariants cover" lists all three invariant families - "How this was proven" describes all four function models - Added proof status table (1 proven, 11 open benchmark tasks) - Hypotheses updated: added hPrevLink (GS205), hClean (setupOwners), reclassified hAcyclic and hFreshInList as provable properties - Links updated for new Specs.lean line numbers and OpenProofs.lean Co-Authored-By: Claude Opus 4.6 --- components/research/SafeGuarantee.jsx | 6 +- data/research.js | 6 +- pages/research/safe-owner-reachability.jsx | 256 +++++++++++++-------- 3 files changed, 172 insertions(+), 96 deletions(-) diff --git a/components/research/SafeGuarantee.jsx b/components/research/SafeGuarantee.jsx index 554e66f..6267435 100644 --- a/components/research/SafeGuarantee.jsx +++ b/components/research/SafeGuarantee.jsx @@ -53,12 +53,12 @@ export default function SafeGuarantee() { aria-hidden={showEnglish} > 
    -            {'-- for every address in the list'}
+            {'-- membership \u2261 reachability'}
             {'\n'}
             {'next(SENTINEL) \u2260 0  \u2227'}
             {'\n'}
             
-              {'\u2200 key, next(key) \u2260 0 \u2192 reachable(SENTINEL, key)'}
+              {'\u2200 key \u2260 0, next(key) \u2260 0 \u2194 reachable(SENTINEL, key)'}
    @@ -78,7 +78,7 @@ export default function SafeGuarantee() {
    - Safe Owner List Reachability Invariant | Research | LFG Labs + Safe Owner List Invariants | Research | LFG Labs @@ -42,7 +42,7 @@ export default function SafeOwnerReachabilityPage() {

    - Safe Owner List Reachability Invariant + Safe Owner List Invariants

    @@ -61,11 +61,13 @@ export default function SafeOwnerReachabilityPage() { . A sentinel node at address{' '} 0x1 anchors - the list. When an owner is added, it is inserted at the head: + the list. All four ownership-mutating functions are modeled: 

    -              {'SENTINEL \u2192 ownerA \u2192 ownerB \u2192 SENTINEL\n'}
-              {'SENTINEL \u2192 NEW \u2192 ownerA \u2192 ownerB \u2192 SENTINEL'}
+              {'setupOwners  \u2192 build initial list\n'}
+              {'addOwner     \u2192 insert at head\n'}
+              {'removeOwner  \u2192 unlink node\n'}
+              {'swapOwner    \u2192 atomic replacement'}
    @@ -78,32 +80,39 @@ export default function SafeOwnerReachabilityPage() { The Safe is the most widely used multi-signature wallet on Ethereum, securing billions of dollars. Its{' '} OwnerManager{' '} - contract maintains the set of signers as a linked list. If{' '} - addOwnerWithThreshold{' '} - could leave a node unreachable from the sentinel, the owner - would exist in storage but be invisible to the signing logic, - breaking the integrity of the multisig. + contract maintains the set of signers as a linked list. If any + ownership operation could leave a node unreachable from the + sentinel, the owner would exist in storage but be invisible to + the signing logic, breaking the integrity of the multisig.

    - +

    - This proof covers the{' '} - inListReachable{' '} - invariant from Certora's{' '} - OwnerReach.spec: - after{' '} - addOwner{' '} - executes, every node with a non-zero successor in the{' '} - owners mapping - is reachable from SENTINEL by following next-pointers. + Three families of invariants are specified across all four + ownership-mutating functions:

    +
      +
    • + inListReachable{' '} + — every node with a non-zero successor is reachable from + SENTINEL +
      • +
    • + ownerListInvariant{' '} + — membership (non-zero successor) is equivalent to + reachability from SENTINEL (combines{' '} + inListReachable and{' '} + reachableInList) +
      • +
    • + acyclic{' '} + — the linked list has no internal cycles +
      • +

    - It does not cover{' '} - removeOwner,{' '} - swapOwner, or the - initial{' '} - setupOwners{' '} - call. Threshold management is also elided as it does not - affect the owners mapping. + These correspond to invariants from Certora's{' '} + OwnerReach.spec. + Threshold management is elided as it does not affect the + owners mapping.

    @@ -114,20 +123,17 @@ export default function SafeOwnerReachabilityPage() { How this was proven

    - The{' '} - addOwnerWithThreshold{' '} - function performs a head insertion into the linked list. Proving - reachability is preserved requires showing that: the new - owner is reachable (via{' '} - - SENTINEL → owner - - ), and all previously reachable nodes remain reachable through - the updated path ( - - SENTINEL → owner → old head → ... - - ). + Each function mutates the linked list differently:{' '} + addOwner performs + a head insertion,{' '} + removeOwner unlinks + a node,{' '} + swapOwner atomically + replaces one node with another, and{' '} + setupOwners constructs + the initial list. For each, the proof must show that the + invariants are preserved (or established, in the case of{' '} + setupOwners).

    Reachability is expressed using witness chains: a @@ -138,14 +144,15 @@ export default function SafeOwnerReachabilityPage() { list indices, making the proof mechanically checkable.

    - The contract logic was modeled in{' '} + All four functions were modeled in{' '} Verity - . The proof first characterizes the post-state (which - next-pointers changed), then lifts pre-state chains to the - post-state and prepends the new path. A reference proof is - provided in{' '} + . The{' '} + addOwner{' '} + inListReachable{' '} + proof is complete. The remaining 11 theorems are scaffolded + as benchmark tasks for AI agents. Reference proofs are in{' '} Proofs.lean @@ -165,6 +172,58 @@ export default function SafeOwnerReachabilityPage() {

    + +
    +

    + Proof status +

    +
    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    FunctioninListReachableownerListInvariantacyclicity
    setupOwnersopenopenopen
    addOwnerprovenopenopen
    removeOwneropenopenopen
    swapOwneropenopenopen
    +
    +

    + Open theorems are scaffolded with correct type signatures and + available as{' '} + + benchmark tasks + {' '} + for AI proof agents. +

    +
    {/* Hypotheses */} @@ -173,32 +232,20 @@ export default function SafeOwnerReachabilityPage() { Hypotheses

    - The proof uses zero axioms. The theorem requires these - hypotheses, which encode the function's preconditions and - structural assumptions about the linked list: + The proofs use zero axioms. Each theorem requires hypotheses + drawn from the function's preconditions and structural + properties of the linked list. The hypotheses vary by function:

      - The new owner cannot be the zero address. Enforced by the{' '} - require guard - in{' '} - - addOwnerWithThreshold - - . - - - The sentinel address is reserved as the list anchor and - cannot be used as an owner. Adding it would corrupt the list - structure. + The owner cannot be the zero address or the sentinel. These + are enforced by{' '} + require guards + in every ownership-mutating function. The owner must not already be in the list. A zero mapping - value means the address is not yet a node. This prevents - duplicate insertion which would create cycles. + value means the address is not yet a node. Used by{' '} + addOwner and{' '} + swapOwner. + + + The predecessor must correctly point to the target owner. + Used by{' '} + removeOwner{' '} + and{' '} + swapOwner to + verify the caller supplied the right predecessor. - The proof is inductive: it assumes the reachability invariant - holds before{' '} - addOwner and - shows it holds after. The base case (initial setup via{' '} - setupOwners) - is not covered. + The proof is inductive: it assumes the invariant holds before + the function executes and shows it holds after.{' '} + setupOwners{' '} + is the base case and does not require this hypothesis. The linked list does not cycle back to SENTINEL before - reaching its natural end. Without this, lifting pre-state - chains to the post-state would be unsound, because - SENTINEL's next-pointer changes during insertion. + reaching its natural end. Defined as a theorem target + ( + acyclic) + in{' '} + Specs.lean, + paving the way to eliminate it as an assumption once the + acyclicity proofs are complete. Strengthens{' '} hFresh: the - new owner address must not appear anywhere in the existing - chain, not just have a zero mapping value. This ensures that - the owner's next-pointer (which changes during - insertion) does not affect any existing chain. + new address must not appear anywhere in existing chains. + Defined as{' '} + freshInList{' '} + in{' '} + Specs.lean and + intended to be derived from{' '} + acyclic plus + the zero mapping value.
    +

    + setupOwners{' '} + additionally requires a{' '} + hClean{' '} + hypothesis (all storage slots are zero) to ensure no stale + mappings from a prior state. +

    View specs in Lean - View proof in Lean + View proofs in Lean + + + View open theorems

    From 25a1c8812c77d38d6af8ff21cd2f06a503b5a44e Mon Sep 17 00:00:00 2001 From: Claude Code Date: Thu, 9 Apr 2026 17:55:09 +0200 Subject: [PATCH 08/13] Show all three invariants in hero guarantee toggle Display inListReachable, ownerListInvariant, and acyclic as a stacked list with English/formal toggle. Each invariant label links to its definition in Specs.lean. Co-Authored-By: Claude Opus 4.6 --- components/research/SafeGuarantee.jsx | 111 ++++++++++++++++---------- 1 file changed, 68 insertions(+), 43 deletions(-) diff --git a/components/research/SafeGuarantee.jsx b/components/research/SafeGuarantee.jsx index 6267435..0b68dfb 100644 --- a/components/research/SafeGuarantee.jsx +++ b/components/research/SafeGuarantee.jsx @@ -1,6 +1,30 @@ import { useState, useEffect, useRef } from 'react' import { ExternalLinkIcon } from './ExternalLink' +const INVARIANTS = [ + { + english: 'Every owner in the list is reachable from the sentinel.', + formal: '\u2200 key, next(key) \u2260 0 \u2192 reachable(SENTINEL, key)', + link: 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Safe/OwnerManagerReach/Specs.lean#L63-L65', + label: 'inListReachable' + }, + { + english: + 'Being in the list is equivalent to being reachable from the sentinel.', + formal: + '\u2200 key \u2260 0, next(key) \u2260 0 \u2194 reachable(SENTINEL, key)', + link: 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Safe/OwnerManagerReach/Specs.lean#L87-L90', + label: 'ownerListInvariant' + }, + { + english: 'The owner list has no internal cycles.', + formal: + '\u2200 key \u2260 SENTINEL, \u2200 chain, isChain(chain) \u2227 noDups(chain) \u2192 SENTINEL \u2209 chain', + link: 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Safe/OwnerManagerReach/Specs.lean#L118-L124', + label: 'acyclic' + } +] + export default function SafeGuarantee() { const [showEnglish, setShowEnglish] = useState(true) const timerRef = useRef(null) @@ -43,49 +67,50 @@ export default function SafeGuarantee() { {showEnglish ? 'Switch to formal' : 'Switch to English'} -
    -
    - 
    -            {'-- membership \u2261 reachability'}
-            {'\n'}
-            {'next(SENTINEL) \u2260 0  \u2227'}
-            {'\n'}
-            
-              {'\u2200 key \u2260 0, next(key) \u2260 0 \u2194 reachable(SENTINEL, key)'}
-            
-
    -
    -
    -

    - Every owner in the Safe can be reached by walking the list from the sentinel node. -

    -
    -
    - -
    - - View Lean - - +
    + {INVARIANTS.map((inv) => ( +
    +
    +
    + + {inv.label} + + + {inv.formal} + +
    +
    +
    +
    + + {inv.label} + +

    + {inv.english} +

    +
    +
    +
    + ))}
    ) From b2f4b7a8aad0fec33190c39dcd2f2bad576212ab Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 9 Apr 2026 18:34:39 +0200 Subject: [PATCH 09/13] Update Safe research page to reflect full benchmark state - Extract shared Hypothesis component from duplicated code in both research pages (bugbot fix) - Move safe-owner-reachability to top of research list as newest entry (bugbot fix) - Update page content: all 4 functions modeled (setupOwners, addOwner, removeOwner, swapOwner), 6/6 benchmark proofs complete - Update SafeGuarantee to show ownerListInvariant (biconditional) instead of just inListReachable - Add proof status table, stronglyAcyclic hypothesis, and updated hypothesis descriptions (hOwnerInList, hOldNePrev, hStrongAcyclic) - Update page title and metadata to "Safe Owner List Invariants" Co-Authored-By: Claude Opus 4.6 --- data/research.js | 38 +-- pages/research/safe-owner-reachability.jsx | 258 +++++++++++++-------- 2 files changed, 177 insertions(+), 119 deletions(-) diff --git a/data/research.js b/data/research.js index 5210024..106699b 100644 --- a/data/research.js +++ b/data/research.js @@ -1,4 +1,14 @@ export const research = [ + { + slug: 'safe-owner-reachability', + title: 'Safe Owner List Invariants', + subtitle: + 'Formally verified linked list invariants of the Safe smart account.', + description: + 'How we proved reachability and acyclicity across all four ownership-mutating functions in the Safe OwnerManager using Verity and Lean 4.', + date: '2026-04-09', + tag: 'Case study' + }, { slug: 'formalizing-transaction-interpretation', title: 'Formalizing Transaction Interpretation', @@ -29,25 +39,6 @@ export const research = [ date: '2025-07-01', tag: 'Publication' }, - { - slug: 'what-is-a-formal-proof', - title: 'What is a formal proof?', - subtitle: 'A short explanation for non-specialists.', - description: - 'An introduction to formal verification for smart contracts — what it means to prove a contract correct.', - date: '2025-06-01', - tag: 'Explainer' - }, - { - slug: 'safe-owner-reachability', - title: 'Safe Owner List Invariants', - subtitle: - 'Formally verified linked list invariants of the Safe smart account.', - description: - 'Reachability, biconditional membership, and acyclicity invariants for all four ownership-mutating functions of the Safe OwnerManager, modeled in Verity and Lean 4.', - date: '2026-04-09', - tag: 'Case study' - }, { slug: 'lido-vault-solvency', title: 'Lido V3 Vault Solvency Guarantee', @@ -57,5 +48,14 @@ export const research = [ 'How we proved the solvency invariant of Lido V3 StakingVaults using Verity and Lean 4.', date: '2025-06-15', tag: 'Case study' + }, + { + slug: 'what-is-a-formal-proof', + title: 'What is a formal proof?', + subtitle: 'A short explanation for non-specialists.', + description: + 'An introduction to formal verification for smart contracts — what it means to prove a contract correct.', + date: '2025-06-01', + tag: 'Explainer' } ] diff --git a/pages/research/safe-owner-reachability.jsx b/pages/research/safe-owner-reachability.jsx index 62bc941..8b54809 100644 --- a/pages/research/safe-owner-reachability.jsx +++ b/pages/research/safe-owner-reachability.jsx @@ -110,8 +110,10 @@ export default function SafeOwnerReachabilityPage() {

    These correspond to invariants from Certora's{' '} - OwnerReach.spec. - Threshold management is elided as it does not affect the + + OwnerReach.spec + + . Threshold management is elided as it does not affect the owners mapping.

    @@ -123,18 +125,32 @@ export default function SafeOwnerReachabilityPage() { How this was proven

    - Each function mutates the linked list differently:{' '} - addOwner performs - a head insertion,{' '} - removeOwner unlinks - a node,{' '} - swapOwner atomically - replaces one node with another, and{' '} - setupOwners constructs - the initial list. For each, the proof must show that the - invariants are preserved (or established, in the case of{' '} - setupOwners). + All four functions were modeled in{' '} + + Verity + + . 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 +
      • +

    Reachability is expressed using witness chains: a concrete list of addresses where each consecutive pair follows @@ -144,86 +160,103 @@ export default function SafeOwnerReachabilityPage() { list indices, making the proof mechanically checkable.

    - All four functions were modeled in{' '} - - Verity - - . The{' '} - addOwner{' '} - inListReachable{' '} - proof is complete. The remaining 11 theorems are scaffolded - as benchmark tasks for AI agents. Reference proofs are in{' '} + For{' '} + removeOwner{' '} + and{' '} + swapOwner, + the proofs require strong acyclicity{' '} + (antisymmetry of the reachability relation) to show that + excising or replacing a node does not orphan downstream + nodes. This matches Certora's{' '} + reach_invariant{' '} + axiom. +

    +

    + Reference proofs are provided in{' '} Proofs.lean - . -

    -

    - The proof is checked by Lean 4's kernel, a small program - that accepts or rejects proofs deterministically. If the proof - were wrong, it would not compile. + . The proof is checked by Lean 4's kernel, a small + program that accepts or rejects proofs deterministically. If + the proof were wrong, it would not compile.

    {VERIFY_COMMAND}

    - If the build succeeds, the proof is correct.{' '} + If the build succeeds, the proofs are correct.{' '} Source repository

    + -
    -

    - Proof status -

    -
    - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
    FunctioninListReachableownerListInvariantacyclicity
    setupOwnersopenopenopen
    addOwnerprovenopenopen
    removeOwneropenopenopen
    swapOwneropenopenopen
    -
    -

    - Open theorems are scaffolded with correct type signatures and - available as{' '} - - benchmark tasks - {' '} - for AI proof agents. -

    + {/* Proof status */} +
    +

    + Proof status +

    +

    + Six benchmark tasks are defined, all proven. Additional{' '} + ownerListInvariant{' '} + theorems remain open in{' '} + + OpenProofs.lean + + . +

    +
    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    FunctionInvariantStatus
    setupOwnersinListReachableProven
    setupOwnersacyclicProven
    addOwnerinListReachableProven
    addOwneracyclicProven
    removeOwnerinListReachableProven
    swapOwnerinListReachableProven
    +

    + Open tasks (not yet proven):{' '} + ownerListInvariant{' '} + for all four functions, plus{' '} + removeOwner{' '} + and{' '} + swapOwner{' '} + acyclicity. +

    {/* Hypotheses */} @@ -282,33 +315,52 @@ export default function SafeOwnerReachabilityPage() { The linked list does not cycle back to SENTINEL before - reaching its natural end. Defined as a theorem target - ( - acyclic) - in{' '} - Specs.lean, - paving the way to eliminate it as an assumption once the - acyclicity proofs are complete. + reaching its natural end. Proven as a theorem for{' '} + setupOwners{' '} + and{' '} + addOwner. + Used as a hypothesis for{' '} + removeOwner{' '} + and{' '} + swapOwner. + Strong acyclicity: the reachability relation is + antisymmetric. Required by{' '} + removeOwner{' '} + and{' '} + swapOwner{' '} + to ensure that excising or replacing a node doesn't + orphan downstream nodes through non-SENTINEL cycles. + + + The owner being removed must actually be in the list (has a + non-zero successor). Removing a node that isn't in the + list would zero SENTINEL's pointer. Used by{' '} + removeOwner. + + - Strengthens{' '} - hFresh: the - new address must not appear anywhere in existing chains. - Defined as{' '} - freshInList{' '} - in{' '} - Specs.lean and - intended to be derived from{' '} - acyclic plus - the zero mapping value. + In{' '} + swapOwner, + the old owner cannot be its own predecessor. A self-loop + would cause the if-chain in the storage map to zero out the + previous owner's pointer, orphaning the new owner.

    @@ -336,6 +388,12 @@ export default function SafeOwnerReachabilityPage() {

    Learn more

    +

    + + Certora OwnerReach.spec + {' '} + — the original specification this work is based on. +

    Date: Thu, 9 Apr 2026 19:38:04 +0200 Subject: [PATCH 10/13] Remove unused ExternalLinkIcon import from SafeGuarantee The INVARIANTS-based multi-row layout uses plain tags for invariant labels, so ExternalLinkIcon is no longer referenced. Co-Authored-By: Claude Opus 4.6 --- components/research/SafeGuarantee.jsx | 1 - 1 file changed, 1 deletion(-) diff --git a/components/research/SafeGuarantee.jsx b/components/research/SafeGuarantee.jsx index 0b68dfb..2242d20 100644 --- a/components/research/SafeGuarantee.jsx +++ b/components/research/SafeGuarantee.jsx @@ -1,5 +1,4 @@ import { useState, useEffect, useRef } from 'react' -import { ExternalLinkIcon } from './ExternalLink' const INVARIANTS = [ { From d54828473ffa78d6be96b4ff5391c3a9c6387ff9 Mon Sep 17 00:00:00 2001 From: Claude Code Date: Thu, 9 Apr 2026 19:40:46 +0200 Subject: [PATCH 11/13] Add stronglyAcyclic invariant to hero and disclosure Reflects the new stronglyAcyclic definition (antisymmetry of reachability) added in verity-benchmark PR #18, which captures Certora's reach_invariant axiom and is required by removeOwner and swapOwner proofs. Co-Authored-By: Claude Opus 4.6 --- components/research/SafeGuarantee.jsx | 7 +++++++ pages/research/safe-owner-reachability.jsx | 8 ++++++-- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/components/research/SafeGuarantee.jsx b/components/research/SafeGuarantee.jsx index 2242d20..0d889b5 100644 --- a/components/research/SafeGuarantee.jsx +++ b/components/research/SafeGuarantee.jsx @@ -21,6 +21,13 @@ const INVARIANTS = [ '\u2200 key \u2260 SENTINEL, \u2200 chain, isChain(chain) \u2227 noDups(chain) \u2192 SENTINEL \u2209 chain', link: 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Safe/OwnerManagerReach/Specs.lean#L118-L124', label: 'acyclic' + }, + { + english: 'If A reaches B and B reaches A, then A equals B.', + formal: + '\u2200 a b, reachable(a, b) \u2227 reachable(b, a) \u2192 a = b', + link: 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Safe/OwnerManagerReach/Specs.lean#L138-L139', + label: 'stronglyAcyclic' } ] diff --git a/pages/research/safe-owner-reachability.jsx b/pages/research/safe-owner-reachability.jsx index 8b54809..4c5b862 100644 --- a/pages/research/safe-owner-reachability.jsx +++ b/pages/research/safe-owner-reachability.jsx @@ -87,7 +87,7 @@ export default function SafeOwnerReachabilityPage() {

    - Three families of invariants are specified across all four + Four families of invariants are specified across all four ownership-mutating functions:

      @@ -105,7 +105,11 @@ export default function SafeOwnerReachabilityPage() {
    • acyclic{' '} - — the linked list has no internal cycles + — the linked list has no SENTINEL cycles +
      • +
    • + stronglyAcyclic{' '} + — reachability is antisymmetric (no cycles at all)

    From dbcdbf3e8724fd8092a5d2059a95cff9d50334c1 Mon Sep 17 00:00:00 2001 From: Claude Code Date: Thu, 9 Apr 2026 21:01:07 +0200 Subject: [PATCH 12/13] Fix proof status table: 9 of 12 theorems proven The table was showing only 6 benchmark tasks and incorrectly listing removeOwner/swapOwner acyclicity and setupOwners ownerListInvariant as open. Cross-referencing Proofs.lean (0 sorry) shows 9 theorems are proven. Only 3 ownerListInvariant preservation theorems (addOwner, removeOwner, swapOwner) remain open. Switched to a compact function x invariant grid matching the actual proof state. Co-Authored-By: Claude Opus 4.6 --- pages/research/safe-owner-reachability.jsx | 50 ++++++++-------------- 1 file changed, 18 insertions(+), 32 deletions(-) diff --git a/pages/research/safe-owner-reachability.jsx b/pages/research/safe-owner-reachability.jsx index 4c5b862..659c495 100644 --- a/pages/research/safe-owner-reachability.jsx +++ b/pages/research/safe-owner-reachability.jsx @@ -201,9 +201,9 @@ export default function SafeOwnerReachabilityPage() { Proof status

    - Six benchmark tasks are defined, all proven. Additional{' '} + 9 of 12 theorems are proven. The remaining three{' '} ownerListInvariant{' '} - theorems remain open in{' '} + preservation theorems remain open in{' '} OpenProofs.lean @@ -213,54 +213,40 @@ export default function SafeOwnerReachabilityPage() { - - - + + + + - - - - - - - + + + - - - - - - - + + + - - + + + - - + + +
    FunctionInvariantStatusFunctioninListReachableownerListInvariantacyclicity
    setupOwnersinListReachableProven
    setupOwnersacyclicProvenprovenprovenproven
    addOwnerinListReachableProven
    addOwneracyclicProvenprovenopenproven
    removeOwnerinListReachableProvenprovenopenproven
    swapOwnerinListReachableProvenprovenopenproven

    -

    - Open tasks (not yet proven):{' '} - ownerListInvariant{' '} - for all four functions, plus{' '} - removeOwner{' '} - and{' '} - swapOwner{' '} - acyclicity. -

    {/* Hypotheses */} From 33f9da6f4917126ec9edb49752f1d77a1a9049a6 Mon Sep 17 00:00:00 2001 From: Thomas Marchand Date: Fri, 10 Apr 2026 09:43:55 +0100 Subject: [PATCH 13/13] Polish Safe owner reachability research page and hero - SafeGuarantee: English summary wording, formal-only math (no Lean names), centered sizing tuned vs Lido hero - Page: disclosure lists four invariants; prose and links (OwnerManager.sol, Verity Contract.lean); remove em dashes; How this was proven intro ties Verity model to Solidity source Made-with: Cursor --- components/research/SafeGuarantee.jsx | 110 +++++++-------------- pages/research/safe-owner-reachability.jsx | 79 +++++++++------ 2 files changed, 85 insertions(+), 104 deletions(-) diff --git a/components/research/SafeGuarantee.jsx b/components/research/SafeGuarantee.jsx index 0d889b5..b15468b 100644 --- a/components/research/SafeGuarantee.jsx +++ b/components/research/SafeGuarantee.jsx @@ -1,34 +1,9 @@ import { useState, useEffect, useRef } from 'react' -const INVARIANTS = [ - { - english: 'Every owner in the list is reachable from the sentinel.', - formal: '\u2200 key, next(key) \u2260 0 \u2192 reachable(SENTINEL, key)', - link: 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Safe/OwnerManagerReach/Specs.lean#L63-L65', - label: 'inListReachable' - }, - { - english: - 'Being in the list is equivalent to being reachable from the sentinel.', - formal: - '\u2200 key \u2260 0, next(key) \u2260 0 \u2194 reachable(SENTINEL, key)', - link: 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Safe/OwnerManagerReach/Specs.lean#L87-L90', - label: 'ownerListInvariant' - }, - { - english: 'The owner list has no internal cycles.', - formal: - '\u2200 key \u2260 SENTINEL, \u2200 chain, isChain(chain) \u2227 noDups(chain) \u2192 SENTINEL \u2209 chain', - link: 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Safe/OwnerManagerReach/Specs.lean#L118-L124', - label: 'acyclic' - }, - { - english: 'If A reaches B and B reaches A, then A equals B.', - formal: - '\u2200 a b, reachable(a, b) \u2227 reachable(b, a) \u2192 a = b', - link: 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Safe/OwnerManagerReach/Specs.lean#L138-L139', - label: 'stronglyAcyclic' - } +const FORMAL_INVARIANTS = [ + '\u2200 key, next(key) \u2260 0 \u2192 reachable(SENTINEL, key)', + '\u2200 key \u2260 0, next(key) \u2260 0 \u2194 reachable(SENTINEL, key)', + '\u2200 a b, reachable(a, b) \u2227 reachable(b, a) \u2192 a = b' ] export default function SafeGuarantee() { @@ -73,50 +48,41 @@ export default function SafeGuarantee() { {showEnglish ? 'Switch to formal' : 'Switch to English'} -
    - {INVARIANTS.map((inv) => ( -
    -
    -
    - - {inv.label} - - - {inv.formal} - -
    -
    -
    +
    + {FORMAL_INVARIANTS.map((formal, i) => ( + -
    - - {inv.label} - -

    - {inv.english} -

    -
    -
    -
    - ))} + {formal} + + ))} +
    +
    +

    + The owners mapping forms a proper loop-free linked list starting at + a special node called{' '} + + SENTINEL + + , and the owners are exactly the addresses on that list. +

    +
    ) diff --git a/pages/research/safe-owner-reachability.jsx b/pages/research/safe-owner-reachability.jsx index 659c495..ff6cd37 100644 --- a/pages/research/safe-owner-reachability.jsx +++ b/pages/research/safe-owner-reachability.jsx @@ -13,6 +13,12 @@ const VERIFY_COMMAND = `git clone https://github.com/lfglabs-dev/verity-benchmar cd verity-benchmark lake build Benchmark.Cases.Safe.OwnerManagerReach.Compile` +const OWNER_MANAGER_SOL = + 'https://github.com/safe-fndn/safe-smart-account/blob/a2e19c6aa42a45ceec68057f3fa387f169c5b321/contracts/base/OwnerManager.sol' + +const VERITY_OWNER_MANAGER_CONTRACT = + 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Safe/OwnerManagerReach/Contract.lean' + export default function SafeOwnerReachabilityPage() { const otherResearch = getSortedResearch().filter( (r) => r.slug !== 'safe-owner-reachability' @@ -78,38 +84,46 @@ export default function SafeOwnerReachabilityPage() {

    The Safe is the most widely used multi-signature wallet on - Ethereum, securing billions of dollars. Its{' '} - OwnerManager{' '} - contract maintains the set of signers as a linked list. If any - ownership operation could leave a node unreachable from the - sentinel, the owner would exist in storage but be invisible to - the signing logic, breaking the integrity of the multisig. + 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.

    -

    - Four families of invariants are specified across all four - ownership-mutating functions: +

    + The owners mapping forms a proper loop-free linked list + starting at a special node called{' '} + SENTINEL, and + the owners are exactly the addresses on that list. +

    +

    + In Lean, that goal is split into four named properties:

    • - inListReachable{' '} - — every node with a non-zero successor is reachable from + inListReachable + : every node with a non-zero successor is reachable from SENTINEL
    • - ownerListInvariant{' '} - — membership (non-zero successor) is equivalent to + ownerListInvariant + : membership (non-zero successor) is equivalent to reachability from SENTINEL (combines{' '} inListReachable and{' '} reachableInList)
    • - acyclic{' '} - — the linked list has no SENTINEL cycles + acyclic: the + linked list has no SENTINEL cycles
    • - stronglyAcyclic{' '} - — reachability is antisymmetric (no cycles at all) + stronglyAcyclic + : reachability is antisymmetric (no cycles at all)

    @@ -129,30 +143,31 @@ export default function SafeOwnerReachabilityPage() { How this was proven

    - All four functions were modeled in{' '} - - Verity + 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) + 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 + 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 + 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 + swapOwner: atomic replacement. The old owner + is unlinked and the new owner spliced into its position

    @@ -381,8 +396,8 @@ export default function SafeOwnerReachabilityPage() {

    Certora OwnerReach.spec - {' '} - — the original specification this work is based on. + + {', the original specification this work is based on.'}