Contributing to Verifereum

Verifereum is an executable formal semantics of the Ethereum Virtual Machine in the HOL4 theorem prover, with machine-checked theorems and a program logic built on it. Contributing means writing HOL4 definitions and proofs, or Standard ML for the tooling around them. This page covers getting a build, setting up an editor, and where help is welcome.

Building

Verifereum is built with holbuild, which fetches and builds the pinned HOL4 version for you, so there is no HOL4 to install first; you need Poly/ML and git. The version of holbuild to install is minimum_version in holproject.toml, which also pins HOL4 and the project’s dependencies. Then, in a clone of the repository:

holbuild buildhol          # build the HOL4 toolchain (once)
holbuild -j"$(nproc)" build

The README has the details, and the CI workflow in .github/workflows/ is the exact build to compare against. Running the Ethereum conformance tests is a separate, many-hour job described in tests/README.md.

Editor integration

HOL4 proofs are developed interactively, sending goals and tactics from the editor to a running HOL session. HOL4 ships modes for Emacs, Vim and Kakoune, and there is a separate VS Code extension:

• Emacs: the most complete; see the interaction guide.
• Vim and Neovim: see the README.
• Kakoune: see the README.
• VS Code: hol4-vscode, still experimental.

Ask in the Verifereum channel on the HOL Zulip if setup gives you trouble; different approaches work better on different systems.

Where help is welcome

The open issues are the current to-do list. The broad areas:

• Keeping the semantics current: each Ethereum fork changes the EVM, and the next one, Glamsterdam, is coming. Tracking the execution spec and the test suite releases is ongoing work.
• Conformance test exceptions: the tests that don’t pass yet are timeouts in evaluation inside the logic (the checked runner), and the tests that modify the EIP-7002 and EIP-7251 request contracts, which the semantics models instead of executing (issue #177). Making evaluation faster, or finding why a test is slow, moves the checked pass rate.
• Theorems about the semantics: frame theorems, gas accounting, and invariants of execution, in spec/prop/. Many instructions and cases still lack them.
• Program logic: the separation logic in prog/ provides instruction rules and their connection to execution. Extend the rules and their supporting proofs.
• Faster execution: a proof-producing translation of the semantics to CakeML (issue #14).
• HOL4 itself: Verifereum stresses the prover, and improvements to HOL4’s libraries and evaluation help everyone; its issues are open too.

If you are new to HOL4, start by building the project and stepping through an existing proof in your editor, then pick a small issue and say in Zulip that you are on it.

Getting help

• The Verifereum channel on the HOL Zulip, which is also where the HOL4 community is.
• GitHub issues.
• Ramana (xrchz), who leads the project.