币圈界报道：

zkWasm形式化验证落地：CertiK公布完整数学证明成果

CertiK正式对外披露其已完成针对zkWasm的完整形式化验证工作。该成果建立在Coq定理证明器之上，通过机器可检查的数学推导，对非零知识虚拟机的执行轨迹进行严格校验。尽管该项目自2024年4月起已在技术博客中持续更新，但此次9月28日发布的版本标志着首次实现生产级应用层面的全面验证。

核心属性获数学确证：健全性与知识健全性双达标

本次验证确立了两个关键数学特性：一是“健全性”——任何被接受的计算路径均对应合法的WebAssembly程序执行；二是“知识健全性”——攻击者无法构造出虚假执行的可信证明。验证覆盖算术运算、位操作、内存访问、控制流及函数调用等核心模块，被业界视为当前最完备的生产级zkVM形式化验证实践之一。

转化与构建：从Rust代码到Coq命题的严谨映射

为实现验证，CertiK将zkWasm的Halo2电路逻辑逐步转化为Coq语言表达式，并对每一步转换进行数学证明。整个过程由人工主导，力求贴近原始Rust代码结构以降低引入错误风险。项目共生成约33,000行Coq代码，其中约21,000行为证明部分。值得注意的是，尽管Coq自2025年起更名为Rocq，CertiK材料仍沿用旧称。

发现并修复隐蔽缺陷：两类漏洞暴露系统脆弱性

在验证过程中识别出多个细微的正确性问题，均已修复。具体包括：一处因手动审查遗漏的内存加载约束，以及另一处证明阶段发现的Return指令缺失约束，后者可能允许恶意证明者伪造返回值。若未及时修补，此类漏洞将使验证器误信无效执行结果，进而危及所有依赖该系统的应用。

多方协同推进zkVM安全：行业生态正加速成熟

CertiK并非唯一参与者。以太坊基金会已投入2,000万美元支持zkEVM的形式化验证项目，多支团队持续推动底层核心电路的数学确证。Certora近期获得资助，用于验证自动预编译优化方案。与此同时，Nethermind采用Lean工具链，成功在Scroll Keccak-256电路中发现关键漏洞，该电路随后被弃用，因其证明者存在中心化风险，实际利用可能性极低。

验证范畴受限：信任边界需理性认知

CertiK官方声明明确界定本次验证的范围仅限于Halo2电路相对于WebAssembly语义的正确性。构建表格的Rust代码、Wasmi解释器、指令解码逻辑及外部调用接口均不在验证范围内，前者依赖人工审计，后者因缺乏显式约束而被跳过。此外，所有保证均建立在Halo2本身已被验证的前提下，而该组件亦未包含在本次验证体系中。

目前，公众虽可查阅公开GitHub仓库中的定义与定理声明，但核心证明内容以占位符替代。公告未说明后续是否开放完整证明、所验证的具体zkWasm版本，或自2024年以来的功能变更情况。因此，当前的安全承诺仅适用于电路层，其余部分仍需基于信任模型进行评估。