pith. sign in

arxiv: 2606.01794 · v2 · pith:U5CD3NUZnew · submitted 2026-06-01 · 💻 cs.CR · cs.LO· cs.PL

Tridirectional Discriminating-Power Formal Verification of Smart Contract Reentrancy Defense Against Production-Deployed Solidity Source

Ray Iskander This is my paper

Pith reviewed 2026-06-28 14:18 UTC · model grok-4.3

classification 💻 cs.CR cs.LOcs.PL
keywords reentrancysmart contractsformal verificationLean 4OpenZeppelinSolidityEthereumDAO
0
0 comments X

The pith

A machine-checked Lean 4 proof shows the OpenZeppelin reentrancy guard blocks attacks on production Solidity contracts while preserving correct execution.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes the first machine-checked correctness proof of the OpenZeppelin ReentrancyGuard pattern using a Lean 4 state-machine model of actual deployed Solidity source code. It verifies three production contracts plus one mutant through a tridirectional structure that reproduces the DAO attack, proves safe execution on Compound v2, and distinguishes Aave V3 from its vulnerable variant. This matters to anyone relying on the guard in DeFi because reentrancy has already caused over $500M in losses and prior formal work had not covered both attack blocking and non-attack preservation on real source. All thirteen theorems are checked with no sorry statements and only the standard propext axiom.

Core claim

The central claim is that the reentrancy guard has discriminating power: it blocks the DAO 2016 attack pattern, ensures correct non-attacking transactions on Compound v2, and separates the safe Aave V3 flashLoan implementation from a minimal-diff vulnerable mutant, all composed by a meta-theorem under a no-retrofit discipline that is demonstrated in a cross-protocol stress test.

What carries the argument

The Lean 4 state-machine model of production-deployed Solidity source that directly encodes reentrancy behavior and the guard's state transitions.

If this is right

  • The guard blocks reproduction of the DAO 2016 attack pattern in the model.
  • Compound v2 transactions execute correctly without allowing reentrancy.
  • Aave V3 flashLoan is shown safe while its minimal mutant is shown vulnerable.
  • The three directional proofs compose into a single meta-theorem.
  • The same no-retrofit discipline supports a cross-protocol check from Compound v2 to Aave V3.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same modeling approach could be applied to other common smart-contract security patterns beyond reentrancy.
  • Continuous integration of the proofs could be extended to additional production contracts without changing the axiom footprint.
  • If the model construction generalizes, it would allow boundary-case verification for other DeFi protocols using similar flash-loan or lending logic.
  • The tridirectional structure supplies a template for proving both attack prevention and functional preservation on the same code base.

Load-bearing premise

The Lean 4 state-machine model accurately captures reentrancy behavior and the guard's effects for the three contracts and the mutant.

What would settle it

Execution of one of the three contracts or the mutant on the actual Ethereum blockchain that produces a reentrancy exploit the model claims the guard prevents.

read the original abstract

We present the first machine-checked correctness proof of the OpenZeppelin reentrancy-guard pattern against a Lean 4 state-machine model of production-deployed Solidity source. All thirteen theorems are machine-checked with zero sorry, zero user-introduced axioms, and an axiom footprint bounded by [propext] (a standard mathlib4 axiom), gated under continuous integration. Smart contract reentrancy has caused over US$500M in documented losses since 2016, with the DAO 2016 attack draining ~3.6M ETH and forcing the hard fork that split Ethereum. The OpenZeppelin ReentrancyGuard pattern is the de facto defense across production DeFi, yet no prior work has established its discriminating power: that the guard blocks attacks on vulnerable instances, preserves correct execution for non-attacking transactions, and distinguishes adjacent safe and vulnerable variants. Prior efforts formalized either guard correctness on toy contracts or attack feasibility on isolated instances - not both directions plus boundary cases against production source. We verify three production instantiations - DAO 2016, Compound v2, and Aave V3 flashLoan - plus a minimal-diff mutant of Aave V3's flashLoan (flashLoanVulnerable) isolating one security-critical difference, via mutation testing. The tridirectional structure pairs (a) attack reproduction of the DAO 2016 pattern, (b) a correctness proof for Compound v2, and (c) a boundary-case proof distinguishing Aave V3's CEI-correct flashLoan from the mutant. A capstone meta-theorem composes the three under a no-retrofit discipline, demonstrated at the first cross-protocol stress test (Compound v2 to Aave V3); broader-family portability is future work. Full Lean 4 source, CI config and reproduction commands are at https://github.com/rayiskander2406/qanary-contracts, reproducible at v1.6-phase7-closure (substrate: v1.3-layer6-closure).

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The manuscript claims to provide the first machine-checked proof in Lean 4 of the OpenZeppelin ReentrancyGuard's discriminating power (attack blocking, correct execution preservation, and boundary distinction) on three production Solidity contracts (DAO 2016, Compound v2, Aave V3 flashLoan) plus a minimal mutant, via a state-machine model with thirteen theorems proved with zero sorry, zero user axioms beyond propext, and a capstone meta-theorem under no-retrofit discipline.

