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 / EEST.

Build status: ok passing tests valid license

Authors

rodrigogribeiroλ6cfadb5

Documentation

Tags

License

(Apache-2.0 OR MIT)

Language families

Racket

Last updated

Tuesday, August 18th, 2026 4:27:37pm (UTC)

Ring

Conflicts

None

Dependencies

Build platforms

any platform

Most recent build results

Compiled successfully: transcript
Tests succeeded: transcript

Version Exceptions

Version	Source	Checksum
default	https://github.com/lives-group/evm-redex.git	4ed2fdcb7f2cdc250e35eb1328f52b45c15d1acd

Last checked

Wednesday, August 19th, 2026 4:27:21am (UTC)

Last edited

Tuesday, August 18th, 2026 1:00:50pm (UTC)

Date added

Tuesday, August 18th, 2026 1:00:50pm (UTC)

Modules

evm-redex/tests/equivalence/equivalence.rkt
evm-redex/asm/opcodes.rkt
evm-redex/private/ec.rkt
evm-redex/tests/web3bugs/5-vader-lockunits/props.rkt
evm-redex/private/forks.rkt
evm-redex/sim.rkt
evm-redex/tests/voting/ballot-props.rkt
evm-redex/tests/conformance/runner.rkt
evm-redex/sim/runtime.rkt
evm-redex/scribblings/sim.scrbl
evm-redex/tests/open-zeppelin/properties/ERC20.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/asm.rkt
evm-redex/tests/sim/examples/block.rkt
evm-redex/tests/erc721/erc721-props.rkt
evm-redex/tests/unit/mpt-test.rkt
evm-redex/tests/unit/zero-length-copy-test.rkt
evm-redex/tests/asm/examples/arithmetic.rkt
evm-redex/private/keccak.rkt
evm-redex/tests/unit/forks-test.rkt
evm-redex/pbt/vocab.rkt
evm-redex/sim/engine.rkt
evm-redex/tests/web3bugs/6-beebots-free-mint/props.rkt
evm-redex/private/pairing.rkt
evm-redex/tutorial/explore.rkt
evm-redex/tests/coverage/coverage.rkt
evm-redex/private/state.rkt
evm-redex/private/mem.rkt
evm-redex/private/mpt.rkt
evm-redex/private/fields.rkt
evm-redex/tests/unit/precompiles-test.rkt
evm-redex/sim/state-root.rkt
evm-redex/tests/sim/examples/erc20.rkt
evm-redex/tutorial/counter.rkt
evm-redex/private/native.rkt
evm-redex/tests/asm/examples/calldata.rkt
evm-redex/tests/scribblings/testing.scrbl
evm-redex/private/bls-map-constants.rkt
evm-redex/tests/conformance/blockchain-harness.rkt
evm-redex/tests/unit/sim-test.rkt
evm-redex/tutorial/tutorial-en.scrbl
evm-redex/tutorial/ballot.rkt
evm-redex/private/interpreter.rkt
evm-redex/tests/web3bugs/5-vader-asymmetric-share/props.rkt
evm-redex/tests/open-zeppelin/properties/ERC721.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/tests/web3bugs/5-vader-liquidity-units/props.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/tests/web3bugs/6-beebots-tradevalid/props.rkt
evm-redex/pbt.rkt
evm-redex/scribblings/pbt.scrbl
evm-redex/sim/receipt.rkt
evm-redex/tests/web3bugs/20-spartan-poolshareweight/props.rkt
evm-redex/tests/conformance/blockchain-test.rkt
evm-redex/asm/lang/reader.rkt
evm-redex/tests/pbt/coverage-test.rkt
evm-redex/tests/erc20/erc20-props.rkt
evm-redex/scribblings/asm.scrbl
evm-redex/crypto.rkt
evm-redex/tests/unit/m4-test.rkt
evm-redex/tests/unit/m3-test.rkt
evm-redex/tests/unit/m2-test.rkt
evm-redex/pbt/property.rkt
evm-redex/tests/sim/examples/revert.rkt
evm-redex/tests/open-zeppelin/properties/ERC1155.rkt
evm-redex/private/transaction.rkt
evm-redex/tests/unit/sim-examples-test.rkt
evm-redex/asm/assemble.rkt
evm-redex/private/precompiles.rkt
evm-redex/tests/unit/interp-test.rkt
evm-redex/tests/blind-auction/blind-auction-props.rkt
evm-redex/tests/open-zeppelin/properties/AccessControl.rkt
evm-redex/tests/unit/exec-racket-test.rkt
evm-redex/tutorial/purchase.rkt
evm-redex/tutorial/auction.rkt
evm-redex/tests/web3bugs/5-vether-addexcluded/props.rkt
evm-redex/tests/unit/m13-test.rkt
evm-redex/tests/unit/asm-test.rkt
evm-redex/tests/conformance/conformance-test.rkt
evm-redex/tests/unit/words-test.rkt
evm-redex/sim/lang/reader.rkt
evm-redex/sim/parse.rkt
evm-redex/tests/pbt/equivalence-test.rkt
evm-redex/asm/execute.rkt
evm-redex/pbt/main.rkt
evm-redex/private/hashes.rkt
evm-redex/tests/open-zeppelin/properties/Ownable.rkt
evm-redex/tests/unit/asm-examples-test.rkt
evm-redex/tests/storage/storage-props.rkt
evm-redex/tests/coverage/coverage-demo.rkt
evm-redex/tests/asm/examples/loop.rkt
evm-redex/tests/equivalence/erc20-equivalence.rkt
evm-redex/asm/parse.rkt
evm-redex/tutorial/token.rkt
evm-redex/tests/conformance/harness.rkt
evm-redex/private/gas.rkt
evm-redex/tests/scribblings/pbt-tutorial.scrbl
evm-redex/tests/pbt/pbt-test.rkt