Verifereum is an executable formal semantics of the Ethereum Execution Layer’s EVM, mechanised in the HOL4 theorem prover. The semantics runs inside the logic, which is how it is checked against Ethereum’s conformance tests, and it is the foundation for machine-checked proofs about EVM bytecode: theorems about the semantics itself, a program logic for contracts, and compiler verification targeting the EVM. Audits find bugs; proofs rule out whole classes of them, and Ethereum’s small, deterministic programs are a good fit for that.
The semantics targets the live fork, Osaka, and is tested against the 17550 Osaka blockchain tests in the Ethereum Execution Spec Tests (EEST) v21.0.1, in two ways. The checked runner evaluates each test inside the logic, so every result is a theorem; a full run takes about five hours on 16 cores, and the last one passed 17487 of them, 99.6% (checked results). The unchecked runner compiles the same definitions to native code and runs them without proof, which takes about half an hour on CI; it passed 17530, 99.9% (unchecked results). The 43 tests that only the unchecked runner passes time out in the checked one. The 20 tests both fail all involve the EIP-7002 and EIP-7251 request contracts, which the semantics models instead of executing their code, so it can’t follow the tests that modify, break or deploy them (issue #177).
The repository is GPLv3. It contains:
spec/: EVM state
(vfmStateScript.sml), operations
(vfmOperationScript.sml), and execution
(vfmExecutionScript.sml) as a definitional interpreter,
with block and transaction processing.spec/prop/: frame
theorems about what execution can touch, such as
run_call_preserves_storage_outside_accessed_slots in
vfmRunCallScript.sml (a storage slot a call never accesses
is unchanged by it) and run_static_preserves in
vfmStaticCallsScript.sml (a static call changes no account,
transient storage, or deletion); the gas accounting theorems of
vfmDecreasesGasScript.sml; and the preserves
combinators of vfmPreservesScript.sml for proving
invariants of the monadic semantics.prog/vfmProgScript.sml: a
separation-logic model of the EVM, with EVM_SPEC_SEMANTICS
relating specifications to execution traces.examples/: the WETH contract
(wrappedEtherScript.sml), with
deploy_result_correct proving that deploying its bytecode
produces the expected state.util/: RLP, Merkle Patricia tries, the
contract ABI, and the precompiles’ cryptography (secp256k1, secp256r1,
BN254, BLS12-381, Blake2f).tests/, which fetches the EEST
fixtures, runs them through the semantics, and writes the results
table.