本文介绍了Clean框架的最新进展，该框架是一个基于Lean4的零知识电路验证DSL。主要创新是引入了Channel原语，用于建模多AIR系统（如zkVM）中的跨表交互。通过Channel，电路可以本地进行推理，同时通过通道平衡保证全局正确性。文章详细说明了Channel的结构、本地证明与全局意义的关系，以及如何通过组件组合实现端到端验证。还以斐波那契VM为例展示了实际应用，并讨论了完整性的重要性。Clean的目标是从验证单个电路扩展到验证整个zkVM系统。

文章宣布了mpcsec.org的发布，这是一个由zkSecurity、Trail of Bits等安全团队共同维护的多方计算（MPC）实现陷阱指南。该指南涵盖输入验证、上下文绑定、并发与状态、不安全子协议、故障恢复和自适应输入六类常见错误，并附有来自tss-lib、WSTS、MP-SPDZ、Drand等真实库的案例。此外，还提供了用于AI辅助代码审查的SKILL.md文件。

本文是系列第三部分，在引入环和模的基础上，继续构建线性映射、同构和双线性映射的数学工具。通过定义、例子和直觉解释，为后续用代数张量约简视角理解sum-check协议奠定基础。强调线性映射保持模结构，同构表示结构等价，双线性映射是双变量线性映射，是张量积的动机。

本文提出了一种软件开发的新范式：使用AI代理直接编写RISC-V汇编代码，并在Lean证明助手中进行形式化验证，确保zkVM的guest程序无bug。作者认为，由于RISC-V汇编易于推理，且AI代理能自动编写代码和证明，这种方法比使用Rust、C等高级语言更可靠，避免了编译器优化带来的不确定性和未定义行为。文章比较了CompCert、CakeML、Rust等方案，并指出汇编+Lean是范畴论意义上的最终形式。

本文是系列文章的第二部分，旨在为将sum-check协议形式化为代数张量约化建立数学基础。文章介绍了环和模的定义、例子和直觉，重点阐述了为何需要这些概念：在sum-check场景中，多项式环可视为R-模，区分环结构和模结构对于描述协议中的代数约化至关重要。文章提供了丰富的例子（如整数环、多项式环、矩阵环等）和直觉解释（模是向量空间的推广，标量来自环而非域），并预告后续将介绍模同态等概念。

本文揭示了Jolt透明/非ZK验证器中的一个soundness漏洞：在uni-skip优化中，验证器未检查证明提供的输出声明是否与提交的单变量多项式在挑战点r0处的求值一致。

本文介绍了基于除子（divisor）的椭圆曲线内积证明（ECIP）技术，该技术由 Liam Eagen 提出，用于 Monero 的 FCMP++ 升级。zkSecurity 对其进行了安全审计，并发布了详细笔记，涵盖从代数几何到具体约束的完整形式化处理。核心技巧是利用有理函数与除子的一一对应关系，通过对数导数技巧将验证简化为线性关系，使得任意长度的多标量乘法（MSM）仅需 7 个乘法约束即可验证。该技术将大幅提升 Monero 的成员证明效率，使其能够包含所有可能的交易。

文章深入探讨了加密内存池的安全设计，指出其不仅依赖加密方案，还需确保在整个交易生命周期中，交易内容在排序确定前保持隐藏，解密后必须立即执行或终结。重点分析了阈值加密、CCA安全、密文上下文绑定、解密时机与最终性对齐、防止无效交易被解密后利用等关键安全点，并讨论了资源耗尽、边界重放等常见失败模式。最后强调加密内存池能减少抢先交易MEV，但无法完全消除，用户需明确其局限性。

本文是zkSecurity团队对赞助zkSummit14会议的公告，同时回顾了零知识证明领域十年来的进展。文章提到，尽管ZKP已从理论走向实际应用，日处理数亿美元价值，但安全漏洞仍频发。近期发生了首个公开的黑客攻击事件（Veil隐私池被盗约5K美元）和白帽救援行动（Foom彩票应用挽回约50万美元），而这两个漏洞都源于部署脚本缺失，而非复杂的密码学缺陷。作者强调，自动化审计工具（如zkao）虽能捕获部分错误，但高价值漏洞仍需人工审计。最后邀请参会者现场交流。

本文分析了一个在 Rust 实现的 Limbo 零知识证明协议中的单字符 bug：代码中本应计算多项式 f(r) = Σ e_i·r^i，但由于将 r *= challenge 误写为 r *= r，导致实际计算的是 Σ e_i·r^{2^i}。