Verifereum

Verifereum is a formal model of Ethereum implemented in higher-order logic (#HOL4), aiming to enable the verification of applications and tools within the Ethereum ecosystem (#EVM), from smart contracts to compilers, to prevent hacks and offer the highest assurance of vulnerability-free code possible.