MDHV

@VitalikButerin opened @EFDevcon with it: we need to be able to trust our operating systems and our hardware — a formally verified OS, open silicon. Here is a piece of that, running today. Eita: an EVM specified in @leanprover Lean 4, with the code that runs emitted from the spec. Open source, MIT. What it is The EVM's semantics are a Lean 4 translation of the Ethereum execution specs (EELS), clause by clause, Frontier to Osaka, with Amsterdam staged, plus the OP Stack and Arc chain rules. The code that runs — the ARM64 and x86-64 interpreter handlers, JIT code, gas formulas, and the effect layer for calls, creates, storage and transaction application — is emitted from that spec, not written by hand; on ARM64 the handlers are proved against the spec at the instruction level. CI fails if the committed generated code differs from what the emitters produce. Not "audited": specified, derived, and checked. Checked against the real chain, every block It re-executes @ethereum mainnet and @circle's @arc mainnet from genesis and follows both live: gas used, logs bloom, receipts and transactions roots, EELS validate_header (base fee included) on every block, and the full state root every 10,000 blocks on Ethereum and at each 32,768-block anchor on Arc. That loop also caught our own mistakes: a missing P-256 precompile in our Base rules, and an SBCL 2.6.0 miscompile that corrupted wide integers in snapshot records. What a replay sees that logs don't • 2 Nov: 8 USDT destroyBlackFunds calls zeroed 2,529,259.73 USDT of blacklisted balances — a DestroyedBlackFunds event, no Transfer. • 27 Oct–2 Nov: 41% of the ERC-20 holder-events we checked were Transfer logs from a token whose storage did not change in that transaction. • One token credits balances in mint() and emits nothing: 23,614 silent balance changes in a week. Live at eita.run, with what is proved, what is checked and what is still trusted spelled out: eita.run/verified It's early. 19 proof obligations are still open and tracked in the repo. It isn't an execution client yet: an Engine API block source is the step that makes it one. The next frontier: hardware The techniques behind Eita — a Lean specification, the implementation derived from it, a continuous check against the real system — matter even more for secure hardware, where a bug is etched into silicon and can't be patched. Lean-specified firmware and RTL on open silicon is where "trust our hardware" gets real, and it's what I'm building now: holodi.io (@beledgerless), together with @maqstik and @sbellem to the future of mobile trusted compute. Credit where it's due: this work was motivated by conversations moths ago with @ilyasergey and his team at &Truth (@andTruthPBC), out of stealth last week. The more of us building this, the sooner verified code becomes the default. I'll be at #Devcon in Mumbai Thursday to Saturday. Happy to talk. @ethereumfndn. Code: github.com/valeryz/eita-evm