zkEVM performance headlines arrive at an accelerating pace, but full and robust formal correctness guarantees have not yet been established for any zkEVM. We set out the properties that constitute a good specification, share what we learned by formally specifying the EVM state transition function in evm-sail, and describe progress toward verifying the safety of production zkEVM components.