EquiVM: Foundational refinement proofs for EVM bytecode

EquiVM is a framework that allows proving that a piece of EVM bytecode refines a high-level program, written in a specification language called Stele. This specification provides a human-readable, formal, source-language agnostic view of the bytecode. It can serve in further verification of the contract's behavior or in human audits.

Refinement proofs are intended to be generated by autonomous LLM agents. We are currently evaluating the capabilities of LLMs to provide such refinement proofs autonomously and their cost (see the Examples/ and Benchmarks/ directories). The framework has been designed with this goal in mind.

We have used the framework to prove refinement for several real-world contracts, including MakerDAO's Dss, WETH9, and several OpenZeppelin contracts. Our case studies exercise various versions and options of the solc compiler, including optimizations, and we have proof-of-concept proofs for the Vyper compiler as well.

Status. EquiVM is experimental work under active development. The Stele language, the reasoning library, and the proof interfaces are still evolving, and the example and benchmark proof developments are at varying stages of completion.

Stele

Stele is a small imperative language, inspired by Solidity and designed to be syntactically close to it. However, Stele is just a semantic specification language and is not implemented by any compiler. It serves as a formal high-level, source-language agnostic human-readable view of the bytecode, and can be certified equivalent to it. Stele is parametric in the contract's storage layout, so one can describe bytecode generated by different compilers (or no compiler at all).

Stele specifications are written in Lean with a Solidity-like surface syntax (defined in Stele/Notation.lean). Every contract under Examples/ and Benchmarks/ carries one specification in the file SpecSyntax.lean. For example, for the ERC20 contract, the transfer function is specified as:

function transfer(address «to», uint256 value) external returns (bool) {
  require(balanceOf[msg.sender] >= value, "ERC20: insufficient balance");
  balanceOf[msg.sender] -= value;
  balanceOf[«to»] = (balanceOf[«to»] + value) as uint256;
  emit Transfer(msg.sender, «to», value);
  return true;
}

