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