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生态系统中更安全、可信地落地应用。
