Skip to main content

One post tagged with "functional specification"

View All Tags

ยท 5 min read

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.