2024 年 10 月 21 日，CertiK 高级首席科学家 Vilhelm Sjöberg 博士受邀出席由以太坊基金会和 ZKProof 联合主办的“零知识证明（ZKP）形式化验证研讨会”并发表主题演讲，分享了 CertiK 在 zkWasm 形式化验证中的前沿研究成果。此次研讨会旨在探讨 ZKP 形式化验证领域的最佳实践和创新思路，尤其是零知识虚拟机（zkVM）的验证方法。从而推动以太坊基金会近期启动的零知识以太坊虚拟机（zkEVM）形式化验证计划——一个总额达 2000 万美元、为期多年的计划[1]，以期实现以太坊未来 L1 和 L2 层扩展的重要里程碑。

在研讨会上，Sjöberg 博士就 zkWasm[2]的形式化验证进行了讲解，这是今年早些时候由 CertiK 完成的全球首个通用 zkVM 的形式化验证。WebAssembly（Wasm）是一种广受欢迎的便携式应用执行平台，能够提供接近原生的运行性能。对其 zkVM 的形式化验证将大大增强该技术在区块链和零知识计算领域的可信度和应用前景。在此次突破性的验证工作中，CertiK 还发现了两个关键漏洞，并与 zkWasm 的开发方 Delphinous Lab 合作将其修复。经过数学上的正确性和保密性验证，基于 zkWasm 的区块链应用如今已逐步投入生产应用，为安全和高效的零知识计算提供了强大支持。

凭借在 zkWasm 及其他 Web3 前沿形式化验证项目中积累的创新技术和丰富经验，CertiK 计划将在未来数年与以太坊基金会及相关社区展开密切合作，致力于实现以太坊 zkEVM 的完整验证，逐步查找和修复系统内每一个潜在漏洞。这些合作将助力以太坊实现全面扩展潜力，推动零知识技术在 Web3 生态系统中更安全、可信地落地应用。

[1] https://verified-zkevm.org/

[2] https://skynet.certik.com/projects/zkwasm