Significance. If the underlying state-machine model is faithful, the work would be a notable advance by supplying the first bidirectional (attack reproduction plus defense correctness) machine-checked results on real deployed contracts rather than toys, together with mutation-based boundary cases and cross-protocol portability evidence.

major comments (2)
  1. [model-construction section] Model-construction section: the central claim that the thirteen theorems transfer to production-deployed Solidity requires that the Lean 4 state-machine model faithfully reproduces EVM reentrancy call-stack behavior, storage effects, delegatecall semantics, and guard insertion points for the three contracts; no independent cross-check (EVM trace comparison, bytecode equivalence, or alternative semantics) is supplied, leaving the bridge between internal theorems and observable on-chain behavior unverified.
  2. [the three instantiations] Section on the three instantiations and the mutant: the boundary-case theorem distinguishing Aave V3 CEI-correct flashLoan from flashLoanVulnerable and the cross-protocol stress test (Compound v2 to Aave V3) both presuppose that the model accurately isolates the single security-critical difference and preserves reentrancy semantics across protocols; without external validation this distinction remains internal to the model.
minor comments (1)
  1. The GitHub repository link and version tag (v1.6-phase7-closure) are given but the manuscript does not state the exact commit hash or provide a DOI for the artifact, which would aid reproducibility.

Simulated Author's Rebuttal

2 responses · 1 unresolved

We thank the referee for the constructive review and for acknowledging the potential advance if the model is faithful. We respond point-by-point to the major comments on model fidelity and external validation.

read point-by-point responses

  1. Referee: [model-construction section] Model-construction section: the central claim that the thirteen theorems transfer to production-deployed Solidity requires that the Lean 4 state-machine model faithfully reproduces EVM reentrancy call-stack behavior, storage effects, delegatecall semantics, and guard insertion points for the three contracts; no independent cross-check (EVM trace comparison, bytecode equivalence, or alternative semantics) is supplied, leaving the bridge between internal theorems and observable on-chain behavior unverified.

    Authors: The Lean 4 state-machine is constructed by direct embedding of the production Solidity source (DAO 2016, Compound v2, Aave V3 flashLoan) together with the minimal reentrancy-relevant EVM semantics (call stack, storage writes, delegatecall forwarding, and guard predicate insertion points) drawn from the Ethereum yellow paper and the contracts' own source. All thirteen theorems are proved inside this model with zero sorry and only the standard propext axiom. The transfer claim is therefore scoped to the formalized model of the deployed source rather than to raw EVM bytecode execution. We agree that an independent EVM-trace or bytecode-equivalence check would further strengthen the on-chain correspondence; the present work does not supply one. revision: no

  2. Referee: [the three instantiations] Section on the three instantiations and the mutant: the boundary-case theorem distinguishing Aave V3 CEI-correct flashLoan from flashLoanVulnerable and the cross-protocol stress test (Compound v2 to Aave V3) both presuppose that the model accurately isolates the single security-critical difference and preserves reentrancy semantics across protocols; without external validation this distinction remains internal to the model.

    Authors: The boundary-case theorem is obtained by a single-line mutation that removes the reentrancy-guard check from the Aave V3 flashLoan implementation while leaving all other code identical; the model therefore isolates exactly that difference by construction. The cross-protocol meta-theorem composes the Compound v2 correctness result with the Aave V3 model under the explicit no-retrofit discipline stated in the paper. Both results are internal to the parameterized state machine, as the referee observes. revision: no

standing simulated objections not resolved
  • Independent external validation of the state-machine model against live EVM execution traces, bytecode equivalence, or an alternative semantics

Circularity Check

0 steps flagged

No significant circularity; formal proof is self-contained within Lean model

full rationale

