TechFlow news: On May 18, Vitalik published an article titled “A Shallow Dive into Formal Verification,” outlining recent progress in applying formal verification to cutting-edge Ethereum research and development. The article states that developers can write code in Lean, EVM bytecode, or assembly language and verify its correctness via mathematically rigorous, automatically checkable proofs—thereby enhancing both code efficiency and security.
He notes that formal verification is especially suitable for complex yet security-objective–clear systems such as STARKs, Byzantine Fault Tolerant (BFT) consensus, ZK-EVMs, and post-quantum signatures, and cites related projects including Arklib, VCV-io, and evm-asm. The article also emphasizes that formal verification is not a panacea—it remains subject to limitations such as specification errors, unverified code paths, hardware boundaries, and side-channel attacks.
