Lean

本文介绍了如何形式化验证Plonky2中的U32AddManyGate。通过从Rust导出多项式约束到Lean，将约束通用化并编写基于自然数算术的规范，然后证明约束满足推导出规范（可靠性）以及规范存在时约束可满足（完备性）。验证过程发现了一个隐式假设：进位输入必须≤15，而接口允许更大值，这可能导致不完整。该工作为Lighter项目提供了可信任的电路基础。

AMO-Lean 是一个经过验证的优化器，它将 Lean 4 中编写的数学规范转换为具有形式正确性保证的优化后的 C 和 Rust 代码。它通过将代数定理编译为重写规则，并将其输入到纯函数式等式饱和引擎中来实现这一点。每个应用的转换都有一个对应的 Lean 证明，并且可以根据形式验证的逻辑来审计发出的代码。

文章比较系统地对比了多个用于验证算术电路与零知识电路的形式化验证框架，包括 ACL2（r1cs/PFCS）、acl2-jolt、Garden、zk-lean、sp1-lean 和 Clean。作者从示例复杂度、可复现性、Claude Code 辅助证明能力、优缺点与设计取舍等维度做了实测式评估，并指出不同工具在安装门槛、证明风格、完备性、工程透明度和可扩展性上的差异。文章核心观点是：未来电路验证会越来越自动化，但高质量、可复用、可验证的框架仍然稀缺。

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

本文详细解释了Poseidon arity-1 (t=2) 哈希函数在BN254曲线上的soundness和completeness形式化证明。

形式化验证（Formal Verification）是通过编写数学证明并由计算机自动验证程序正确性的技术。以太坊联合创始人Vitalik Buterin深入探讨了该技术在区块链、密码学和AI领域的应用，强调其在保证代码安全性、尤其是在智能合约和ZK-EVM等核心组件上的潜力。文章指出，形式化验证并非万能，存在规范遗漏、部分验证等缺陷，但通过AI辅助可大幅提升效率，形成“安全核心+边缘非安全代码”的新安全模型，有望实现防御方优势。

本文深入剖析了Succinct Labs与Nethermind对SP1 Hypercube RISC-V zkVM的形式化验证工作。作者详细解释了验证的范围、假设、公理以及各个芯片的定理，并指出尽管验证了51个操作码的正确性，但存在多个未覆盖或错误的情况。通过测试发现了JALR指令的bug（未清除最低位），并利用LLM审计发现了SLTI指令的空证明和加载指令的错误规范。文章最后对形式化验证的沟通和验证提出了建议，强调需要明确的规范、可重现性和更多的验证。

本文作者回顾了自己2014年创建的Proof Market，并探讨了使用zkVM构建非托管版本，以及使用计算机语言来编写和检查数学证明来验证算术电路的正确性。文章对比分析了多个用于验证算术电路的框架，包括ACL2、Garden、zk-lean、sp1-lean和Clean，并评估了它们在不同方面的优缺点，以及作者和Claude Code在这些框架上的使用体验。

本文介绍了交互式定理证明器（又称证明助手），这种工具可以创建严格的、机器可检查的数学定理和计算证明。文章以 Lean 为例，展示了如何使用证明助手来验证数学证明的正确性，并探讨了证明助手在零知识虚拟机（zkVM）开发中的应用。

本文介绍了如何使用Lean工具来验证密码学论文的正确性，以FRI（Fast Reed-Solomon Interactive Oracle Proof of Proximity）为例，阐述了通过Lean形式化验证密码学证明的过程，并讨论了未来将该形式化验证结果整合到Arklib以及进行具体实例化的可能性，最终帮助非专家人士更好地理解和验证密码学研究。

Lean4工程化入门：Elan工具链配置与Lake包管理实战Lean4不仅仅是数学家的证明助手，更是一门兼顾严谨逻辑与高性能的现代编程语言。要真正驾驭Lean4，理解其背后的工程化逻辑比记忆语法更重要。本文将越过理论，直击底层，详解如何通过Elan管理版本工具链，并利用La