What Software Can We Verify Today?, Part 2: Eita

07 Case Study: eita.run

Fifty LeetCode problems show what works in principle. A shipping product shows what holds in practice. Eita, built by Valeriy Zamaraiev, is an Ethereum Virtual Machine specified in Lean 4. The code that runs is emitted from that specification, and every mainnet block is re-executed and checked against the chain. The project site describes it as the work of one engineer and the verification loop.

The EVM is close to a perfect target: economically critical, deterministic, with a detailed executable reference specification and an oracle of more than 26 million real blocks to check against.

08 Spec First, Code Emitted

Eita does not lift Geth or Reth into a prover, so it fits none of the five routes cleanly. It runs the pipeline in the opposite direction. The Ethereum Foundation's Python execution specifications (EELS) are translated clause by clause into Lean, citing the Python by file and line, with every fork from Frontier to Osaka expressed as a delta over its predecessor. Lean emitters then generate the executable parts: ARM64 and x86-64 threaded-interpreter handlers (about 33,500 lines of assembly between them), a per-chunk JIT, and the gas formulas and state-effect layer of a Common Lisp host. The public repository holds roughly 101,000 lines of Lean across specification, emitters, and proofs. The emitted code is not slow: the repository reports a 2.12 Ggas/s median on a Google Cloud VM, 1.22× revm on the same machines and blocks (method and caveats).

Translating the Python spec into Lean is route A applied to a reference specification rather than to a production client. Proving the emitted ARM64 and x86-64 handlers against instruction semantics written in Lean is partly route E. The semantics are deliberately narrow: Eita models only the subset of instructions it needs, rather than pulling in a third-party verified ISA semantics, which Zamaraiev calls “more work with unclear benefit” for the EVM; for RISC-V, where the ecosystem is more active, he expects to reuse one. Taken together it is the older spec-first, extract-the-implementation pattern of CompCert and Fiat-Crypto, rebuilt for the vibe-coding era. The site's pitch says so directly:

The model writes the implementation; a formal proof in Lean is the gate. The aim is software correct by construction, not correct by hope.

09 Proved, Checked, Trusted

Eita's bookkeeping is the useful part. Its verification page sorts every claim into three tiers, which is the discipline this post has been arguing for, and Figure 1 follows that split.

Each tier in Figure 1 rests on a different kind of evidence:

• Proved. The state-effect layer (calls, creates, storage, self-destruct, fee settlement, block rewards) is proved equal to each fork's specification. The internal IR compiler is proved sound against the spec, the emitted gas formulas are proved, and a Block-STM theorem shows that a parallel transaction schedule produces exactly the state of running the block in order. A CI gate checks that the axiom closure of the audited theorems is Lean's standard three (propext, Classical.choice, Quot.sound) and that the committed generated files are byte-identical to what the emitters produce now. That is the axiom gate and the drift gate from the blueprint in Part 3, running in a real repository.
• Checked. This is runtime evidence. On every block, gas used, the logs bloom, and the receipts, transactions, and withdrawals roots are recomputed and compared with the header, and every sender is recovered from its signature. The full state root is recomputed on a schedule, every 10,000 blocks at the Ethereum tip, in a separate process from the snapshot files. On the ethereum/tests blockchain suite, 111,835 of 111,983 tests pass on both the interpreter and the JIT. The remaining 148 are 40 skipped tests and 108 expected failures, each listed with its reason, and nothing else fails.
• Trusted. Stated as plainly: the 256-bit arithmetic helpers and buffer copies in C; the crypto inside the precompiles (blst, OpenSSL, libsecp256k1) as declared oracles with stated contracts, while the precompile wrappers are proved against EELS for any oracle and BLAKE2F is pure Lean; the account tables and frame plumbing still written in Lisp, while the per-account storage slot tables have been Velvet-proved and C-emitted since November 8; the SBCL runtime; the emitters' printers; and above all the faithfulness of the Lean specification to EELS. Eita also does not validate consensus. It has no networking and takes its blocks from a node.

