evm-redex: An Executable EVM Specification in PLT Redex🔗ℹ

This document describes the library and its public interface. For a quick-start and installation, see the repository "README.md". The tutorial, worked examples, test suites, and conformance corpora live under the package’s "tests/" directory and are documented in The evm-redex test suite: tutorial, tests, and examples.

evm-redex is an executable specification of the Ethereum Virtual Machine, written in PLT Redex and Racket. It models the EVM as a formal small-step semantics — a Redex reduction relation over an explicit machine / world / transaction grammar — and runs that semantics directly against the official Ethereum test vectors (ethereum/tests / EEST), from which it derives its structure alongside ethereum/execution-specs.

The default target hard fork is Prague, and the semantics is multi-fork (Frontier through Prague). The project is designed to be read and tested: every opcode, gas rule, and precompile is an inspectable rewrite rule or metafunction, and conformance is established by computing real post-state roots and log hashes and comparing them against the reference fixtures.

The library’s public interface is three modules: (require evm-redex) — the whole specification (grammar, interpreter, world and transaction machinery, fork gates, precompiles); (require evm-redex/pbt) — the property-based testing DSL, documented in full below; and (require evm-redex/crypto) — the curve and field primitives. Nothing else is public: "private/" is an implementation detail and should never be imported directly.

New here? Start with the step-by-step tutorial that writes, compiles, and tests a small Solidity contract: Tutorial: testing Solidity contracts with evm-redex (English) / Tutorial: testando contratos Solidity com evm-redex (português).

The worked examples and the test suites live under "tests/" and are documented in The evm-redex test suite: tutorial, tests, and examples.

The library also ships two languages: #lang evm-redex/asm, whose source is an EVM program in assembly (#lang evm-redex/asm — writing and running EVM assembly), and #lang evm-redex/sim, a transaction-scenario language that submits transactions against an evolving chain and reports receipts, traces, and a state diff (#lang evm-redex/sim — simulating transactions).