据 ChainCatcher 称，Vitalik 今天发布了一篇题为《对形式化验证的浅层探索》的文章，讨论了形式化验证如何在以太坊开发中同时提升安全性和效率。开发者可以使用 Lean、以太坊虚拟机（EVM）字节码或汇编语言来编写代码，并通过可自动检查的数学证明来验证其正确性。Vitalik 指出，形式化验证尤其适用于 STARKs、拜占庭容错共识、ZK-EVM 和后量子签名等复杂系统，尽管它也有局限性，包括规格说明错误、代码覆盖不完整以及硬件层面的攻击。