The homepage no longer claims that every fork is verified: its per-fork row now reads "specified · proofs in progress" with a count, and its replay row says "checked, every block" rather than "verified." The repository's generated coverage matrix is the precise record. As of November 10, 2026, 202 of 203 spec-relation theorems are proved across all forks, with no sorry in any relation theorem and no shape placeholders. The one open relation is Amsterdam's code-size rule (EIP-7954), deliberately left open until Amsterdam has a mainnet activation; Eita emits nothing for an unscheduled fork. Seven sorry remain in the whole Lean tree, none in a relation theorem or an executable definition: three trie lemmas and four internal lemmas. The effect-layer proofs cover each fork's specification and are axiom-audited.

The replay and the test suite remain independent evidence that Eita matches Ethereum: they check the implementation against the chain, not against the specification. The old caveat that only Frontier carried proved per-opcode refinements no longer holds; the matrix's "proved" is still textual (no literal sorry), the axiom audit is the separate check, and CI fails if the debt rises.

Eita is not alone on Ethereum. Nethermind's Lean model of the EVM passes all but two of 22,332 Cancun conformance tests, an independent semantics that a project like Eita could be checked against. A 2026 paper by Lazaropoulos and Paraskevopoulou has agents prove that the deployed bytecode of 35 production contracts, including Uniswap's and Compound's, refines a Lean specification without trusting the Solidity compiler: route E on the same platform.

10 Interview: Valeriy Zamaraiev

The Eita section lays out the mechanics. This interview is about the choices behind them. It follows a conversation with Zamaraiev, edited for length and clarity, and starts with the choice of the EVM, what correctness means across clients, and how to tell when a specification is complete.

The through-line is that the specification, not the proof, is the weak link: replay, differential testing, and property tests are what expose its gaps. The conversation then turns to the proved, checked, and trusted ledger, the spec-first pipeline that keeps code and theorems in sync, the agentic optimization loop that turns correctness constraints into performance, and the non-functional requirements a proof cannot capture. It closes with the JIT, Block-STM, and the lessons for a second attempt.

What Is Unique About the System

B.L.: What made you choose the EVM, and what was unique about the system you set out to build?

V.Z.: I had a historical interest because I worked on an AVM implementation before, on a layer-1 the two of us worked on. Then, as chief technology officer of a venture fund, I kept running into cases where I wanted an EVM that was easy to modify: fast calculations in the node's address space, chain replay for indexing, all sorts of archaeology. I imagined it in Lisp because Lisp lets you compile incrementally over current and historical chain state. Paradigm's revm showed how much engineering that takes; AI made it possible, and formal verification made it defensible. By spring 2026 I was the only person in the proof communities I followed who was not using Lean. I had prototypes very soon, by July the system had replayed five million blocks, and now it runs in production on a couple of chains.

I treat correctness as plural. EELS, the Ethereum Foundation's Python execution specs, is the closest thing to a shared definition: rigorous, runnable, and readable. The clients are the other definition, and they do not always agree. Geth and revm disagree on obscure hash-collision cases, and the EIPs themselves can disagree; the cases never happen on chain, so nobody cares. Differential testing against the clients is one check. The chain is another: a cryptographic oracle of what actually happened. Its limit is that what happened is not everything that can happen. Replaying four million blocks does not prove the fifth, and a transaction can still expose a combination nobody has seen. I point to the Nethermind bug that hit a slice of validators as evidence that client diversity matters, and to consensus as a late-stage detection mechanism. For an L2, the sequencer is authoritative; for a ZK rollup, the prover and verifier carry the trust.

How Do You Know the Specification Is Complete?

B.L.: How do you know when a specification is complete enough to build on, and what do you do when it is not?

