Verifereum

Verifereum is an open-source project that uses the HOL4 theorem prover to provide mathematically rigorous correctness verification for Ethereum smart contracts. It builds an executable formal semantics of the EVM in higher-order logic, runs the Ethereum execution specification test suite through a definitional interpreter, and derives frame-style theorems for storage and account preservation. The pain point it addresses is that traditional audits can only find bugs but cannot prove the absence of entire vulnerability classes, leaving security at an empirical level.

Verifereum's positioning is a public research effort that strengthens contract security with mathematical rigor. In the Ethereum Security quadratic-funding round of July 2026, it received community donations and matching funds to update its formal semantics for the Glamsterdam fork and advance Vyper-related verification. By bringing EVM operations, precompiles, and compiler verification into one machine-checkable proof system, it offers high-value contracts a guarantee path beyond manual audits.