In this blog post, we show how we state the functional correctness of the implementation of the STATIC_CALL instruction in Revm, an implementation of the Ethereum's virtual machine EVM in Rust. This involves running rocq-of-rust to translate the Rust code to the theorem prover Rocq, and then making a proof by refinements until obtaining a specification of the code written in purely functional style, optimized for formal verification. This also proves the code cannot panic, as our specifications are free of panics.
🦀 Functional correctness of STATIC_CALL in Revm
· 9 min read