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.
Verifereum v1.2.0 targets Osaka and is tested against all 17,441 Osaka blockchain cases in the Ethereum Execution Spec Tests (EEST) v21.0.2.
The checked runner evaluates the semantics inside HOL4: a Passed result is backed by a kernel-checked theorem. The latest full run passed 17,386 cases (99.7%) in 5h22m on 16 cores; 55 cases timed out, with no other failures (checked results). The unchecked runner compiles the same definitions to native code and runs them without producing proofs. It passed all 17,441 cases (100%) in 38 minutes on CI, including every case that timed out in the checked run (unchecked results).
Block processing executes the deployed beacon-roots, block-history, withdrawal-request and consolidation-request contracts. For their canonical bytecode, HOL4 correspondence proofs relate both return bytes and final account state to the high-level models, under documented bounds.
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.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.