KEVM writes down what the Ethereum Virtual Machine actually does

A model, not a node, and the difference matters

The repository provides a model of the EVM in K, and the title of the project page is KEVM: Semantics of EVM in K. The primary language is recorded as KCL, the configuration language of the K framework.

It is worth being precise about what that means, because the word emulator invites a wrong assumption. KEVM is not a client, not a node and not something you point at a JSON RPC endpoint. It is a specification that can be executed, and the point of expressing it in K rather than in C++ or Rust is that the same text can be run concretely for a test case and symbolically for a proof.

Two backends of K are available, LLVM for concrete execution and Haskell for symbolic execution, and this repository generates the build products for each backend into a directory named $XDG_CACHE_HOME/evm-semantics-<digest>.

The project has an academic pedigree. The documentation points at the KEVM 1.0 technical report, especially sections 3 and 5, at the KEVM paper at CSF'18/FLoC, at a 20 minute tour of the semantics given at Devcon3 in 2017, at the Jello paper, and at a video on the K, KEVM and Foundry integration.

For an engineer reading the EVM specification today, that list is a map of the argument about what the EVM is, written down.

The semantics are seven files, and each one has a job

The documentation lists the files that constitute the KEVM semantics, and the division is instructive because it mirrors how you would actually think about EVM behaviour.

network.md provides the status codes reported to an Ethereum client on execution exceptions. json-rpc.md is an implementation of JSON RPC in K. evm-types.md provides the functional data of the EVM, the 256-bit words, the word stacks and the rest. serialization.md provides helpers for parsing and unparsing data, hex strings, recursive-length prefix, Merkle trees. evm.md is the main semantics, containing the EVM configuration and the transition rules. gas.md contains all information relevant to gas, and schedule.md all information relevant to EVM schedules.

Two files are the ones you read first. evm.md is where the transition rules live, so it is where the behaviour of each opcode is decided. gas.md is where the cost model lives, which is where the subtle disagreements between clients usually come from. And schedule.md holds the fork-by-fork schedule of which rules apply when, which is the file you need when a behaviour changed at a particular block.

That last split is the part that matters most for the EVM specifically. The EVM is not one machine, it is a series of machines with different rules over time, and any specification that does not model the schedule is describing a machine that never existed.

The extension files exist to make the model usable in proofs

Then there are the files that extend the semantics to make the repository more useful, and they are the part that shows this is a working research tool rather than a paper artefact.

buf.md defines the #buf byte-buffer abstraction for use during symbolic execution. abi.md defines the Contract ABI Specification for use in proofs and easy contract and function specification. hashed-locations.md defines the #hashedLocation abstraction used to specify Solidity-generated storage layouts. edsl.md combines the previous three abstractions for ease of use.

The reason these exist is worth spelling out. A raw EVM model is precise but awkward to write specifications against. The buffer abstraction gives symbolic execution something to reason about instead of raw memory. The ABI definition lets you state a property about a contract function, and the hashed location abstraction lets you state a property about a storage slot that Solidity computed for you, which is otherwise a hash you cannot reason about symbolically.

Without those three, you could still run KEVM on a test case. With them, you can write a specification about a contract. The distinction is the difference between a conformance model and a verification tool.

For testing the semantics itself there are two more files. state-utils.md provides functionality for EVM initialisation, setup and querying, and driver.md is an execution harness providing a simple language for describing tests and programs.

Installing through kup, and the 30 minutes nobody warns you about

