A provably-correct EVM.

• Ethereum mainnet from genesis through the Merge, replayed bit-exact. every block’s gas, logs bloom, receipts and transactions roots match · the full state root every 250,000 blocks · over 170M accounts and 690M storage slots verified ∎
• Sixteen forks, Frontier through Amsterdam — one Lean specification. EELS-tracked, clause by clause · the executable is generated from the spec verified ∎
• The state transition itself — calls, creates, storage, transactions, blocks — derived from Lean. ten effect-layer proofs · gas formulas emitted from the spec · native ARM64 and x86-64 backends verified ∎
• A parallel transaction schedule, proven to produce exactly the state of running the block in order. Block-STM refinement theorem · validation proven necessary · executor derived next verified ∎

Arc mainnet, every block, as it lands.

Eita replays Circle’s Arc chain from genesis and follows it live. Every number on the Arc pages is folded from the fact log that replay writes — USDC supply, holders, fees, protocols and lending — and each window states its block range, the state roots checked in it, and the fact-log shards behind it.

One specification. One streaming engine.

The Lean specification is the only place the EVM’s rules are written. Everything that executes is generated from it, and everything the engine produces is checked against the chain as it runs.

Fast enough to follow the chain — and getting faster.

• DoneThe Merge — block 15,537,394, the first proof-of-stake block.Crossed on 28 October, by the same engine and the same specification.
• DaysThe chain tip, about 26.3 million blocks.Then the replay follows new blocks as they arrive, each checked before it is recorded.
• Next1.2–1.5 Ggas/s, still executing in order.Per-transaction cost fell 57 % this week, from 28.4 to 12.3 µs on our 2018 benchmark; the remaining serial costs are measured and queued.
• ThenParallel execution, from the proof.The Block-STM schedule is already proven equivalent to running the block in order; the executor is derived from that theorem.

As of 28 October 2026.

Vibecoding is fast, but unproven. Put a machine-checked specification between the AI and the code, and you keep the speed — with a proof underneath.

The model writes the implementation; a formal proof in Lean is the gate. The result is correct by construction, not correct by hope. Eita is the existence proof that this works at the scale of a whole EVM — built by one engineer and the verification loop.

When the code moves money, correctness can’t be a hope.

For programmable money, a single execution or accounting bug is a consensus split, a frozen settlement, or a regulatory event. Today that risk is held back by audits and testing — best effort, not proof. Eita turns “trust us” into “here’s the proof”: a verified execution and state engine that indexers, block builders, and searchers can all build on, knowing the state they see is exactly the state the chain produced.