近日，以太坊基金会公布了2025年第一季度研究资助名单，全球最大的Web3.0安全公司CertiK荣获两项研究资助，源于zkEVM形式化验证竞赛。这不仅是以太坊扩展性战略的里程碑式事件，也进一步彰显了CertiK在零知识证明（ZKP）系统形式化验证领域的全球技术领导力。
CertiK的“先进形式化验证”技术是此次获奖的关键，相比传统方案，它实现了四大突破：直接针对具体代码而非抽象模型；深入验证代码独特属性而非通用特性；通过自动化框架攻克人力难以企及的复杂验证；适用于大规模生产环境而非局限于学术研究。值得一提的是，CertiK自创立之初便以形式化验证为核心技术，依托学术研究成果，为Web3.0项目提供高可靠性的安全服务。
这些优势使其特别适合处理复杂零知识证明系统。例如，CertiK去年完成了zkWasm电路的首次完整形式化验证，这一突破性成果证明了复杂零知识电路的全面形式化验证是可行的。此外，CertiK的形式化验证技术已经在多个Web3.0顶级项目和基础设施中得到广泛应用，包括zkWasm、TON主链合约、Cosmos SDK，以及蚂蚁集团的HyperEnclave TEE、Asterinas OS和SGX TRTS SDK等，充分展现了其技术的广泛适用性和高可靠性。
zkEVM（零知识以太坊虚拟机）是区块链技术中的一项创新，通过零知识证明实现以太坊的可扩展性。它允许将交易计算移至链下，并提供简洁的证明以验证交易的有效性，从而降低成本并提高吞吐量。然而，zkEVM的复杂性使其面临安全风险，形式化验证成为确保其正确性和安全性的关键工具。形式化验证通过数学方法证明系统在所有可能条件下的行为，确保没有漏洞或意外行为。
随着区块链技术的快速发展，特别是零知识证明系统的广泛应用，形式化验证将成为确保系统安全和可靠性的关键工具。CertiK的工作将为以太坊生态系统的可扩展性和安全性提供更高保障，同时为其他区块链项目树立了形式化验证的标杆。