The fast installation is a short list of commands, given as a set of bullets. The first is bash <(curl https://kframework.org/install), which installs the kup package manager. Then kup install kevm installs KEVM, kup list kevm lists the available KEVM versions, and kup update kevm updates to the latest KEVM version.

The note under those commands is the important part. The first run will take longer to fetch all the libraries and compile sources, and the estimate given is 30 minutes to an hour. That is a compilation of the K definitions and the toolchain, not a network problem, and it is the single thing that makes people give up on this kind of project before they see it work.

The K framework itself has to be installed, and the documentation gives the version-pinned way to do it through kup, reading the version out of a file in the repository.

kup install k.openssl --version v$(cat deps/k_release)

There is also a single development shell option, which drops you into an environment with the correct version of K on the path.

kup shell k.openssl --version v$(cat deps/k_release)

The pinned version matters. The repository carries a deps/ directory and a flake.nix with a flake.lock, so the K version the semantics were written against is recorded rather than assumed, and reading that file is how you get a build that matches the published results.

Building from source, one layer at a time

Building from source has an order, and the order is not arbitrary. System dependencies come first, and there is an install-build-deps script for the packages the operating system provides, with the documented caveats that the script works on Ubuntu 22.04 and later, and that on Ubuntu older than 18.04 you need to skip libsecp256k1-dev and build it from source with make libsecp256k1. Arch is noted as having no known issues. macOS needs the Command Line Tools, Homebrew and the blockchain plugin, and the documentation recommends the Homebrew version of flex and XCode.

Apple Silicon gets its own note: ensure that your PATH is set up correctly before running make deps or make k-deps, which the documentation says can be done with direnv by copying macos-envrc to .envrc and running direnv allow.

Then Python 3.10 or newer and uv, and you can check your setup by running make. The Makefile picks python3.10 as the interpreter unless k-which-python is on the path, in which case it uses that one.

The build then proceeds in layers. The blockchain plugin submodule has to be fetched and built.

git submodule update --init --recursive
uv --project kevm-pyk run -- kdist --verbose build evm-semantics.plugin

Then the K definitions themselves.

uv --project kevm-pyk run -- kdist --verbose build -j6

Specific targets can be built instead, with the options named as evm-semantics.{llvm,kllvm,kllvm-runtime,haskell,haskell-standalone,plugin}, which is how you avoid building the Haskell backend if you only want to run concrete tests. The compiler can be changed with a CXX environment variable, and APPLE_SILICON=true is passed for Apple hardware.

The conformance suite is the yardstick, and the failing list is public

The Makefile shows how the semantics are tested, and the shape of it is the point.

The top level test target runs test-integration, test-conformance, test-prove and test-interactive, so a full check covers integration, conformance, proofs and interactive use. The conformance target runs the integration tests filtered to test_conformance.py, which is the Ethereum test suite applied to the model.

The most interesting target is conformance-failing-list, and it is worth reading closely because it shows how the project treats its own limits. It clears tests/failing.llvm, reruns the conformance tests with --save-failing and a high --maxfail, sorts the output, and normalises the leading blank line, with a different sed invocation on Darwin. So the repository carries a checked-in list of the conformance tests that the model does not yet pass, sorted and machine readable.

A semantics project that publishes its own failing list is making a specific claim: that the model is a work in progress measured against an external test suite, not a claim of perfect equivalence. Anyone evaluating it can see the gap.

There is a parallel path for the newer execution spec tests. download-json-fixtures removes the fixtures directory and refetches them with a shell script in tests/execution-spec-tests, and test-fixtures runs the integration tests filtered to the execution spec test file and the bchain tests, with its own failing list.

Licence, repository shape and the maintenance picture

The licence is BSD-3-Clause, with the LICENSE file at the root of the repository.

The repository is broader than the EVM files. Besides kevm-pyk/ with the Python package and the kproj semantics directory, there is a deps/ directory for pinned dependencies, an optimizer/ directory, a package/ directory, a scripts/ directory, a tests/ directory with the conformance and execution spec tests, a nix/ directory alongside flake.nix and flake.lock, docs/, web/ and media/. There is also an INSTALL.md, a CLAUDE.md, a funding.json, a _config.yml and a CNAME, which suggests the project also publishes a website.

The release history is dense and machine oriented. The listed releases are v1.0.921 on 2026-06-19, v1.0.920 the same day, and v1.0.919 on 2026-06-18. A version number in the nine hundreds for a semantics project means the model is being regenerated and republished continuously as the K definitions change, not that there are hundreds of user visible features.

The last push was on 2026-10-05 and the repository is not archived.

One documentation gap is worth flagging for anyone starting out. The README links to tests/specs/examples/README.md for how to start proving with KEVM, and that file is where the proof workflow is documented, but the project page itself stops at the beginning of the running tests section, where the text is cut off mid-command.

Editorial conclusion

KEVM fits a protocol engineer, a standards committee or an academic who needs a machine checkable account of EVM behaviour rather than a second implementation to trust, since the transition rules, the gas rules and the schedules are written in one declarative language that can be executed and proved over. It does not fit an application developer who wants to talk to a node, because nothing here is a client, and it does not fit a team without patience for the K toolchain, since the documentation warns the first run takes 30 minutes to an hour. Before adopting it, read the KEVM 1.0 technical report sections 3 and 5 and the 20 minute tour of the semantics, and check the conformance failing list in the repository, because that file is where the model's limits against the Ethereum test suite are visible.

Frequently asked questions

Official sources

1. Issues
2. License: BSD-3-Clause
3. README
4. Releases
5. runtimeverification/evm-semantics on GitHub