4 posts tagged with "rocq-of-rust"

We have updated our translation and functional specification of Revm, a Rust implementation of the Ethereum Virtual Machine (EVM), to Revm v102. We use our tool rocq-of-rust to translate the Rust code to the Rocq theorem prover, where we write purely functional specifications and prove them equivalent to the translated code.

This upgrade introduced a large change in the generated Rocq code and in the interfaces used by the EVM instructions. The first translation did not compile in Rocq. We repaired the link and simulation layers one instruction family at a time and updated the tests and continuous integration pipeline to the new Revm architecture.

Here is our proposal to make end-to-end formally verified zkEVMs for the next version of Ethereum, with an estimated gain of between 2x and 4x more TPS compared to existing approaches.

We have completed a formal specification of Revm, the main Rust implementation of the Ethereum Virtual Machine (EVM), covering 94% of the EVM instructions, considering the function of their definitions. Using our tool rocq-of-rust, we translated the Rust code into the Rocq theorem prover and wrote purely functional specifications proven equivalent to the original code. In total, we produced about 50,000 lines of Rocq, and also proved the absence of panics for all covered instructions. We publish our full report: Formal Specification of Revm.

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.