V.Z.: I do not know the right answer in advance. There is no magic way to produce a correct specification; if there were, I would use it. The practical signal is a bug: when the implementation disagrees with the chain or a test, the question is whether the code is wrong or the specification is underspecified. Testing is the feedback loop that exposes the gap. A specification is not unlike testing, because it quantifies over the domain instead of enumerating examples, but it does not remove the need for tests.

The EVM's 256-bit words make the point concrete. You cannot model arithmetic with unbounded integers; multiplication is bitvector arithmetic over four 64-bit limbs on a 64-bit platform. Proofs use bv_decide and SMT-backed decision procedures, not just omega over naturals. One bug was exactly there. A gap in the proof becomes a gap in the code: if a corner is not specified and not proved, the LLM-generated implementation can look plausible and still be wrong. AI code is impressive until you find the corner cases, and the corner cases do not end.

I did not try to prove every corner. Projects that do end up with millions of lines of Lean; I worked incrementally, area by area, and chose what to trust. The tree stayed under 100,000 lines. A cryptographic implementation used across many blockchains, such as Keccak, is borrowed as an assumption rather than proved from scratch. That is a deliberate trade: the specification is more verbose than the system, and the proof is larger than the code, so the question is always which gap is worth closing.

The EELS-to-Lean translation is the same problem one level up. An LLM given the Python spec and enough context usually gets it right, but the work is iterative: one part is specified, another is specified, and the interaction between them is missed. In one case a test battery failed and the model changed the specification instead of fixing the precondition. That is why I treat mutation testing as necessary: break the system deliberately and see whether the models catch it. Property-based tests found a scalar-multiplication bug in the BLS opcodes that no spec covered. The proof, the regression suite, the multi-client tests, and mainnet replay are not substitutes for one another; they cover different failures. The combination is the thing that works.

Where Does the Trust Come From for the End-Product?

B.L.: Where does the trust in the end product come from, and how do you keep the proved, checked, and trusted tiers honest?

V.Z.: Trust in Eita is a ledger, not a theorem. The verification page splits every claim into proved, checked, and trusted. Proved claims are theorems in Lean; checked claims are re-evaluated at runtime; trusted claims are assumptions with a name. The ledger is public because the useful question is not whether the system is verified, but which parts are verified and what the rest rests on.

The proved tier starts from the specification. Each opcode gets a denotation, then operational semantics, then a refinement into an intermediate representation and the emitted code. The equivalence between operational semantics and denotation is proved; the extracted implementation inherits it. The correspondence between the emitted assembly and the denotation is a smaller but real trust surface: I saw about 200 lines of assembly strings that morning that still have to be eyeballed against their meaning. The same is true of the emitters' printers. We track the axiom closure, and we avoid native_decide because it runs compiled Lean and enlarges the trusted base, which is why Mathlib bans it in some contexts. The proof-debt ledger is the other half: most relation theorems are proved, one Amsterdam rule is open, and a handful of sorrys remain outside relations and executable definitions. The count moves; the debt may fall but not rise.

The checked tier is runtime evidence. On every block, gas used, the logs bloom, and the receipts, transactions, and withdrawals roots are recomputed and compared with the header, and every sender is recovered from its signature. The full state root is recomputed on a schedule, and the ethereum/tests suite and mainnet replay compare the implementation with the chain. These checks are independent of the specification: they catch cases where the code matches its Lean semantics and still disagrees with Ethereum. That is why they sit beside the proof rather than inside it.

The trusted tier is the list that remains: the fidelity of the EELS-to-Lean translation, the C helpers, the cryptography inside the precompiles as declared oracles, the SBCL runtime, the emitters' printers, and consensus, which Eita does not validate. The Lisp account tables and frame plumbing are shrinking as pieces move into proved, C-emitted tables. I would keep the ledger but treat it as a moving frontier: move a claim from trusted to checked where a runtime check can cover it, and from checked to proved where the proof is worth its maintenance cost. The direction is one-way, and the debt is allowed to fall but not rise.

