Foundational Refinement Proofs for Deployed Bytecode, at the Price of Tokens

Scientific Impact Assessment

Core Contribution. This paper introduces EqiVM, a Lean-based framework for producing *foundational, machine-checked refinement proofs* between deployed EVM bytecode and high-level specifications, with proofs synthesized by LLM agents. The central problem it addresses is a decades-old tradeoff in relating low-level code to high-level behavior: verified compilers, translation validators, and proof-carrying code each sacrifice at least one of generality, automation, or a small trusted base. EqiVM claims to achieve all three simultaneously *for bytecode of arbitrary provenance* — no source language, compiler, or toolchain cooperation required — by (1) defining an executable EVM semantics and a Solidity-mirroring specification language (Sol−) that commits to no compiler, (2) stating refinement over complete transactions with unknown-code interaction folded into the semantics via a multi-language-style external-call boundary, and (3) delegating the actual proof labor to frontier LLM agents whose output the Lean kernel checks (so the agent need not be trusted). The empirical thesis — "foundational proofs can now be bought at the price of tokens" — is demonstrated by proving 23 real deployed contracts, including most of MakerDAO.

Methodological Rigor. The design is careful and self-aware. Proofs are kernel-checked, and the trusted computing base is explicitly enumerated: the EVM model (conformance-tested at 99.99%), the refinement relation's fidelity, the Lean kernel, an opaque Keccak FFI, per-contract selector facts, and — notably — `native_decide` axioms used for large computations. The authors are commendably honest about these trust compromises and about intentional under-specification (gas, substate, revert payloads not modeled, and vacuous equivalence under gas exhaustion). The external-call boundary construction, where the specification-side and bytecode-side calls instantiate the *same* Θ function so results coincide "by construction," is an elegant and sound way to obtain interoperation without a linking theorem. Weaknesses: cost figures are approximate (subscription rather than metered API), two of the hardest contracts remain incomplete, and one genuine semantic mismatch (dynamic-array byte-count wraparound) required patching the refinement relation with a well-formedness hypothesis — an honest but scope-narrowing move.

Potential Impact. The application domain is high-value: smart contracts control large sums, bytecode is immutable (one proof holds for life), and no verified EVM compiler exists while solc has a documented miscompilation record. A foundational, compiler-independent certificate that transfers auditing scrutiny to a readable specification is directly valuable to the smart-contract security industry (auditors, Certora/hevm-style tooling vendors). Beyond the domain, the paper makes a broader claim likely to resonate across the verification community: that LLM economics invert the traditional cost model, and that *verification frameworks should be re-architected for machine, not human, proof authors*. This meta-point could influence how PL researchers design proof libraries and specification languages going forward.

Timeliness & Relevance. Extremely timely. It sits at the confluence of a genuine methodological wave (agentic proof development, following Ioannidis et al., Paraskevopoulou, Verity, Axon) and a mature applied need (bytecode-level smart-contract verification). It arrives as frontier models cross a capability threshold that makes 76k-line proofs feasible.

Strengths.

Limitations & Gaps.

Other observations. The paper is a system/framework + empirical evaluation hybrid. Its lasting value likely lies as much in the *architectural thesis* (design verification frameworks for LLM proof authors) and the reusable Lean framework as in the specific numbers, which will date quickly as models improve. Reproducibility of the *artifacts* (checkable certificates) is strong even though reproducibility of the *generation process* is weak.

Overall, this is a high-impact, forward-looking paper that plausibly marks an inflection point in how a subfield approaches a long-standing barrier, tempered by dependence on proprietary models and a not-yet-minimal trusted base.