EquiVM 0.1.0
First release of EquiVM, a Lean 4 framework for formally verifying that
that EVM bytecode is equivalent to a high-level, human-readable specification
written in Sol⁻, a small Solidity-like specification language.
Refinement proofs are produced by autonomous LLM agents; the framework,
semantics, and reasoning library are designed around that workflow.
What's in this release
- Sol⁻: syntax, semantics, Solidity-like surface notation, and the
refinement relation (Solm/Equiv.lean), including a formal treatment of
external calls to arbitrary EVM bytecode. - Refinement statement: Formal statement of the bytecode refinement.
- EVM Semantics: the repo builds on top of the EVMLean semantics.
- ABI formalization: calldata/returndata encoding and decoding, function
signatures and selectors. - Reasoning library: forward symbolic-execution combinators,
dispatcher/ABI/storage lemmas, and external-call bridges. - 17 completed example proofs (
Examples/), from small hand-written
contracts to Solidity-docs contracts, four OpenZeppelin contracts, and a
Vyper ERC20 (UniswapV2Pairis in progress). - 19 completed benchmark proofs (
Benchmarks/): canonical WETH9 and 18
MakerDAO Dss contracts, proved against the deployed compiler output
(Dss/Clipperis in progress). - 11 prepared scaffolds (
Benchmarks/Scaffolds/): spec, bytecode, and
theorem statements checked in and compiling, proofs pending — including
Safe, Compound Comet, and UniswapV3Pool. - Proof-of-concept property proofs on Sol⁻ specifications (
Proofs/),
e.g. the ERC20 invariant that total supply equals the sum of balances.
Case studies cover solc 0.5.16–0.8.35 with the optimizer both on and off, and
vyper 0.4.3.