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.