2 posts tagged with "formal specification"

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.

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.