以太坊联创 Vitalik Buterin 发布文章《A shallow dive into formal verification》，系统梳理了形式化验证（Formal Verification）在以太坊及更广泛计算领域中的最新发展与局限。文章指出，近几个月在以太坊前沿研究圈中，一种新编程范式正在快速兴起：开发者直接使用极低级语言（如 EVM 字节码、汇编）或 Lean，并通过可自动验证的数学证明来验证代码正确性。这种方法理论上既能提升代码效率，也能显著提高安全性，被部分研究者称为“软件开发的终极形态”