Prove functional correctness of Ethereum smart contracts in higher-order logic.

Verifereum is an open-source project that brings mathematical rigour to Ethereum smart contract verification. Using the HOL4 theorem prover, we're building tools to prove the correctness of smart contracts and eliminate entire classes of vulnerabilities.

• Beyond Traditional Auditing: While audits can find bugs, mathematical verification proves the absence of entire classes of vulnerabilities
• High Stakes, Higher Standards: With billions of dollars secured by smart contracts, formal verification offers the strongest security guarantees possible
• Perfect Fit: Ethereum's deterministic execution model, where code is expensive so applications are small, makes it an ideal candidate for formal verification

• Formal specification of EVM operations in HOL4
• Progress on passing the Ethereum Execution Spec Tests (EEST)
• Work-in-progress verification of WETH contract (see examples/wrappedEtherScript.sml)
• Vyper language semantics and compiler verification underway

verifereum/
├── spec/           # Formal EVM specification
│   ├── vfmExecutionScript.sml    # EVM execution semantics
│   ├── vfmOperationScript.sml    # EVM operations
│   ├── vfmStateScript.sml        # EVM state model
│   └── prop/                     # Properties and proofs about EVM
├── prog/           # Program logic for verification
├── util/           # Utilities (RLP, Merkle Patricia Trie, crypto primitives)
│   ├── recursiveLengthPrefixScript.sml
│   ├── merklePatriciaTrieScript.sml
│   ├── secp256k1Script.sml
│   └── contractABIScript.sml
├── examples/       # Example contract verifications
│   └── wrappedEtherScript.sml    # WETH contract verification
├── tests/          # EVM test suite
├── website/        # Project website source
└── docs/           # Documentation

Verifereum is developed in the HOL4 theorem prover, which is written in Standard ML.

1. Install Poly/ML (you may prefer to use a packaged version if available)

   curl -L https://github.com/polyml/polyml/archive/refs/heads/master.zip | bsdtar -xf -
   cd polyml-master
   ./configure --enable-intinf-as-int
   make -j4
   make install
   cd ..
   rm -r polyml-master

2. Build HOL4

   git clone -b master https://github.com/HOL-Theorem-Prover/HOL
   cd HOL
   poly --script tools/smart-configure.sml
   bin/build

   Add to your .bashrc:

   export HOLDIR=<path-to-HOL>/HOL
   export PATH=$HOLDIR/bin:$PATH

3. Clone and Build Verifereum

   git clone https://github.com/verifereum/verifereum
   cd verifereum
   Holmake

See docs/run-with-docker.md for instructions on running with Docker.

We welcome contributors of all experience levels! See the contributor guide for details on:

• Setting up your development environment
• Current project areas (EVM formalisation, verification experiments, performance improvements)
• Editor integration (Emacs, Vim, VSCode, Kakoune)

Get involved:

• Join us on Zulip (Verifereum channel)
• Check open issues
• Contact Ramana (xrchz)

• HOL Theorem Prover
• Ethereum Execution Specs - Official Python EVM specification
• evm.codes - EVM opcode reference
• Vyper-HOL - Vyper semantics in HOL4

Verifereum is free software, released under the GNU General Public License v3.