From ab7ebdec097d84941b65304b9d8bd003c24469d6 Mon Sep 17 00:00:00 2001 From: "Thomas Marchand (agent)" Date: Fri, 24 Apr 2026 15:40:18 +0200 Subject: [PATCH 1/3] Add ERC-4337 EntryPoint proof case study --- components/research/EntryPointGuarantee.jsx | 85 +++++ data/research.js | 10 + .../research/erc4337-entrypoint-execution.jsx | 359 ++++++++++++++++++ 3 files changed, 454 insertions(+) create mode 100644 components/research/EntryPointGuarantee.jsx create mode 100644 pages/research/erc4337-entrypoint-execution.jsx diff --git a/components/research/EntryPointGuarantee.jsx b/components/research/EntryPointGuarantee.jsx new file mode 100644 index 0000000..a63e114 --- /dev/null +++ b/components/research/EntryPointGuarantee.jsx @@ -0,0 +1,85 @@ +import { useState, useEffect, useRef } from 'react' + +const FORMAL_INVARIANTS = [ + 'execute(i) -> validated(i)', + 'validated(i) -> exactlyOneExecute(i)', + 'execute(i) occurs after validateUserOp(i)' +] + +export default function EntryPointGuarantee() { + 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 ( +
+ + +
+
+ {FORMAL_INVARIANTS.map((formal, i) => ( + + {formal} + + ))} +
+
+

+ EntryPoint executes a user operation exactly once, if and only if + that same operation successfully passed validation. +

+
+
+
+ ) +} diff --git a/data/research.js b/data/research.js index 07d639e..397d7d6 100644 --- a/data/research.js +++ b/data/research.js @@ -1,4 +1,14 @@ export const research = [ + { + slug: 'erc4337-entrypoint-execution', + title: 'ERC-4337 EntryPoint Execution Invariant', + subtitle: + 'Formally verified execution-after-validation guarantees for EntryPoint.', + description: + 'How we proved that ERC-4337 EntryPoint executes each UserOperation exactly once if and only if validation succeeds, using Verity and Lean 4.', + date: '2026-04-24', + tag: 'Case study' + }, { slug: 'midas-feed-growth-safety', title: 'Midas Growth-Aware Feed Safety Guarantees', diff --git a/pages/research/erc4337-entrypoint-execution.jsx b/pages/research/erc4337-entrypoint-execution.jsx new file mode 100644 index 0000000..e67e3fa --- /dev/null +++ b/pages/research/erc4337-entrypoint-execution.jsx @@ -0,0 +1,359 @@ +import Head from 'next/head' +import Link from 'next/link' +import PageLayout from '../../components/PageLayout' +import ResearchCard from '../../components/ResearchCard' +import EntryPointGuarantee from '../../components/research/EntryPointGuarantee' +import Disclosure from '../../components/research/Disclosure' +import CodeBlock from '../../components/research/CodeBlock' +import ExternalLink from '../../components/research/ExternalLink' +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 +git checkout feat/erc4337-entrypoint-invariant +lake build Benchmark.Cases.ERC4337.EntryPointInvariant.Compile` + +const ENTRYPOINT_SOL = + 'https://github.com/eth-infinitism/account-abstraction/blob/v0.9.0/contracts/core/EntryPoint.sol' + +const BENCHMARK_BRANCH = + 'https://github.com/lfglabs-dev/verity-benchmark/blob/feat/erc4337-entrypoint-invariant' + +const VERITY_PR = 'https://github.com/lfglabs-dev/verity/pull/1746' + +export default function ERC4337EntryPointExecutionPage() { + const otherResearch = getSortedResearch().filter( + (r) => r.slug !== 'erc4337-entrypoint-execution' + ) + + return ( + <> + + + ERC-4337 EntryPoint Execution Invariant | Research | LFG Labs + + + + +
+ + +
+

+ ERC-4337 EntryPoint Execution Invariant +

+
+ +
+ +

+ ERC-4337 adds account abstraction without changing Ethereum + consensus. Users submit{' '} + UserOperations, + bundlers collect them, and a singleton{' '} + EntryPoint{' '} + contract validates and executes the bundle onchain. +

+

+ EntryPoint is the trusted router in that flow. For every + operation, it may deploy the account, call account validation, + call paymaster validation, account for gas, execute the account + call, run post-operation accounting, and compensate the bundler. + The security-critical question is simple to say and hard to + prove: did the exact operation that passed validation get + executed exactly once? +

+
+ +
+

+ Why this matters +

+

+ ERC-4337 accounts and paymasters are arbitrary contracts. A proof + cannot assume that they are honest, simple, or even cooperative. + The invariant has to hold across reverts, external calls, + callbacks, gas-sensitive branches, and malicious return data. +

+ +

+ The proof tracks validation and execution as trace events for + each operation index in a call to{' '} + handleOps. +

+
    +
  • + Safety: EntryPoint never executes operation{' '} + i unless + account validation, paymaster validation when present, nonce + checks, and prefund checks for that same operation succeeded. +
    • +
  • + Exactness: a successfully validated + operation produces exactly one account execution attempt, not + zero and not two. +
    • +
  • + Ordering: execution for operation{' '} + i occurs only + after validation for operation{' '} + i. +
    • +
  • + Isolation: validation for one operation does + not authorize execution for a different operation. +
    • +
+

+ This is the main invariant engineers usually mean when they say + EntryPoint should call the account with{' '} + userOp.callData{' '} + if and only if{' '} + validateUserOp{' '} + passed for that same{' '} + UserOperation. +

+ +
+ +
+

+ How this was proven +

+

+ The Verity model follows the Solidity{' '} + EntryPoint.sol{' '} + structure function by function. The model keeps the same major + phases as the production implementation: the validation pass over + the bundle, the transition to execution, the per-operation + execution wrapper, and the post-operation accounting path. +

+
    +
  • + Validation phase: models account creation, + account validation, paymaster validation, signature/time-range + data, nonce checks, prefund checks, and validation failure. +
    • +
  • + External contracts: account, factory, + aggregator, and paymaster calls are modeled as adversarial + oracle-backed calls, so the theorem ranges over all possible + external behaviors admitted by the EVM model. +
    • +
  • + Execution phase: records account execution as + an indexed trace event tied to the same operation data that was + validated. +
    • +
  • + Failure paths: distinguishes validation + failure, execution failure, bundle revert, and post-operation + behavior instead of collapsing them into a single boolean. +
    • +
+

+ The proof is written in Lean 4 over the Verity model. The main + theorem decomposes the English statement into safety, liveness, + exactness, and ordering lemmas, then combines them into the final + biconditional over execution trace counts. +

+

+ The benchmark case lives in{' '} + + Contract.lean + + , with specifications in{' '} + + Specs.lean + {' '} + and proofs in{' '} + + Proofs.lean + + . The required Verity features for faithful external-call and + control-flow modeling are introduced in{' '} + Verity PR 1746. +

+ + {VERIFY_COMMAND} +

+ If the build succeeds, Lean has checked every proof term.{' '} + + Benchmark pull request + +

+ +
+ +
+

+ Proof status +

+

+ The case proves the main EntryPoint execution invariant and + supporting trace properties.{' '} + + Proofs.lean + {' '} + is sorry-free. +

+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
PropertyMeaningStatus
execution_implies_validationno execution without prior validationproven
validation_implies_executionvalidated operations are executedproven
exactly_once_executionone indexed execution event per validated opproven
validation_before_executionexecution occurs after same-op validationproven
operation_isolationone op cannot validate execution for anotherproven
+
+
+ +
+

+ Assumptions +

+

+ The proof does not assume that accounts or paymasters are honest. + Their behavior is universally quantified through the external-call + model. The remaining assumptions are the same engineering + boundary any formal model needs: the audited Solidity source, + Verity's EVM semantics, and the mapping from Solidity events + of interest to trace predicates. +

+
    + + The Verity model follows the v0.9 EntryPoint control flow. The + proof is a statement about that modeled source, not about an + unrelated deployed fork. + + + Calls to arbitrary contracts are not replaced with trusted + booleans. They are modeled through Verity's adversarial + call interface, and the theorem quantifies over those outcomes. + + + The English guarantee is expressed as a theorem about trace + events. The trace records which operation was validated and + which operation was executed, making “same operation” + and “exactly once” explicit. + +
+

+ + View specs in Lean + + + View proofs in Lean + +

+
+ +
+

+ Learn more +

+

+ + ERC-4337 + + {', the account abstraction standard that defines UserOperations and EntryPoint.'} +

+

+ + EntryPoint audits + + {', including OpenZeppelin, Spearbit, and Cantina reviews of the reference implementation.'} +

+

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

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

+ More research +

+
+ {otherResearch.map((r) => ( + + ))} +
+
+ )} +
+ + + ) +} From b2f7e9b4cf580d746880daf36fe61878792f7c86 Mon Sep 17 00:00:00 2001 From: "Thomas Marchand (agent)" Date: Fri, 24 Apr 2026 18:35:54 +0200 Subject: [PATCH 2/3] Clarify ERC4337 proof scope --- components/research/EntryPointGuarantee.jsx | 11 +- data/research.js | 4 +- .../research/erc4337-entrypoint-execution.jsx | 149 ++++++++---------- 3 files changed, 77 insertions(+), 87 deletions(-) diff --git a/components/research/EntryPointGuarantee.jsx b/components/research/EntryPointGuarantee.jsx index a63e114..b85ceb6 100644 --- a/components/research/EntryPointGuarantee.jsx +++ b/components/research/EntryPointGuarantee.jsx @@ -1,9 +1,9 @@ import { useState, useEffect, useRef } from 'react' const FORMAL_INVARIANTS = [ - 'execute(i) -> validated(i)', - 'validated(i) -> exactlyOneExecute(i)', - 'execute(i) occurs after validateUserOp(i)' + 'attemptExecute(i) -> validated(i)', + 'validated(i) -> attemptExecute(i)', + 'handleOps reverts -> no attemptExecute(i)' ] export default function EntryPointGuarantee() { @@ -75,8 +75,9 @@ export default function EntryPointGuarantee() { aria-hidden={!showEnglish} >

- EntryPoint executes a user operation exactly once, if and only if - that same operation successfully passed validation. + In the modeled handleOps control flow, EntryPoint reaches a user + operation's execution path if and only if that same operation + successfully passed validation.

diff --git a/data/research.js b/data/research.js index 397d7d6..c3429e5 100644 --- a/data/research.js +++ b/data/research.js @@ -3,9 +3,9 @@ export const research = [ slug: 'erc4337-entrypoint-execution', title: 'ERC-4337 EntryPoint Execution Invariant', subtitle: - 'Formally verified execution-after-validation guarantees for EntryPoint.', + 'Formally verified validation-before-execution control-flow slice for EntryPoint.', description: - 'How we proved that ERC-4337 EntryPoint executes each UserOperation exactly once if and only if validation succeeds, using Verity and Lean 4.', + 'How we proved that the modeled EntryPoint handleOps execution path is reached exactly when validation succeeds, using Verity and Lean 4.', date: '2026-04-24', tag: 'Case study' }, diff --git a/pages/research/erc4337-entrypoint-execution.jsx b/pages/research/erc4337-entrypoint-execution.jsx index e67e3fa..267302b 100644 --- a/pages/research/erc4337-entrypoint-execution.jsx +++ b/pages/research/erc4337-entrypoint-execution.jsx @@ -35,7 +35,7 @@ export default function ERC4337EntryPointExecutionPage() { @@ -71,8 +71,8 @@ export default function ERC4337EntryPointExecutionPage() { call paymaster validation, account for gas, execute the account call, run post-operation accounting, and compensate the bundler. The security-critical question is simple to say and hard to - prove: did the exact operation that passed validation get - executed exactly once? + prove in full: can an operation reach execution unless that same + operation passed validation?

@@ -81,48 +81,42 @@ export default function ERC4337EntryPointExecutionPage() { Why this matters

- ERC-4337 accounts and paymasters are arbitrary contracts. A proof - cannot assume that they are honest, simple, or even cooperative. - The invariant has to hold across reverts, external calls, - callbacks, gas-sensitive branches, and malicious return data. + ERC-4337 accounts and paymasters are arbitrary contracts. The + full theorem engineers want would quantify over all of that EVM + behavior. This benchmark proves a narrower, useful slice: the + two-loop EntryPoint control flow that gates the operation + execution path on successful validation.

- The proof tracks validation and execution as trace events for - each operation index in a call to{' '} + The proof tracks validation outcomes and execution-path + attempts for each operation index in a call to{' '} handleOps.

  • - Safety: EntryPoint never executes operation{' '} + Safety: EntryPoint never attempts the + execution path for operation{' '} i unless - account validation, paymaster validation when present, nonce - checks, and prefund checks for that same operation succeeded. + validation for that same operation succeeded in the model.
  • - Exactness: a successfully validated - operation produces exactly one account execution attempt, not - zero and not two. + Liveness: when the modeled validation phase + succeeds, every in-bounds operation reaches the execution + path.
  • - Ordering: execution for operation{' '} - i occurs only - after validation for operation{' '} - i. -
    • -
  • - Isolation: validation for one operation does - not authorize execution for a different operation. + Revert behavior: if validation fails and + handleOps{' '} + reverts, no execution-path attempt is recorded.

- This is the main invariant engineers usually mean when they say - EntryPoint should call the account with{' '} - userOp.callData{' '} - if and only if{' '} - validateUserOp{' '} - passed for that same{' '} - UserOperation. + The model records reaching _executeUserOp, + not successful account execution. It intentionally elides the + callData.length > 0{' '} + branch, gas accounting, and arbitrary account/paymaster + internals.

@@ -132,41 +126,38 @@ export default function ERC4337EntryPointExecutionPage() { How this was proven

- The Verity model follows the Solidity{' '} + The Verity model follows the selected Solidity{' '} EntryPoint.sol{' '} - structure function by function. The model keeps the same major - phases as the production implementation: the validation pass over - the bundle, the transition to execution, the per-operation - execution wrapper, and the post-operation accounting path. + control-flow slice. It keeps the validation pass over the bundle + and the transition to the per-operation execution wrapper, while + abstracting data payloads and most accounting details.

  • - Validation phase: models account creation, - account validation, paymaster validation, signature/time-range - data, nonce checks, prefund checks, and validation failure. + Validation phase: models validation as a + universally quantified boolean outcome per operation.
  • - External contracts: account, factory, - aggregator, and paymaster calls are modeled as adversarial - oracle-backed calls, so the theorem ranges over all possible - external behaviors admitted by the EVM model. + Native Verity shape: includes a contract model + using bounded loops, oracle-backed calls, and low-level + try/catch support from Verity PR 1746.
  • - Execution phase: records account execution as - an indexed trace event tied to the same operation data that was - validated. + Execution phase: records whether the modeled + execution path is reached for each operation index.
  • - Failure paths: distinguishes validation - failure, execution failure, bundle revert, and post-operation - behavior instead of collapsing them into a single boolean. + Failure path: preserves the all-or-nothing + validation loop behavior: a validation failure reverts the + modeled batch before execution attempts.

The proof is written in Lean 4 over the Verity model. The main theorem decomposes the English statement into safety, liveness, - exactness, and ordering lemmas, then combines them into the final - biconditional over execution trace counts. + all-validated-on-success, all-executed-on-success, and + no-execution-on-revert lemmas, then combines the first two into + the biconditional.

The benchmark case lives in{' '} @@ -187,8 +178,8 @@ export default function ERC4337EntryPointExecutionPage() { > Proofs.lean - . The required Verity features for faithful external-call and - control-flow modeling are introduced in{' '} + . The required Verity features for this native-loop and low-level + call model are introduced in{' '} Verity PR 1746.

@@ -207,8 +198,8 @@ export default function ERC4337EntryPointExecutionPage() { Proof status

- The case proves the main EntryPoint execution invariant and - supporting trace properties.{' '} + The case proves the selected EntryPoint control-flow invariant + and supporting properties.{' '} @@ -228,27 +219,27 @@ export default function ERC4337EntryPointExecutionPage() { execution_implies_validation - no execution without prior validation + no execution-path attempt without validation proven validation_implies_execution - validated operations are executed + validated operations reach the execution path proven - exactly_once_execution - one indexed execution event per validated op + all_validated_on_success + a successful modeled batch has all validations true proven - validation_before_execution - execution occurs after same-op validation + all_executed_on_success + a successful modeled batch attempts every execution path proven - operation_isolation - one op cannot validate execution for another + no_execution_on_revert + validation failure records no execution attempts proven @@ -261,12 +252,11 @@ export default function ERC4337EntryPointExecutionPage() { Assumptions

- The proof does not assume that accounts or paymasters are honest. - Their behavior is universally quantified through the external-call - model. The remaining assumptions are the same engineering - boundary any formal model needs: the audited Solidity source, - Verity's EVM semantics, and the mapping from Solidity events - of interest to trace predicates. + The proof does not establish full arbitrary account/paymaster EVM + correctness. The remaining assumptions are explicit: the selected + Solidity control-flow slice, Verity's semantics for the modeled + constructs, and the abstraction from concrete calls and calldata + to per-index validation and execution-path outcomes.

    - The Verity model follows the v0.9 EntryPoint control flow. The - proof is a statement about that modeled source, not about an - unrelated deployed fork. + The case is pinned to EntryPoint v0.9.0 and models the + `handleOps` validation loop plus execution loop, not every + helper branch in the contract. - Calls to arbitrary contracts are not replaced with trusted - booleans. They are modeled through Verity's adversarial - call interface, and the theorem quantifies over those outcomes. + The native Verity model uses oracle-backed calls for the + validation and execution-attempt stubs, while the pure proof + quantifies over all validation result lists. - The English guarantee is expressed as a theorem about trace - events. The trace records which operation was validated and - which operation was executed, making “same operation” - and “exactly once” explicit. + The English guarantee is expressed as a theorem about indexed + validation outcomes and execution-path attempts. It does not + claim account-call success or calldata equivalence.

From bbd305b8ae93365181bf9bbd23732259df770fc8 Mon Sep 17 00:00:00 2001 From: "Thomas Marchand (agent)" Date: Fri, 24 Apr 2026 18:43:00 +0200 Subject: [PATCH 3/3] Match formal proof notation style --- components/research/EntryPointGuarantee.jsx | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/components/research/EntryPointGuarantee.jsx b/components/research/EntryPointGuarantee.jsx index b85ceb6..d271f4a 100644 --- a/components/research/EntryPointGuarantee.jsx +++ b/components/research/EntryPointGuarantee.jsx @@ -1,9 +1,9 @@ import { useState, useEffect, useRef } from 'react' const FORMAL_INVARIANTS = [ - 'attemptExecute(i) -> validated(i)', - 'validated(i) -> attemptExecute(i)', - 'handleOps reverts -> no attemptExecute(i)' + 'attemptExecute(i) → validated(i)', + 'validated(i) → attemptExecute(i)', + 'handleOps reverts → no attemptExecute(i)' ] export default function EntryPointGuarantee() {