Digging into the EVM Object Format (EOF)

The EVM Object Format (EOF) introduces a structured container format for EVM bytecode. The EOF proposal is spread over several EIPs (see the “Mega EOF Endgame” for an overview). My goal here is to provide a high level overview and, in particular, to clarify what problems it is trying to solve.

Proving a Beautiful Identity in Dafny

Recently, I came across a tweet about the following identity: This seemed quite surprising to me, though the tweet’s thread included a number of proofs. We can check the first few values easily for ourself:

Pattern Matching in Rust's Neverland

Recently, I’ve been working on a tool for manipulating EVM bytecode and assembly language. I wanted to describe low level bytecode and assembly language using the same datatype. At the same time, I wanted some instructions to be allowed only in assembly language but not bytecode (e.

Disassembling EVM Bytecode (the Basics)

Recently, I’ve been looking at how to disassemble (and eventually decompile) bytecode for the Ethereum Virtual Machine (EVM). This is an interesting computer science problem which I’ve been thinking about lately.

Formalising a Simple Virtual Machine

Since starting my new role at ConsenSys, I have become interested in formalising virtual machines. For example, there are already some formalisations of the Ethereum Virtual Machine (e.g. in K, Lem, Coq).