The paper presents thirteen machine-checked theorems in Lean 4 with zero sorrys and an axiom footprint limited to propext. The derivation consists of formal proofs inside an explicitly defined state-machine model of Solidity source; the theorems establish attack reproduction, guard correctness, and boundary distinction directly from the model axioms and definitions. No equations reduce to fitted parameters, no predictions are constructed from inputs by renaming, and no load-bearing steps rely on self-citations whose content is unverified. Model fidelity to EVM is an external validation question, not a circularity in the internal derivation chain. The work is self-contained against its stated formal benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the fidelity of the Lean state-machine model to real Solidity execution and on the completeness of the thirteen theorems; the only non-standard element is the standard mathlib4 axiom propext.

axioms (1)
  • standard math propext (propositional extensionality)
    Explicitly stated as the sole axiom used, a standard mathlib4 axiom.

pith-pipeline@v0.9.1-grok · 5911 in / 1314 out tokens · 33690 ms · 2026-06-28T14:18:41.045195+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

13 extracted references

  1. [1]

    Formal verification of smart contracts (short paper),

    K. Bhargavanet al., “Formal verification of smart contracts (short paper),” inProc. ACM Workshop Programming Languages and Anal- ysis for Security (PLAS), 2016

    2016

  2. [2]

    KEVM: A complete formal semantics of the Ethereum Virtual Machine,

    E. Hildenbrandtet al., “KEVM: A complete formal semantics of the Ethereum Virtual Machine,” inProc. IEEE Computer Security Foundations Symp. (CSF), 2018. 16 TABLE 2 Positioning against principal industrial / academic formal verification systems for smart contracts and adjacent verification work. System Verification target Composition support Axiom footpri...

    2018

  3. [3]

    A semantic framework for the security analysis of Ethereum smart contracts,

    I. Grishchenko, M. Maffei, and C. Schneidewind, “A semantic framework for the security analysis of Ethereum smart contracts,” inPrinciples of Security and Trust (POST), LNCS 10804, 2018

    2018

  4. [4]

    Defining the Ethereum Virtual Machine for interactive theorem provers,

    Y. Hirai, “Defining the Ethereum Virtual Machine for interactive theorem provers,” inProc. Financial Cryptography and Data Security (WTSC), 2017

    2017

  5. [5]

    Sereum: Protect- ing existing smart contracts against re-entrancy attacks,

    M. Rodler, W. Li, G. O. Karame, and L. Davi, “Sereum: Protect- ing existing smart contracts against re-entrancy attacks,” inProc. Network and Distributed System Security Symp. (NDSS), 2019

    2019

  6. [6]

    Precise attack synthesis for smart contracts (SmartScopy),

    Y. Feng, E. Torlak, and R. Bod ´ık, “Precise attack synthesis for smart contracts (SmartScopy),” inProc. ACM Conf. Computer and Communications Security (CCS), 2018

    2018

  7. [7]

    Formal verification of a realistic compiler (CompCert),

    X. Leroy, “Formal verification of a realistic compiler (CompCert),” Commun. ACM, vol. 52, no. 7, 2009

    2009

  8. [8]

    Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning,

    R. Junget al., “Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning,” inProc. ACM Principles of Programming Languages (POPL), 2015

    2015

  9. [9]

    Hints on test data selection: Help for the practicing programmer,

    R. A. DeMillo, R. J. Lipton, and F. G. Sayward, “Hints on test data selection: Help for the practicing programmer,”IEEE Computer, vol. 11, no. 4, 1978

    1978

  10. [10]

    An analysis and survey of the develop- ment of mutation testing,

    Y. Jia and M. Harman, “An analysis and survey of the develop- ment of mutation testing,”IEEE Trans. Software Engineering, vol. 37, no. 5, 2011

    2011

  11. [11]

    Baldur: Whole-proof generation and repair with large language models,

    E. First, M. Rabe, T. Ringer, and Y. Brun, “Baldur: Whole-proof generation and repair with large language models,” inProc. ACM ESEC/FSE, 2023

    2023

  12. [12]

    LeanDojo: Theorem proving with retrieval- augmented language models,

    K. Yanget al., “LeanDojo: Theorem proving with retrieval- augmented language models,” inNeurIPS, 2023

    2023

  13. [13]

    An in-context learning agent for formal theorem-proving (COPRA),

    A. Thakur, G. Tsoukalas, Y. Wen, J. Xin, and S. Chaudhuri, “An in-context learning agent for formal theorem-proving (COPRA),” inConf. Language Modeling (COLM), 2024

    2024