(«to» escapes a Lean keyword; as uint256 checks the addition's range. The preceding require already guarantees that the sender subtraction cannot underflow.)

EquiVM provides the tools for stating and proving that the bytecode implements the Stele specification. This includes semantics for the EVM, semantic rules for Stele, the formal specification of the ABI, and the refinement relation between Stele and EVM. Furthermore, EquiVM provides a library of compositional lemmas and tactics to help with the proofs.

Refinement

The top-level refinement states that the bytecode faithfully implements the semantics of the Stele specification. The refinement relation is defined in Stele/Refine.lean.

Once refinement is established, one can reason about the bytecode at the Stele level. This alleviates the need to both reason about low-level EVM bytecode and to trust the compiler that produced it.

For a contract <Name>, the certificate is the capstone theorem of its Correct.lean:

theorem <name>ContractCorrect :
    contractRefinement config creationBytecode contract

Every deployment of the creation code is matched by a run of the spec's constructor, and the code it deploys refines the spec run with the immutables that constructor set. For a contract without immutables it is built with contractRefinement.of_constant from a constructor proof returning one runtime bytecode and a runtime equivalence of that bytecode; contracts with immutables use contractRefinement.of_runtime.

Interoperability

One of the technical innovations of Stele is that it gives a formal semantics to a contract interacting with arbitrary EVM bytecode. We achieve this by using an approach inspired by multi-language semantics: the external call boundary is defined in terms of the EVM semantics.

Architecture

• EVM semantics (EVM/) We build on top of the EVMLean semantics, a formal model of the EVM in Lean. The semantics is a port of Nethermind's EVMYulLean to a newer version of Lean with a few other adjustments. The EVM semantics is executable and it passes the official EVM conformance test suite.

• Stele (Stele/) This contains Stele's syntax, semantics, and surface notation. The file Stele/Refine.lean defines the refinement relation between Stele and EVM.

• ABI (ABI/) This contains the formal specification of the EVM ABI, including encoding and decoding of calldata and return data, function signatures, and selectors.

• Reasoning library (Reasoning/) A library of compositional lemmas and tactics to help with the proofs. Among other things, it includes forward symbolic-execution combinators, dispatcher/ABI/storage lemmas, and external-call bridges.

• Examples (Examples/) Contracts (small or large ones) that were proved correct using LLMs in parallel to the development of the reasoning library. The proofs drove the design of the library and its lemmas and tactics. The file Examples/README.md is the per-contract status index.

• Benchmarks (Benchmarks/) Larger case studies of real contracts that were proved correct by LLMs. The file Benchmarks/README.md is the per-contract status index.

• Miscellaneous (Misc/) Miscellaneous files, including the contract template (Misc/Template/) and the agent prompt (Misc/prompt.md).

• Proofs (Proofs/) Proof-of-concept high-level proofs on Stele specifications, e.g. the inductive ERC20 invariant that the total supply equals the sum of all balances.

Building

Install the toolchain pinned in lean-toolchain (easiest via elan), then:

lake exe cache get   # prebuilt Mathlib cache
lake build           # core library
lake build Examples Benchmarks   # the proof developments (large: expect a long build)

Proving a contract correct

To prove a new contract correct, create a new directory following the template in Misc/Template/: the user provides the compiled artifacts and the Stele specification (SpecSyntax.lean); the boilerplate and the proof are the job of the LLM agent, instructed with the prompt in Misc/prompt.md.

The Stele specification is typically pretty close to the Solidity source, though it is not always a verbatim translation of it. LLMs can also be used to draft the Stele specification, or to audit its semantic faithfulness against the bytecode before attempting a proof.

Walkthrough: the ERC20 example

Examples/ERC20/ is a minimal ERC20 token. It contains:

• ERC20.sol — the Solidity source, compiled with solc 0.8.35 (optimizer off).
• Bytecode.lean — the exact compiled bytecode as a Lean byte array, the verified jump-destination table, and the six function-selector theorems.
• Spec.lean / SpecSyntax.lean — the Stele specification, and the same spec in surface syntax, proved definitionally equal.
• Correct.lean — the top-level theorem; per-function proofs live in sibling files (Transfer.lean, Approve.lean, …).

The specification declares the storage layout and one transition per ABI function (transfer is shown in full above):

def contractSyntax : ContractDecl := solidity% contract ERC20 {
  mapping(address => uint256) balanceOf;
  mapping(address => mapping(address => uint256)) allowance;
  uint256 totalSupply;

  constructor(uint256 initialSupply) {
    balanceOf[msg.sender] = initialSupply;
    totalSupply = initialSupply;
    emit Transfer(address(0), msg.sender, initialSupply);
  }

  function transfer(address «to», uint256 value) external returns (bool) { ... }
  function approve(address spender, uint256 value) external returns (bool) { ... }
  function transferFrom(address «from», address «to», uint256 value) external returns (bool) { ... }

  -- The getters generated by Solidity's public storage declarations are explicit in Sol⁻.
  function balanceOf(address owner) external view returns (uint256) { ... }
  function allowance(address owner, address spender) external view returns (uint256) { ... }
  function totalSupply() external view returns (uint256) { ... }
}

The top-level theorem is

theorem erc20Correct : runtimeRefinement erc20Config erc20Bytecode erc20Contract

It quantifies over every initial state: any account map, block environment, calldata, call value, gas, and permission mode (the contract may be entered through STATICCALL), provided the deployed code is erc20Bytecode. For each such state it relates one full execution of the bytecode to one execution of the specification: either the bytecode execution runs out of gas (in which case the specification side is unconstrained), or its result is related to a Stele execution result. Successful executions return the same ABI-encoded values and leave equal account maps. An EVM revert can match .reverted, .noMatch, or .decodingFailed; the latter two cover missing entry points and rejected calldata. An EVM INVALID halt can match .reverted, and a static-mode violation must match .staticViolation. Because the theorem holds for all inputs and gas values, every behavior of the deployed contract is covered by this relation. The companion erc20ContractCorrect bundles this with the constructor equivalence for the creation code. erc20ContractSyntaxCorrect states that same certificate directly against contractSyntax.

Checking the proof can be done with:

lake build Examples.ERC20.Correct Examples.ERC20.SpecSyntax Proofs.ERC20.Bytecode
lake env lean --run Examples/ERC20/SpecTests.lean

and #print axioms ERC20.erc20Correct lists the trusted facts it rests on (see Trusted computing base below).

Trusted computing base

An EquiVM certificate is a Lean theorem checked by the Lean kernel, so the trusted base is small and explicit. Accepting a certificate means trusting:

• The theorem statement. The bytecode literal, the Stele specification, and its declared storage layout are part of the statement. Auditing a certificate means reading them: the specification is what the bytecode is proved to implement.
• The proof checker. The Lean 4 kernel and the three standard axioms of Lean's core library (propext, Classical.choice, Quot.sound), and Lean's compiled evaluator, which native_decide uses to check concrete byte-level facts such as the jump-destination tables.
• The EVM model. The refinement is stated against the EVMLean semantics that follows the EVM Yellow Paper. The model is executable and passes the official EVM conformance test suite, but its faithfulness to the EVM is trusted.
• The refinement relation. Stele/Refine.lean defines what equivalence means. It deliberately does not compare gas consumption, logs and substate, or revert payloads.

Everything else is untrusted: the proof-producing LLM agent, the tactics, the macros, and the elaborator can all be arbitrarily wrong without compromising a certificate, because the kernel re-checks every proof term they produce.

To audit a certificate, build it and inspect its axiom footprint:

lake build <Module>.Correct

#print axioms <Namespace>.<name>ContractCorrect

The footprint must contain nothing beyond the three standard Lean axioms and documented native_decide evaluation facts used for concrete proof obligations, including jump-destination tables. Any unexpected custom axiom, or any sorry, means the certificate does not hold.

Note on AI use

The development of EquiVM is assisted by LLMs. Semantics and related definitions were designed and reviewed by humans. Proofs of equivalence between the Stele specifications and the EVM bytecode, related boilerplate, and the Stele specifications themselves were produced by LLMs.

Paper

A detailed description of the theory and evaluation can be found in the paper Foundational Refinement Proofs for Deployed Bytecode, at The Price of Tokens.

License

MIT © Argot Collective.