Verifereum is a formal model of the Ethereum Virtual Machine (EVM) in higher-order logic (HOL). The aim of the project is to enable verification of applications that run on Ethereum and other EVM chains, covering smart contracts and decentralised protocols, compilers to/from EVM bytecode, and infrastructure for proof engineering and developing formal specifications. Verifereum is developed using HOL4 (https://hol-theorem-prover.org).