Keeping the Running Code and Theorems Consistent

B.L.: How do you keep the running code and the theorems consistent as the spec changes?

V.Z.: The pipeline runs spec first. The Lean specification is the source; the IR, the ARM64 and x86-64 handlers, the JIT, the Common Lisp host, and the C storage tables are outputs. The proof obligation is that each refinement preserves the denotation. We commit the generated files, and a CI drift gate fails if the committed assembly differs from what the emitters produce now. That is how the running code and the theorems stay in sync as the spec changes: a spec change forces the emitted code and the proof to move together. The drift gate catches the case where they do not.

The host is the instructive exception. It was written in Common Lisp, initially by an LLM and without a specification, because the Lean spec covered the virtual machine and not the chain plumbing. Storage handling, reverts, receipts, and logs were full of bugs. Replay found them, and the response was to specify the missing behavior, fix the code, and let the verified surface catch up. The persistence layer was hand-coded, then brought under the same loop. The in-memory storage tables moved to C, were model-checked with CBMC, and now have a parallel Lean model and a Lean-to-C emitter. For parts that are still not formalized, I treat a parallel Lean spec plus an equivalence check, or model checking, as a valid second-best.

The contrast with other projects is deliberate. Many start with handwritten or LLM-written code and then build a Lean model that relates to it, with the relation checked by hand, property tests, or an extracted IR. Eita goes the other way: the model is the source, and the code is derived. I do not claim that derivation is always the most practical choice. For a system with a lot of unformalized behavior, the traditional model-plus-equivalence approach may be worth adding. What I reject is generating code first and hoping a model can be fitted to it later.

Performance Work With Verification

B.L.: How do verification and performance work together?

V.Z.: Performance is an agentic loop constrained by correctness. About ten days before the conversation Eita was below one Ggas/s; I set a target of two and turned an agent loose to profile, measure, try ideas, reject the ones that did not work, and sweep parameters. I described it to the agent as a constrained search problem: the constraints are the theorems, and within them it can optimize memory, disk layout, cache behavior, and the intermediate representation. Because the code is derived from the specification, an IR change can produce a completely different implementation without invalidating the proofs. Without the formal layer, the same loop would break the system and never converge. With it, the system cannot diverge from a working implementation by construction, even while it tries many designs.

The result is not just a faster interpreter. The proof cost sits in proof search and proof maintenance; the execution path is ordinary native code. The project reports a 2.12 Ggas/s median on a Google Cloud VM, 1.22× revm on the same machines and blocks, at about two cents per teragas on a spot VM. I am careful to call the number a benchmark, not a theorem. The same loop that found the speedup also found the ceiling: the interpreter is small enough to fit in 32 KB of L1 cache, and that is hard to beat.

What Non-Functional Requirements Escape the Spec?

B.L.: What non-functional requirements escape the spec, and how do you handle them?

V.Z.: The proof covers functional behavior under a model. It does not cover disk footprint, machine size, startup time, memory ceiling, tail latency, interfaces, maintainability, or operability. Some resource properties can be proved for objects that are countable in the model; Eita has theorems about resource use, including heap growth, in places. Timing and jitter are harder, and more critical in hardware, where a late signal is an incorrect signal. Most non-functional requirements are empirical, and I treat them as a choice: they can be specified, but the practical move is to pair the proof with a performance budget, a replay gate, and a deployment check. The state transition can be right while the node is too slow to keep up.

The operational numbers are modest but real. Ethereum replay needs about 8 GB of RAM, and the system is designed to run in the cloud as well as on a workstation. The proof does not say that; the benchmark and the deployment do. A proof that ignores the requirements the business actually cares about is a proof of the wrong product.

Does a JIT Make Sense, and How Would You Build One?

B.L.: Does a JIT make sense at this scale, and how would you build one?

