CertiK表示，Coq证明表明zkWasm的核心电路是可靠的_新闻

免责声明：内容不构成买卖依据，投资有风险，入市需谨慎！

CertiK表示，Coq证明表明zkWasm的核心电路是可靠的

2026-09-28 21:16:26

CertiK宣布完成zkWasm的形式化验证：基于Coq的机器检查证明

CertiK宣布已完成对zkWasm的形式化验证工作。zkWasm是一种面向WebAssembly程序的非零知识（Zero-Knowledge）虚拟机，其验证过程使用了在Coq定理证明器中编写的机器检查证明。该公司于9月28日公布了这一结果，尽管该项目并非全新推出。CertiK的技术博客系列早在2024年4月便已开始记录此项工作，当时首次描述了针对zkWasm电路的完整验证方案。

zkWasm允许开发人员在无需披露具体计算内容的情况下，证明某个WebAssembly程序已正确运行。该开源项目源自Delphinus Lab。所有基于该平台构建的应用都依赖于电路及其约束系统，这些系统决定了何种运行被视为有效。如果遗漏任何约束条件，不诚实的证明者可能会使错误的执行结果被接受，从而悄无声息地破坏所有依赖于此的验证逻辑。

CertiK表示已与超过5,500家企业客户合作，并将形式化验证定位为超越传统审计和测试的关键步骤。在实践中，这意味着证明检查器会确认代码对所有输入均符合数学规范，而不仅仅是那些经过人工测试的特定输入。

验证内容详解

根据官方发布的信息，此次验证确立了两个核心属性：

健全性（Soundness）：每一个被接受的执行轨迹都对应着Wasm程序的有效运行。
知识健全性（Knowledge Soundness）：证明者无法为错误的执行生成有效的证明。

验证范围涵盖了算术与位运算、内存访问、控制流以及函数调用。早在2024年，CertiK曾称该项目为全球首个完整的zkVM形式化验证案例。此次新发布的成果被认为是迄今为止针对生产级zkVM最全面的验证努力之一。

其方法论是将zkWasm的Halo2电路逻辑转化为Coq语言，并对转化过程的相关命题进行证明。CertiK公开的README文件指出，转化工作由人工完成，并尽可能贴近Rust源代码以限制错误。内部开发涉及约33,000行Coq代码，其中约21,000行为证明部分。（注：Coq项目自2025年起更名为Rocq，但CertiK的材料中仍沿用旧称。）

发布说明提到，过程中发现了若干细微的正确性问题并已解决，但未列出具体数量或评级。CertiK官网则提供了更详细的细节，列出了zkWasm中的两个健全性漏洞：一个是手动审查中发现的内存加载约束缺失；另一个是证明中发现的Return指令约束缺失，后者可能导致伪造返回。CertiK指出，任一漏洞都可能让恶意证明者通过验证器获取无效证明。

其他团队也在推进zkVM验证工作

CertiK并非孤军奋战。以太坊基金会正在运行一项耗资2,000万美元的zkEVM形式化验证项目。一名研究人员在2026年的研讨会摘要中指出，针对以太坊基础层核心zkVM部分的验证推动已持续一年多，且有多支团队参与。Certora于今年2月获得基金会拨款，用于验证自动预编译（autoprecompiles）这一电路优化方案。

此外，Nethermind团队使用Lean而非Coq构建了工具链，将Halo2约束提取至定理证明器中，并借此发现了一个Scroll Keccak-256电路中的关键漏洞。该电路随后已被弃用，Nethermind表示由于Scroll的证明者是中心化的，该漏洞实际上无法被利用。

验证范围的局限性

CertiK自身的README文件明确了此次验证的边界。其目标是证明电路相对于WebAssembly语义的健全性，因此Halo2电路之外的所有内容均不在验证范围内。这包括构建表格的Rust代码、Wasmi解释器以及Halo2本身。外部调用指令因缺乏实际约束而被跳过；指令解码逻辑仅经过人工审计而非形式化证明；部分生成约束的Rust代码也被假定为正确。因此，当前的保证仅覆盖电路部分，其余部分仍需信任。

目前，外界尚无法完全审查所有细节。公共GitHub仓库发布了定义和定理声明，读者可以查看所声称的内容，但其中的证明部分已被占位符替代。公告未说明这些证明是否会公开、验证的是哪个版本的zkWasm，以及自2024年以来发生了哪些变更。任何关于证明的保证也依赖于Halo2本身的可靠性，而README明确将Halo2列为已验证范围之外。

免责声明：

本网站、超链接、相关应用程序、论坛、博客等媒体账户以及其他平台和用户发布的所有内容均来源于第三方平台及平台用户。百亿财经对于网站及其内容不作任何类型的保证，网站所有区块链相关数据以及其他内容资料仅供用户学习及研究之用，不构成任何投资、法律等其他领域的建议和依据。百亿财经用户以及其他第三方平台在本网站发布的任何内容均由其个人负责，与百亿财经无关。百亿财经不对任何因使用本网站信息而导致的任何损失负责。您需谨慎使用相关数据及内容，并自行承担所带来的一切风险。强烈建议您独自对内容进行研究、审查、分析和验证。

展开阅读全文