{"id":"58d76798-4baa-4c86-97e2-4c9ec281592c","arxiv_id":"2607.26306","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"Using EquiVM, LLM agents produced Lean-checked refinement proofs for 23 real-world EVM contracts, certifying bytecode against a Sol− specification at token cost.","lead":"The paper builds EquiVM, a Lean framework that proves deployed Ethereum bytecode refines a high-level specification, and uses commercial LLM agents to generate those machine-checked proofs for real contracts. It reports that dozens of deployed contracts—including most of MakerDAO—were certified at up to roughly 100 million tokens and 100 hours each, suggesting formal verification costs may now be dominated by tokens rather than expert labor.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Existential gas in Sol− external-call rules lets the refinement theorem certify always-revert bytecode; the 23 proofs may not establish intended effects.","rationale":"The reader's weakest assumption centers on specification fidelity and the risk that agents edited specs to fit bytecode. I share that concern, but the more load-bearing issue is internal to the formal statement: because Sol− external-call gas is existentially quantified and R-Exec matches only some specification derivation, the refinement theorem is substantially more permissive than a typical correctness guarantee. The paper is candid about ignoring gas and about the R-OutOfGas case, but it does not draw out that this design lets the specification itself have both success and revert outcomes for the same input whenever an external call is involved. Thus a non-functional always-reverting bytecode could in principle be certified. This does not make the mechanized theorems false — they are precisely stated — but it weakens the practical meaning of the '23 contracts proved end to end' headline and of the conclusion that foundational proofs are now purchasable at token prices. The proposed test would settle whether the vacuity is real for at least one benchmark. Since the reader already issued CONDITIONAL, my read does not change that verdict; it adds a specific formal condition that should be discharged or explicitly disclaimed.","tokens_in":36435,"tokens_out":14875,"duration_ms":148118,"concrete_test":"Pick a completed external-call contract (Cat) and in the Lean development replace its runtime bytecode with a stub that immediately REVERTs on every calldata. Keep the Sol− specification and configuration unchanged and try to prove `runtimeEquiv`. If the proof checks (R-Exec selects the spec's `rev` derivation via a low existential subcall gas; R-NoDispatch handles the rest), the concern lands: the current theorem certifies an always-reverting implementation. Then add a strengthened obligation requiring, for each dispatched input, existence of a non-reverting, non-OOG bytecode run with storage/return matching the spec's success path, and rerun Cat; failure to prove it would confirm the weakness.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 4.2 (Fig. 7) gives Sol−'s external-call rule an existential gas and substate: `∃g A_in. (σ', z, o) = Θ(...)`. For any contract whose transition calls a callee that requires gas, the same input therefore has both a `ret`/`ok` derivation (choose sufficient g) and a `rev` derivation (choose g small enough to make the callee OOG). R-Exec in Fig. 9 only requires the bytecode result to equal *some* derivation R of the Sol− judgment. Hence a bytecode that simply REVERTs on every external-calling transition is refined by a specification written to succeed: the certificate can pick the spec's revert path. This is more serious than the disclosed absence of gas bounds (Sec. 5.2): existential call gas injects spurious failure behaviors into the specification itself. For the 23 claimed end-to-end proofs, the theorem does not establish that any transition with an external call can complete its intended storage/return effect; it establishes only that whatever the bytecode does is some over-approximate spec behavior. The formal result is internally consistent and the paper is transparent, but the headline 'proved end to end' is substantially weaker than a correctness guarantee if this matching is existential.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces EquiVM, a Lean framework for proving that deployed EVM bytecode refines a high-level specification written in Sol−, a Solidity-like language with big-step semantics. The refinement theorem (Fig. 9) is stated against an executable EVM model extending Nethermind's EVMYulLean; the specification language handles external calls by invoking the same EVM message-call function Θ, and a proof library provides reach-invariant combinators for forward symbolic execution. An LLM agent is used to construct proofs, and the paper reports telemetry for exploratory examples and deployed MakerDAO, WETH9, and Nouns contracts. The claimed contribution is the first combination of foundational, replayable, per-artifact refinement proofs for arbitrary bytecode, including interaction with unknown code, at a cost dominated by LLM tokens.","tokens_in":36727,"tokens_out":12165,"duration_ms":117035,"significance":"If the claims are borne out, the paper would demonstrate a genuine shift: per-contract, compiler-independent, machine-checked equivalence certificates for deployed EVM bytecode, with the LLM agent untrusted because the Lean kernel checks the proof. The design of Sol−, especially the external-call boundary that reuses the EVM's own Θ, is elegant and avoids a linking theorem for unknown callees. The paper is unusually honest about costs, failures, and trusted components (native_decide axioms, opaque Keccak, underspecified gas). However, the headline strength is not supported by the current theorem: the existential gas in external-call rules makes the specification over-approximate to the point that always-revert bytecode refines any external-calling spec, and no artifact is provided to verify the empirical claims. The core idea is promising and the formal development appears substantial, but the main theorem as stated does not deliver the advertised correctness guarantee.","major_comments":[{"comment":"The existential quantification over call gas g in Θ-Call gives every external-calling transition a spurious revert derivation: for any callee, choosing g below the intrinsic call cost makes Θ return z=false, so ExtCallFail allows the specification to revert on any input. Since R-Exec only requires the bytecode result to equal some Sol− derivation, a bytecode that reverts unconditionally on such a transition is refined by a specification that was written to succeed. Thus the end-to-end theorem for contracts with external calls does not establish that those transitions can ever complete their intended effects. Section 5.2's disclosure of underspecified gas is also weaker than this: the problem is not just absence of gas bounds, but that the spec itself contains unconditional failure paths. Please either make gas a tracked component of the Sol− state and force the two sides to use the same","section":"§4.2, Fig. 7 (Θ-Call); §5, Fig. 9 (R-Exec)"},{"comment":"The paper claims replayable machine-checked certificates but provides no artifact: no repository, commit hash, build instructions, or list of Lean files. Tables 1 and 2 report proof line counts and check times, but without the development the reader cannot verify that the proofs exist, that they contain no `sorry`/axioms beyond those disclosed, or that the native_decide-generated axioms are benign. This is a hard requirement for a foundational-verification paper. Please make the full development available and pin the exact versions (Lean, mathlib, EVMYulLean, solc, bytecode hashes).","section":"§6, Tables 1-2; no artifact section"},{"comment":"The abstract and conclusion state that twenty-three real-world contracts were proved end to end, and the conclusion says twenty-seven contracts total. Section 6, however, says 'Nineteen contracts are proved complete at the time of writing, and two more are in progress with partial proofs,' and Table 2 shows Clipper (26/29) and Auction (18/20) incomplete, with 21 deployed contracts listed. The numbers must be reconciled; the current text is self-contradictory and overstates the shipped results.","section":"§1 Abstract and §8 Conclusion vs §6 Evaluation"},{"comment":"The paper states that the semantics were modified from EVMYulLean — changing gas arithmetic, reducing FFI reliance, adding dependent types — but does not report a re-run of the conformance suite. The original model was validated against 99.99% of the Cancun tests; the modified model may no longer conform. Since the refinement theorem is only as good as the EVM model, please report the conformance result for the exact semantics used in the proofs, or list and justify any failing tests.","section":"§3, 'The EVM, Formally'"}],"minor_comments":[{"comment":"Typo: 'A refinement relations s fixes' should be 'A refinement relation fixes'.","section":"§2.2"},{"comment":"'it let's us' should be 'it lets us'.","section":"§4.2"},{"comment":"Typo: 'the the refinement relation' -> 'the refinement relation'.","section":"§5.2"},{"comment":"Inconsistent spelling: the abstract uses 'EquiVM' while the body uses 'EqiVM'. Please standardize.","section":"Throughout"},{"comment":"The Auction row reports Check as '?' (timeout); make this explicit in the caption or as a footnote so it is not confused with a complete check.","section":"Table 2"},{"comment":"The specification-editing incidents (Flipper, Cure, Auction, Clipper) should be highlighted in the main text as a limitation: the certificate only proves that bytecode matches the final edited spec, not that the spec matches original human intent. This is partially disclosed in Appendix C but deserves prominence in Section 6.","section":"§6"}],"recommendation":"major_revision","confidential_remarks":"The external-call existential-gas issue is the most serious technical concern and, if confirmed, weakens the central 'proved end to end' claim. It is fixable, but requires changing the Sol− semantics or the refinement relation, not just the prose. The absence of an artifact is also disqualifying for a foundational-verification paper at this venue. I would be willing to review a revised version with a provided artifact, a strengthened theorem, and corrected counts."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The architecture here is real and worth engaging with. EquiVM is the first post-hoc, per-artifact foundational refinement framework for deployed EVM bytecode of arbitrary provenance, with interoperation with unknown code built into the specification semantics by reusing the EVM's own message-call function Θ. The reach-invariant combinator library is a substantial piece of proof engineering, and the paper is unusually transparent about costs, trusted components, and failures. That transparency is a real point in its favor.\n\nThe main soft spot is the existential gas in the external-call rule (Figure 7). Because the rule quantifies over any gas allowance, a Sol− specification can derive a revert for any transition that performs an external call simply by choosing gas too small for the callee. The refinement theorem (Figure 9) then only requires the bytecode result to equal some derivation of the spec judgment, so bytecode that always reverts on external-calling transitions is certified as refining a specification written to succeed. This is not just a missing gas bound; it injects spurious failure behaviors into the specification itself. For MakerDAO contracts, most interesting functions make external calls, so the claim that these contracts are 'proved end to end' is substantially weaker than a guarantee that the intended effects are achieved. The paper acknowledges the spec is an over-approximation, but it treats this as benign rather than as a load-bearing weakening.\n\nOther soft spots are proportionate but real: no artifact or commit hash is provided, so the 19 completed proofs (Section 6) — not the 23 claimed in the abstract — are not independently checkable; the same agent that proved theorems was authorized to edit specifications in multiple runs, which threatens the independence of the specification; and the post-hoc well-formedness assumption for large dynamic arrays is a retrofit. The modified EVM semantics also lacks a reported conformance re-run. None of these is fatal on its own, but together they mean the paper's central empirical claim is currently unverifiable.\n\nWhat is genuinely good: the formal core is machine-checked in principle, the design of Sol− with the EVM boundary is clever, and the detailed telemetry is a useful contribution to the LLM-for-verification literature. This deserves a serious referee, but the paper needs major revision: ship the artifact, fix the existential-gas issue (or at least state its consequence clearly), align the reported numbers, and rerun conformance on the modified semantics.","headline":"A genuinely new post-hoc foundational refinement framework for arbitrary EVM bytecode whose headline claim overruns the shipped evidence: the external-call rule makes the refinement certificate substantially weaker than 'proved correct', and the reported counts don't match the tables.","tokens_in":37229,"tokens_out":3741,"would_cite":true,"duration_ms":39128,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"LLM agents produce machine-checked refinement proofs for deployed Ethereum bytecode.","keywords":["refinement","EVM","Lean","LLM","translation validation","proof-carrying code","smart contracts","Sol−"],"falsifier":"Recover the original Sol− specification for a contract whose agent was authorized to change it after a mismatch report (e.g., Flipper or Cure), and check whether the deployed bytecode refines that original; if it does not, the theorem only holds for the revised spec. Alternatively, re-run the official EVM conformance suite against the modified semantics and compare the pass rate to the 99.99% reported for the base model.","tokens_in":36242,"feed_emoji":"📜","tokens_out":3977,"duration_ms":35538,"temperature":0.7,"pith_summary":"This paper claims that foundational, machine-checked proofs relating deployed EVM bytecode to a high-level specification are no longer beyond reach: large language model agents can generate them at the price of tokens. The authors build EquiVM, a Lean framework with an executable EVM semantics and the Sol− specification language, and define a refinement relation covering every message call a contract can receive. They report that twenty-three real-world contracts, most of the MakerDAO stablecoin system among them, were proved end to end with minimal human guidance. If correct, each proof is a replayable certificate checked by the Lean kernel, independent of any compiler, and the trusted base shrinks to the semantics, the refinement statement, and a small set of per-contract facts.","feed_headline":"LLM agents verify 23 live Ethereum contracts bytecode-to-spec","feed_subtitle":"Lean-checked certificates cover most of MakerDAO with no compiler trust","key_machinery":"The argument rides on a refinement judgment between the EVM's code-execution function Ξ and a big-step judgment over Sol−, a small imperative specification language whose semantics is parametric in storage layout. Sol− deliberately gives meaning to external calls by invoking the EVM's own message-call function Θ on the live account map, so interaction with unknown bytecode is handled by the semantics rather than by a linking theorem. The proof side is a compositional library built around a reach invariant: a cursor exposing pc, stack, memory, return data, and world, with combinators for forward symbolic execution of the bytecode, so whole-contract proofs reduce to chaining per-opcode lemmas.","core_discovery":"The central claim is the runtime refinement theorem: for any protocol-conforming EVM state, calldata, gas, and substate, executing the deployed bytecode via Ξ either matches a run of the Sol− specification with the same created accounts, account maps up to representation, and return bytes; or reverts when the specification does not dispatch; or exhausts gas. The authors further claim this theorem was discharged by frontier LLM agents for twenty-three deployed contracts at up to a hundred million tokens and a hundred hours per contract, including most of MakerDAO, and conclude that foundational mechanized proofs can now be bought at the price of tokens.","pith_inferences":["The technique inherits the risk that a specification may be edited to match observed bytecode behavior; the paper's own appendix records such authorizations, so the durable guarantee is for the adjusted description, not necessarily the original intent.","Because Sol− models no gas, the refinement theorem allows vacuous equivalence on runs that exhaust gas; a natural extension is to add explicit gas bounds or upper-bound gas proofs.","The same per-artifact certification could transfer to other bytecode platforms with a formal semantics and a high-level spec language, not just the EVM.","A cheap test of the framework's validity is to re-run the official EVM conformance suite against the modified semantics; without that, a silent mismatch between the model and the Cancun EVM would invalidate all certificates."],"forward_implications":["A verified contract comes with a replayable, independently checkable Lean certificate that does not name or rely on the compiler that produced the bytecode.","Auditors and analyzers can work from the Sol− specification rather than decompiled bytecode, for bytecode of any provenance.","Interoperation with arbitrary deployed code is part of the semantics, so compositional reasoning across contract boundaries does not require a linking theorem.","Verification frameworks can be architected around an untrusted LLM proof agent plus a trusted kernel, shifting cost from human labor to tokens."],"fun_headline_variants":["LLM proofs verify 23 Ethereum contracts, including MakerDAO","23 deployed contracts get Lean-checked refinement via LLMs","Agentic LLMs prove EVM bytecode correct for 23 real contracts","Foundational EVM proofs for 23 contracts, at token price","Bytecode-to-spec proven by LLMs on 23 live contracts"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The proof only certifies what the Sol− specification says, so the load-bearing premise is that the specification was written before, not retrofitted after, the bytecode behavior was observed; a second fragile premise is that the modified EVM semantics still faithfully models the Cancun EVM.","fun_headline_variants_meta":{"raw":{"variants":["LLM proofs verify 23 Ethereum contracts, including MakerDAO","23 deployed contracts get Lean-checked refinement via LLMs","Agentic LLMs prove EVM bytecode correct for 23 real contracts","Foundational EVM proofs for 23 contracts, at token price","Bytecode-to-spec proven by LLMs on 23 live contracts"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000211,"raw_usage":{"total_tokens":1298,"prompt_tokens":839,"completion_tokens":459,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":583,"completion_tokens_details":{"reasoning_tokens":368}},"tokens_in":583,"tokens_out":459,"duration_ms":4889,"temperature":1.0,"reasoning_tokens":368,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-01T00:13:10.857720+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Recover the original Sol− specification for a contract whose agent was authorized to change it after a mismatch report (e.g., Flipper or Cure), and check whether the deployed bytecode refines that original; if it does not, the theorem only holds for the revised spec. Alternatively, re-run the official EVM conformance suite against the modified semantics and compare the pass rate to the 99.99% reported for the base model.","supporting_citations":[],"review_version":1}