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 Sol⁻ (pronounced Sol minor). 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 Sol⁻ language, the reasoning library, and the proof interfaces are still evolving, and the example and benchmark proof developments are at varying stages of completion.

Sol⁻

Sol⁻ is a small imperative language, inspired by Solidity and designed to be syntactically close to it. However, Sol⁻ 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. Sol⁻ is parametric in the contract's storage layout, so one can describe bytecode generated by different compilers (or no compiler at all).

Sol⁻ specifications are written in Lean with a Solidity-like surface syntax (defined in Solm/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) {
  uint256 fromBalance = balanceOf[msg.sender];
  require(fromBalance >= value);
  balanceOf[msg.sender] = fromBalance - value;
  uint256 toBalance = balanceOf[«to»];
  uint256 newToBalance = (toBalance + value) as uint256;
  balanceOf[«to»] = newToBalance;
  return true;
}

(«to» escapes a Lean keyword; as uint256 is the checked-arithmetic range assertion.)

EquiVM provides the tools for stating and proving that the bytecode implements the Sol⁻ specification. This includes semantics for the EVM, semantic rules for Sol⁻, the formal specification of the ABI, and the refinement relation between Sol⁻ 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 Sol⁻ specification. The refinement relation is defined in Solm/Equiv.lean.

Once refinement is established, one can reason about the bytecode at the Sol⁻ 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 :
    contractEquivalence config creationBytecode runtimeBytecode contract

which bundles the constructor equivalence (creation code) with the runtime equivalence (deployed code).

Interoperability

One of the technical innovations of Sol⁻ 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.

• Sol⁻ (Solm/) This contains Sol⁻'s syntax, semantics, and surface notation. The file Solm/Equiv.lean defines the refinement relation between Sol⁻ 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 Sol⁻ 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 Sol⁻ specification (SpecSyntax.lean); the boilerplate and the proof are the job of the LLM agent, instructed with the prompt in Misc/prompt.md.

The Sol⁻ 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 Sol⁻ 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 selectors (per-contract trusted facts, since Keccak is an opaque foreign constant).
• Spec.lean / SpecSyntax.lean — the Sol⁻ 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;
  }

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

The top-level theorem is

theorem erc20Correct : runtimeEquivalence erc20Config erc20Bytecode erc20Contract

It quantifies over every initial state: any account map, block environment, calldata, call value, and gas, 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 both revert (no function matches the selector, argument decoding fails, or a require fails), or both succeed, returning the same ABI-encoded value and leaving observationally equal storage. Because the theorem holds for all inputs and gas values, every behavior of the deployed contract is covered by the six transitions of the specification above. The companion erc20ContractCorrect bundles this with the constructor equivalence for the creation code.

Checking the proof can be done with:

lake build Examples.ERC20.Correct

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 Sol⁻ 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. Solm/Equiv.lean defines what equivalence means. It deliberately does not compare gas consumption, logs and substate, or revert payloads.
• Keccak facts. Keccak-256 is an opaque foreign function in the model. Each contract therefore trusts a few axioms giving the concrete selector hashes of its ABI signatures (checkable against any Keccak implementation), and contracts that hash at run time additionally trust the library axiom keccak_size (Keccak output is 32 bytes).
• Precompile output bounds (only for contracts with external calls). The precompiles are opaque foreign functions as well; EVMLean states size bounds on their outputs as axioms (Ethereum/Theory/ReturnDataBound.lean), which enter the footprint through the return-data size bound used by the external-call rules.

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 axioms above: the three standard Lean axioms, the native_decide evaluation facts, the contract's Keccak selector facts, and — where applicable — keccak_size and the EVMLean precompile bounds. Any other 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 Sol⁻ specifications and the EVM bytecode, related boilerplate, and the Sol⁻ 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.