币圈界报道：

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

CertiK正式披露其针对zkWasm项目的完整形式化验证进展。该验证基于Coq定理证明器实现，通过机器可检查的数学证明，确认了zkWasm电路在执行过程中满足核心安全属性。尽管项目并非首次公开，但相关技术记录自2024年4月起已在官方博客持续更新，系统性呈现了从电路设计到验证框架的演进路径。

非零知识虚拟机实现可信计算，依赖严格约束体系

zkWasm作为面向WebAssembly程序的零知识虚拟机，允许开发者在不暴露具体计算逻辑的前提下，向第三方证明程序已正确执行。该项目源自Delphinus Lab，其安全性完全取决于底层电路及其所定义的约束规则。若任何约束被遗漏，恶意参与者可能伪造有效证明，从而绕过所有依赖于该验证机制的应用层信任模型。

验证覆盖核心语义，确立两大安全基石

本次验证聚焦于两个关键属性：健全性（Soundness），确保每一个被接受的执行轨迹均对应合法的Wasm运行；知识健全性（Knowledge Soundness），防止证明者为错误执行生成有效证据。验证范围涵盖算术运算、位操作、内存访问、控制流跳转及函数调用等核心模块。据称，此成果是当前最全面的生产级zkVM形式化验证之一，延续了CertiK在2024年宣称的全球首个完整案例定位。

人工转化与大规模证明工程并行推进

验证过程将Halo2电路逻辑转换为Coq语言，并对转换后的命题进行逐项证明。整个开发流程由人工完成，力求贴近原始Rust代码以减少引入偏差。项目共涉及约33,000行Coq代码，其中约21,000行为实际证明内容。值得注意的是，尽管Coq自2025年起更名为Rocq，CertiK仍沿用旧称。

多团队协同验证，行业安全标准逐步建立

除CertiK外，以太坊基金会正主导一项耗资2,000万美元的zkEVM形式化验证计划。研究显示，该工作已持续超过一年，多个团队参与协作。Certora近期获资助，专注于自动预编译优化方案的验证。与此同时，Nethermind采用Lean定理证明器构建工具链，成功识别出Scroll Keccak-256电路中的严重缺陷，该电路随后已被废弃。团队指出，因证明者中心化，该漏洞实际未造成威胁。

验证边界明确：仅限电路层，其余组件仍需信任

根据CertiK官方文档，本次验证仅覆盖Halo2电路相对于WebAssembly语义的健全性，不包含外围组件。包括构建表格的Rust代码、Wasmi解释器以及Halo2本身均不在验证范围内。外部调用指令因缺乏明确约束而被忽略；指令解码逻辑仅经人工审查，未进行形式化证明；部分生成约束的Rust代码亦被假设为正确。因此，当前的安全保证仅适用于电路层，其他部分仍依赖传统审计与经验判断。

目前，公众无法完整审查所有细节。GitHub仓库虽发布定义与定理声明，但证明内容以占位符替代。公告未说明是否未来公开证明文件，也未明确验证版本及自2024年以来的变更情况。此外，所有结论均依赖于Halo2自身的可靠性，而该组件本身被明确排除在本次验证范围之外。