ai-provers

本文报告了一个验证流水线的经验，该流水线使用AI证明器（Aristotle和Aleph）结合符号提取工具和形式化密码学库，为Lean 4中的Rust密码学代码生成机器检查的正确性证明，并提供了来自以太坊基金会zkEVM项目的案例研究。