Formal Verification of EVM Bytecode

Devconnect Istanbul 2023 · 14 Nov 2023 · 19:18

David Pearce presents an approach to formally verifying EVM bytecode, using mathematical proof techniques to check that deployed smart contract code behaves as intended rather than relying on testing alone. Speaking at Devconnect Istanbul 2023, the talk addresses why bytecode-level verification matters even when contracts are written and audited in Solidity or Vyper, since compiler bugs and optimization passes can introduce discrepancies between source and bytecode. It situates formal verification alongside auditing and fuzzing as part of a layered approach to smart contract security.

Speakers

• David Pearce

Topics

• Security
• Formal Verification

From Devconnect Istanbul 2023, hosted by Ethereum Foundation.