evm-redex

evm-redex 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. It is derived from ethereum/execution-specs and validated against ethereum/tests.

Build status: ok passing tests valid license

README Download
Authors
Documentation
Tags
License
Language familiesRacket
Last updatedFriday, August 21st, 2026 8:27:28pm (UTC)
Ring1
ConflictsNone
Dependencies
Build platformsany platform
Most recent build results
Version Exceptions
VersionSourceChecksum
defaulthttps://github.com/lives-group/evm-redex.gitee52c0242f34e884d91d5db8e79b5ac23bf4df11
Last checkedSaturday, October 3rd, 2026 9:27:16pm (UTC)
Last editedFriday, August 21st, 2026 5:00:14pm (UTC)
Date addedTuesday, August 18th, 2026 1:00:50pm (UTC)
Modules
  • evm-redex/asm/opcodes.rkt
  • evm-redex/private/ec.rkt
  • evm-redex/private/forks.rkt
  • evm-redex/sim/runtime.rkt
  • evm-redex/scribblings/sim.scrbl
  • evm-redex/sim.rkt
  • evm-redex/pbt/deploy.rkt
  • evm-redex/private/lang.rkt
  • evm-redex/private/words.rkt
  • evm-redex/sim/trace.rkt
  • evm-redex/main.rkt
  • evm-redex/private/keccak.rkt
  • evm-redex/pbt/vocab.rkt
  • evm-redex/sim/engine.rkt
  • evm-redex/private/pairing.rkt
  • evm-redex/private/state.rkt
  • evm-redex/private/mem.rkt
  • evm-redex/private/mpt.rkt
  • evm-redex/private/fields.rkt
  • evm-redex/sim/state-root.rkt
  • evm-redex/tutorial/explore.rkt
  • evm-redex/tutorial/counter.rkt
  • evm-redex/private/native.rkt
  • evm-redex/private/bls-map-constants.rkt
  • evm-redex/tutorial/tutorial-en.scrbl
  • evm-redex/tutorial/ballot.rkt
  • evm-redex/private/interpreter.rkt
  • evm-redex/sim/block.rkt
  • evm-redex/pbt/solc.rkt
  • evm-redex/sim/abi.rkt
  • evm-redex/pbt/execute.rkt
  • evm-redex/private/rlp.rkt
  • evm-redex/asm/runtime.rkt
  • evm-redex/private/bls.rkt
  • evm-redex/scribblings/evm-redex.scrbl
  • evm-redex/tutorial/tutorial-pt.scrbl
  • evm-redex/pbt/gen.rkt
  • evm-redex/pbt.rkt
  • evm-redex/scribblings/pbt.scrbl
  • evm-redex/sim/receipt.rkt
  • evm-redex/asm/lang/reader.rkt
  • evm-redex/scribblings/asm.scrbl
  • evm-redex/crypto.rkt
  • evm-redex/private/transaction.rkt
  • evm-redex/asm/assemble.rkt
  • evm-redex/pbt/property.rkt
  • evm-redex/tutorial/purchase.rkt
  • evm-redex/tutorial/auction.rkt
  • evm-redex/sim/lang/reader.rkt
  • evm-redex/sim/parse.rkt
  • evm-redex/asm/execute.rkt
  • evm-redex/pbt/main.rkt
  • evm-redex/private/gas.rkt
  • evm-redex/asm/parse.rkt
  • evm-redex/tutorial/token.rkt
  • evm-redex/asm.rkt
  • evm-redex/private/precompiles.rkt
  • evm-redex/private/hashes.rkt