A provably-correct EVM.

• Every one of the first five million Ethereum mainnet blocks, replayed bit-exact. blocks 0 → 5,000,000 · every tx, gas value, and state change matches the canonical chain verified ∎
• Sixteen forks, Frontier through Amsterdam — one Lean specification. EELS-tracked, clause by clause · the executable is generated from the spec verified ∎
• A native ARM64 JIT, emitted from the spec — not hand-written. runs on Apple Silicon & AWS Graviton · machine code you can trace back to a proof 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 ∎

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.