Axiom Halo2电路的深度分析

Trail of Bits 对 Axiom 系统进行了两轮审计：该系统让 EVM 合约可借助 Halo2 零知识证明查询以太坊历史数据。审计发现若干 soundness 与约束缺失（under-constrained）问题，相关电路后来演进为通用 ZK 虚拟机 OpenVM，支持对任意 Rust 程序生成证明。