In this blog post, we present how we specify and verify the implementation of the ADD instruction of the EVM virtual machine in Rust.
We give a functional specification, meaning that we show the implementation to be equivalent to an idealized version written in the Rocq language. As the Rust code for this instruction involves rather advanced features of Rust, the same techniques could apply to verify a large set of Rust programs.