V.Z.: Eita ships a per-chunk JIT, but I am skeptical of its payoff at mainnet scale. The JIT has to be correct first; the divergences I have seen came from incomplete specifications or from the emitters' printers, not from the idea of compilation. It is a Lean program running in production: the executor sends bytecode, and the server emits machine code directly. It does not run GCC or Clang on generated assembly. The machine code is modeled with monadic combinators and Lean's do notation, so the encoder is ordinary Lean code with a denotation and properties. The executor compiles chunks selectively for contracts that run repeatedly, caches the results, and falls back to the interpreter.

The cache argument is the interesting one. A 25 KB contract can expand to a megabyte or two of native code; the top hundred contracts can be 200 MB. No L2 or L3 cache is that large, so the code has to come from DRAM, while the interpreter already fits in 32 KB of L1 and finishes a meaningful part of the block before the JIT code arrives. I think cache-aware prefetch and pipelining might add around 20%, and another 20% on top, but that is engineering work with a bounded payoff. The JIT is a performance tier, not a correctness tier, and it should stay optional.

I am blunt about the performance game itself. Block times are twelve seconds, and even a one-second chain would not need most of this for ordinary execution; replay and indexing are where throughput matters. A ten-millisecond chain is a different target, and there the tradeoffs change. Beyond the JIT there are other vectors, and I believe the system can go past two Ggas/s. The question is which metric the application actually needs.

Does Block-STM Win Anything?

B.L.: Does Block-STM win anything in practice?

V.Z.: Block-STM is a latency play, not a bandwidth play. For replay you can parallelize whole blocks, because you already have the history. Parallelizing inside a block matters when you need the effects within milliseconds, and low-latency chains tend to have few transactions per block; one engineering team told me it would not change much for them. The users who benefit are block builders and searchers, who can use the conflict graph to understand the block's structure before executing it. Eita has the theorem that a parallel schedule produces the sequential state, but no implementation. I call it one cloud session away, and low priority except for a MegaETH-style ten-millisecond chain.

What Are the Lessons Learned in the Process?

B.L.: What did you learn, and what would you do differently?

V.Z.: My main lesson is order of work. I would generate much more Lean from day one, as much as I could still understand and afford, and I would not generate code without a specification. Derive it from the spec, or model-check it; do not write it first and fit a model to it later. I compare this to test-driven development: everyone says they will start with tests next time, and for a project with this much specification already in the world, it is worth doing. For a prototype whose purpose is to learn, the tradeoff is different. For Eita, I think it would have saved time.

The bug stories are the evidence for that order. The specification-translation bugs were the instructive ones because the proof could not catch them: the Lean spec was the weak link, and the differential check against the tested Lisp host was what exposed it. Mainnet replay caught the self-destruct-to-self and block-hash edge cases. None of those would have been found by the kernel alone. That is why I would not start anything without Lean, and why I would put the specification and the trust ledger before the code.

I am also clear about scale. The Lean tree is under 100,000 lines, the specification is more verbose than the system it describes, and the proofs are larger than the code. A complete model is north of 100,000 lines; I chose what to trust rather than proving every corner. The Ethereum Foundation's larger verified-EVM effort runs past a million lines of Lean and assumes much less, which makes it a different and harder problem. For code that is already in production and battle-tested, the tradeoff is different again: battle-tested does not mean proven, but the code cannot be rewritten, so the work is to prove what is there and close the gaps going forward.

Eita is in production, though not yet a full EVM client. The distance is small, and the interface to a consensus client is not a huge amount of work; I intend to close it. What it does now is replay and expose hooks: attach a condition, change what is calculated, and run it over current or historical state. That is how I describe the archaeology use case. An index is a lossy compression of the chain, and the gaps between the index and what actually happened are where replay earns its keep: token movements in logs that do not match real balance changes, sandwich attacks inside a block, custom calculations that no explorer exposes. The same system can run in the cloud in batches across many blocks. The requirement is not a data center; replay fits in about 8 GB of RAM.