1. 项目概述当形式化验证遇见硬件设计最近在硬件验证的圈子里一个老生常谈但又始终绕不开的痛点就是如何确保我们设计的电路从RTL代码到最终的硅片其行为完全符合我们的数学规格传统的仿真和断言验证SVA覆盖了大部分场景但对于那些性命攸关或极端复杂的模块我们总感觉心里没底。仿真永远无法穷尽所有状态而形式化验证Formal Verification虽然理论上能提供数学上的完备性证明但其陡峭的学习曲线和工具链的复杂性让很多团队望而却步。这就是我接触到CircuitProver这个项目时感到兴奋的原因。它不是一个全新的验证工具而是一个构建在Lean 4定理证明器之上的、面向硬件验证的智能代理Agentic框架和可复用的电路证明库。简单来说它试图用程序员更熟悉的“写代码”的方式来“编写”和“管理”对硬件设计的数学证明。你不再需要去记忆那些晦涩的形式化验证工具的命令行选项和特定语法而是用 Lean 4 这种通用的函数式编程语言来描述你的电路规格并逐步构建证明。更关键的是它引入了“智能代理”的概念让证明过程本身可以部分自动化并能复用前人已经证明过的通用电路模块比如加法器、乘法器、状态机大幅降低验证工作的重复劳动。这个项目瞄准的正是那些对正确性有极致要求又苦于传统形式化工具难以上手的硬件设计团队特别是涉及密码学电路、处理器内核、航天级芯片等安全关键领域的工程师。如果你正在为如何证明一个复杂流水线控制逻辑的无死锁特性而头疼或者想为你设计的加密算法硬件实现提供一个可审计的数学证明那么 CircuitProver 及其背后的思路值得你花时间深入了解。2. 核心思路构建可复用的硬件证明“乐高积木”CircuitProver 的核心哲学是将硬件验证从“一次性、黑盒式的工具应用”转变为“可积累、白盒化的知识构建”。它的整体设计思路可以拆解为三个层次语言层、代理层和库层。2.1 语言层为什么是 Lean 4选择 Lean 4 作为基石是项目最根本也最巧妙的一个决策。Lean 本身是一个依赖类型Dependent Type的定理证明器这意味着它的类型系统强大到可以表达复杂的数学命题。对于硬件验证而言我们可以用 Lean 的类型来精确描述电路的行为。例如一个 32 位加法器在 Lean 中我们可以定义一个类型Adder32它的输入是两个BitVec 3232位位向量输出是一个BitVec 32和一个Bool表示进位。而加法器的正确性规格就可以表述为一个定理Theorem对于任意两个输入a和bAdder32的输出结果等于a b这里是数学上的整数加法但需要定义到位向量的语义上。-- 一个简化的概念性示例非实际 CircuitProver 代码 theorem adder_correct (a b : BitVec 32) : (Adder32 a b).sum bitvec_add a b : by -- 这里会进行证明 ...使用 Lean 4 的优势显而易见统一的环境规格描述、证明过程、甚至测试用例都在同一种语言Lean中完成。避免了规格用某种属性描述语言如PSL与证明工具如商业形式化工具之间的语义鸿沟。可编程的证明Lean 的证明本质上是构造一个满足类型的项。我们可以编写策略Tactics和元程序Metaprogramming来自动化证明步骤这就是“智能代理”能力的基础。严格的数学基础基于依赖类型理论整个证明链条可以被 Lean 内核严格检查最终保证证明的正确性只依赖于 Lean 公理与任何外部工具的可靠性解耦。活跃的生态Lean 社区有庞大的数学库Mathlib其中包含大量已被形式化的数学定理如数论、代数、分析这些可以直接被硬件验证借用例如证明一个加密算法实现的正确性时可以调用Mathlib中关于模运算的定理。注意Lean 4 的安装通常通过其版本管理器elan和包管理器lake完成。对于追求稳定性的工程环境建议使用elan安装一个稳定的 Lean 4 版本如elan default stable并通过lake锁定Mathlib等依赖的版本避免因社区库快速更新而引入的意外变更。2.2 代理层让证明“半自动化”“Agentic”智能代理是项目的点睛之笔。它并不是指一个具备通用人工智能的代理而是指一套在 Lean 证明环境中能够根据当前证明目标Goal自动选择并应用合适证明策略Tactic的自动化机制。在传统的交互式定理证明中工程师需要手动输入一系列策略命令如intro,apply,rewrite,simp来一步步推进证明。这要求工程师既是硬件专家又是证明专家门槛极高。CircuitProver 的代理层试图封装这些专家知识。其工作流程大致如下目标分析代理接收当前的证明目标例如要证明等式A B。策略检索代理根据目标的结构是等式是不等式涉及位向量操作和上下文已有的假设从一个预定义的策略库或通过学习历史成功证明检索可能有效的策略或策略组合。策略执行与回溯代理尝试应用检索到的策略。如果成功则进入下一个子目标如果失败或产生过于复杂的子目标则进行回溯尝试其他策略或组合。与用户交互对于完全自动化失败的关键步骤代理会暂停并提示用户给出当前目标和它建议的几种策略方向由用户做出决策。这形成了人机协同的证明模式。例如在证明一个多路选择器MUX的布尔逻辑性质时代理可能会自动识别出可以使用simp策略来简化基于if-then-else的表达式或者调用专门的bitblast位爆破策略将位向量操作分解为布尔逻辑。2.3 库层可复用的电路证明“零件盒”这是 CircuitProver 提升生产力的关键。想象一下每次设计一个新的芯片你都需要从零开始证明一个与门AND Gate的功能是正确的这无疑是巨大的浪费。CircuitProver 的核心价值之一就是构建一个不断增长的、可复用的电路证明库。这个库按照硬件设计的层次进行组织基础门电路层包含与、或、非、异或等基本逻辑门的定义及其基本性质如结合律、交换律、德摩根定律的证明。组合电路模块层包含编码器、译码器、加法器、乘法器、比较器、多路选择器等常用模块的规格定义和功能正确性证明。时序电路模块层包含触发器Flip-Flop、寄存器、计数器、有限状态机FSM等的模型及其时序性质如建立保持时间关系、状态转移正确性的证明。接口与协议层包含对常见总线协议如 AXI、APB、Wishbone的抽象模型和关键属性如无死锁、数据一致性的证明框架。当你要验证一个包含上述模块的新设计时你不需要重新证明它们。你只需要在你的顶层证明中像调用软件库函数一样“导入”import这些已经证明过的模块并声明你的设计是如何由这些模块互连构成的。然后你的证明任务就简化为证明这些模块在特定互连方式下整体行为满足你的顶层规格。这极大地缩小了需要人工干预的证明范围。3. 实操流程从电路描述到完成证明让我们通过一个相对简单的例子——验证一个 4 位行波进位加法器Ripple Carry Adder, RCA——来具体感受一下使用 CircuitProver 的工作流。这个例子涵盖了从环境搭建、电路建模、规格定义到交互式证明的全过程。3.1 环境准备与项目初始化首先你需要一个可用的 Lean 4 开发环境。安装 elanelan 是 Lean 的版本管理器。通过其安装脚本可以一键安装。curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh安装后重启终端或运行source ~/.bashrc或对应 shell 的配置文件。安装稳定版 Lean 4对于工程项目建议使用稳定版本。elan default stable这会将当前默认的 Lean 工具链设置为最新的稳定版。创建项目使用lake初始化一个新的 Lean 项目。lake是 Lean 的构建系统和包管理器。lake new MyHardwareProofs cd MyHardwareProofs配置依赖编辑项目根目录的lakefile.lean添加对CircuitProver库假设其已发布到某个 Git 仓库或包索引和Mathlib的依赖。-- lakefile.lean import Lake open Lake DSL package «my_hardware_proofs» where -- 更多包配置... require mathlib from git https://github.com/leanprover-community/mathlib4.git -- 假设 CircuitProver 库的地址 require circuitprover from git https://github.com/example_user/CircuitProver.git然后运行lake update来获取依赖。3.2 电路建模与规格定义在MyHardwareProofs项目的Main.lean或你新建的.lean文件中开始建模。导入库import CircuitProver.Core -- 导入 CircuitProver 核心定义 import CircuitProver.Gates -- 导入基础门电路库 import CircuitProver.BitVec -- 导入位向量库定义全加器Full Adder一个全加器是 RCA 的基本单元。我们可以直接复用库中的定义也可以自己定义以理解过程。-- 复用库中的全加器推荐 -- 库中可能已经定义了 full_adder 函数及其性质 -- 或者为了演示我们手动定义一个 def my_full_adder (a b cin : Bool) : Bool × Bool : let sum : xor (xor a b) cin let cout : (a b) || (b cin) || (a cin) (sum, cout)这里my_full_adder接受三个布尔输入a,b,cin返回一个二元组(sum, cout)。定义 4 位 RCA通过串联 4 个全加器来构建。def ripple_carry_adder_4bit (a b : BitVec 4) (cin : Bool) : BitVec 4 × Bool : let (s0, c0) : my_full_adder (a.getLsb 0) (b.getLsb 0) cin let (s1, c1) : my_full_adder (a.getLsb 1) (b.getLsb 1) c0 let (s2, c2) : my_full_adder (a.getLsb 2) (b.getLsb 2) c1 let (s3, c3) : my_full_adder (a.getLsb 3) (b.getLsb 3) c2 (BitVec.ofBits #[s3, s2, s1, s0], c3)这个函数逐位计算将低位的进位输出cout连接到高位的进位输入cin。定义规格定理我们想要证明这个 RCA 实现的加法与数学上的整数加法考虑进位结果一致。theorem rca_4bit_correct (a b : BitVec 4) (cin : Bool) : let (sum, cout) : ripple_carry_adder_4bit a b cin let a_nat : a.toNat let b_nat : b.toNat let cin_nat : if cin then 1 else 0 let total : a_nat b_nat cin_nat sum.toNat total % 16 ∧ cout (total / 16 0) : by -- 证明过程将在这里进行 ...这个定理陈述了将位向量a,b和进位cin转换为自然数后相加得到的总和total。RCA 计算出的sum对应的自然数应等于total对 162^4取模的结果而最终的进位输出cout为真当且仅当total除以 16 的商大于 0即发生了溢出。3.3 交互式证明与代理辅助现在进入最核心的证明环节。我们打开定理rca_4bit_correct下的by块开始构造证明。展开定义第一步通常是展开unfold或简化simp函数定义让证明目标变得更具体。unfold ripple_carry_adder_4bit unfold my_full_adder执行后目标会变成一系列基于布尔逻辑和位操作的复杂等式。调用位爆破Bit-blasting策略对于这种涉及位向量和布尔运算的证明CircuitProver 库通常会提供一个强大的策略比如叫bitblast。这个策略会自动将位向量操作分解爆破到每一位的布尔操作上。bitblast执行bitblast后证明目标会从关于位向量的陈述转化为关于 4 个独立布尔变量a的每一位、b的每一位和进位链的布尔等式集合。这时代理可能会介入自动应用一些布尔化简规则。使用simp和布尔化简对于布尔等式Lean 的simp策略结合布尔代数的引理如Bool.and_true,Bool.xor_false可以自动化简很多项。simp [Bool.xor, Bool.and, Bool.or, not] at *这里的at *表示对所有假设和目标进行化简。代理可能会智能地选择需要应用的特定化简规则而不是一股脑地全部尝试。分情况讨论Case Split有时化简后目标可能依赖于某些布尔变量的值例如cin是true还是false。这时可以使用cases策略进行分情况讨论。cases cin · -- 情况1: cin true ... · -- 情况2: cin false ...代理可以识别出何时需要进行分情况讨论并自动生成相应的子目标结构。逐一解决子目标在bitblast和分情况讨论后你可能会得到几十甚至上百个简单的子目标每个子目标可能只是一个布尔等式如x x或不等式。对于这些simp或trivial策略通常能直接解决。代理可以批量处理这些琐碎目标。all_goals { try simp; try trivial } -- 尝试对所有剩余目标使用 simp 或 trivial完成证明当所有子目标都被解决后Lean 会提示“Goals accomplished ”证明完成。在整个过程中CircuitProver 的“代理”能力体现在当你输入bitblast时它背后可能是一系列预编程的策略组合。当你使用simp时代理可能根据当前目标的形状从Mathlib或 CircuitProver 库中自动选择最相关的化简规则进行应用而不是盲目尝试所有规则这能显著提高证明效率并避免超时。在证明陷入僵局时集成开发环境如 VS Code 的 Lean 插件可能会在“策略建议”Tactic Suggestions面板中给出几个可能有效的下一步策略这就是代理交互的一种体现。3.4 证明复用与组合一旦我们完成了rca_4bit_correct的证明这个定理本身就成为了证明库的一部分。现在如果我们要验证一个使用了这个 4 位 RCA 作为子模块的更大电路例如一个 16 位加法器由 4 个 4 位 RCA 级联而成我们不需要重新证明 RCA 的内部逻辑。我们可以在新的定理中直接引用have或应用apply已经证明过的rca_4bit_correct定理。这体现了“可复用证明库”的巨大威力验证工作变成了模块化的、可组合的工程类似于用已经测试过的软件库函数来构建新程序。4. 深入解析CircuitProver 库的关键组件与设计模式要真正用好 CircuitProver不能只停留在调用几个策略上需要理解其库的核心组件和背后的设计模式。这能帮助你在遇到复杂电路时知道如何有效地建模和分解证明。4.1 硬件模型的抽象层次CircuitProver 库通常提供不同抽象层次的硬件模型以适应不同的验证需求。抽象层次描述适用场景示例行为级Behavioral用纯函数描述电路的输入输出关系忽略内部结构和时序。验证算法功能正确性、高级属性如等价性。直接用 Lean 函数定义adder a b a b。寄存器传输级RTL明确区分组合逻辑和时序元件寄存器。使用时钟和状态的概念。验证同步数字电路的具体实现包括时序和状态机。定义State类型和next_state函数用定理描述每个时钟周期的行为。门级Gate-level电路被描述为由基本逻辑门AND, OR, NOT互连而成的网络。验证综合后网表的功能、进行低功耗或故障分析。使用库中的Gate类型和connect函数来构建网表。在 CircuitProver 中你可以在同一项目甚至同一证明中混合使用这些抽象层次。例如你可以用行为级模型定义规格用 RTL 级模型描述实现然后证明两者在功能上等价。4.2 属性规范不仅仅是功能正确硬件验证远不止于证明“加法器能算对加法”。CircuitProver 库鼓励用户形式化更丰富的属性安全性属性Safety Properties某些“坏事情”永远不会发生。theorem no_buffer_overflow (state : SystemState) (input : Input) : (next_state state input).buffer_size ≤ MAX_BUFFER_SIZE : by ...证明缓冲区永远不会溢出。活性属性Liveness Properties某些“好事情”最终会发生。theorem request_eventually_served (initial_state : SystemState) : ∃ (n : Nat), (run_system_n_steps initial_state n).request_handled : by ...证明每一个请求最终都会被处理。这类证明通常需要引入时序逻辑或归纳法。等价性属性Equivalence Properties两个不同实现的行为一致。theorem rtl_equiv_behavioral (a b : BitVec 32) : rtl_multiplier a b behavioral_multiplier a b : by ...证明 RTL 级乘法器与行为级参考模型等价。资源约束属性证明电路满足面积、时序等约束这通常需要与外部工具结合或建立抽象模型。CircuitProver 库会提供描述这些属性的常用模式和辅助定理。例如对于时序属性库中可能定义了Always和Eventually等时序逻辑算子。4.3 策略库证明自动化的引擎“代理”能力的强弱直接取决于其背后的策略库。CircuitProver 的策略库可能包含bitblast如前所述将位向量操作分解为布尔操作的核心策略。sat或smt调用外部的 SAT 求解器或 SMT 求解器如 Z3, CVC5来处理当前子目标。这是处理复杂布尔/算术公式的有力武器。代理可以判断何时调用外部求解器是合适的。hardware_induction专门为硬件设计优化的归纳法策略。例如证明一个n位加法器的性质策略可以自动对位数n进行归纳。abstract_state用于处理状态机的策略可以帮助抽象掉不相关的状态细节简化证明。coverage与验证覆盖率相关的策略可以帮助检查是否所有重要的代码路径或状态都被属性覆盖到。一个高效的代理能够根据目标特征如包含大量位运算、是等式、是蕴含式等和历史成功案例自动组装和调度这些基础策略形成高效的证明搜索路径。5. 实战经验与避坑指南在实际使用 CircuitProver 或类似框架进行硬件形式化验证时我积累了一些经验教训这些在官方文档里往往不会明说。5.1 从简单开始迭代建模不要试图一开始就对整个 CPU 核心进行形式化。这会让你迅速陷入复杂性泥潭而失去信心。第一步从最小的单元开始比如证明一个与门AND的真值表或者一个 2 选 1 多路选择器MUX的功能。第二步用这些已验证的小单元搭建稍大的模块如 1 位全加器并证明其正确性。第三步用已验证的模块构建更复杂的模块如 4 位加法器、寄存器文件。关键在每一步都确保你的定理规格是清晰的证明是完整的。这样你的证明库就像搭积木一样稳健地增长。这种自底向上的方法能让你的建模和证明技能同步提升并及早发现抽象定义中的问题。5.2 精心设计抽象和接口硬件证明的难点一半在于证明本身另一半在于如何用数学语言优雅地描述硬件。避免过度具体在高层抽象中不要过早引入具体的位宽或硬件实现细节。例如先定义“一个加法器”的类型Adder (n : Nat) : BitVec n → BitVec n → BitVec n然后再用n : 32来实例化。这样你的定理和证明可以泛化到任意位宽。利用类型系统用 Lean 强大的类型系统来捕获不变量。例如定义一个类型NonEmptyList α来表示非空列表可以避免在证明中到处处理“列表可能为空”的边界情况。分离关注点将组合逻辑、时序逻辑、接口协议的定义分开。为时钟、复位、使能信号定义专门的类型和操作符而不是简单使用Bool。5.3 驾驭证明状态分解与聚焦交互式证明中你经常会面对一个包含许多假设和复杂结论的目标。感到无从下手是正常的。使用simp前先unfold如果simp没有效果可能是因为目标中的函数定义还没有展开。先用unfold function_name或dsimp展开定义。cases和induction是你的朋友对于归纳定义的数据类型如Nat,List, 自定义的枚举类型或带有析取∨连接的目标分情况讨论cases是打破僵局的基本方法。对于递归定义的结构或需要证明对所有n都成立的属性数学归纳法induction是标准工具。have引入中间引理如果证明过程很长可以手动have一个中间结论并先证明它。这不仅能理清思路还能让后续证明复用这个结论。CircuitProver 的代理有时也会建议引入某个关键的中间引理。关注当前目标Lean 界面会显示当前要证明的子目标。不要被长长的假设列表吓到一次只专注于解决当前这一个目标。使用{ }来聚焦到某个子目标上进行操作。5.4 性能调优与规模化当电路规模变大证明时间可能从几秒增长到几分钟甚至更长。策略选择simp可能会尝试大量重写规则导致变慢。尝试使用更具体的策略如simp [h1, h2]只使用h1和h2两个假设进行化简或者使用rw重写来定向替换。禁用无关规则simp可以配置为禁用某些规则simp [-rule_name]避免在不必要的方向上搜索。模块化证明将大定理的证明分解成多个独立的引理lemma。每个引理单独证明和缓存。当证明顶层定理时只需apply这些引理可以避免重复计算。利用外部求解器对于纯粹的大规模布尔可满足性问题SAT在策略中适时调用sat或smt策略链接到 Z3 等高性能外部求解器通常是最高效的方式。代理可以配置为在检测到目标是典型的 SAT 问题时自动调用。增量与缓存lake构建系统和 Lean 的编译内核会缓存已编译的.olean文件。合理组织你的代码文件使得修改一个模块时不需要重新证明所有不相关的模块。5.5 与现有工具链的集成CircuitProver 不是要取代现有的仿真或商业形式化验证工具而是互补。规格对齐可以用 CircuitProver 来形式化定义芯片的顶层接口协议如 AXI 一致性属性然后使用这个形式化规格作为黄金参考来编写 SystemVerilog Assertions (SVA) 或指导仿真测试点的生成。等价性检查的补充商业等价性检查EC工具能高效处理门级网表与 RTL 的等价性。但对于算法级变换如不同的乘法器架构或涉及复杂控制逻辑的等价性可以先在 CircuitProver 的行为级或高级 RTL 级进行证明为 EC 工具划定一个更可靠、更抽象的验证范围。形式化属性导出可以将 CircuitProver 中证明的关键属性以某种标准格式如 SVA 或 PSL导出直接嵌入到 RTL 代码中供仿真和动态验证使用实现形式化与动态验证的闭环。6. 常见问题与排查思路在实际操作中你肯定会遇到各种错误和卡点。下面是一些典型问题及其解决思路。问题现象可能原因排查与解决思路lake build失败提示找不到Mathlib依赖配置错误或网络问题。1. 检查lakefile.lean中mathlib的 Git 地址是否正确。2. 运行lake update强制更新依赖。3. 检查网络连接特别是访问 GitHub 是否顺畅。导入CircuitProver时报告未知标识符CircuitProver 库未成功安装或版本不匹配。1. 确认lakefile.lean中require circuitprover的路径正确。2. 运行lake build查看具体编译错误。3. 检查 CircuitProver 库所需的 Lean 版本是否与你安装的版本兼容。证明过程中simp或rw策略无效目标形式与规则不匹配或定义未展开。1. 使用unfold或dsimp展开目标中的函数定义。2. 使用set_option trace.Meta.Tactic.simp.rewrite true开启simp的详细跟踪看它尝试应用了哪些规则为什么失败。3. 检查你要使用的引理lemma的前提条件是否在当前上下文中满足。证明状态中出现大量无法自动解决的琐碎子目标自动化策略如bitblast产生了过多分支。1. 尝试使用;操作符批量应用策略如all_goals { try simp }。2. 考虑是否证明策略过于“暴力”是否需要手动引入更聪明的中间引理来简化问题结构。3. 对于布尔等式可以尝试调用decide策略它使用决策过程decision procedure来判定可判定的命题。证明一个关于BitVec n的性质但归纳法induction n失败对BitVec n直接进行归纳可能不直接因为它的定义可能不是简单的结构归纳。1. 尝试对索引i : Fin n进行归纳或者对自然数n本身进行归纳并在归纳步骤中利用BitVec的构造子如cons和tail来建立联系。2. 查看 CircuitProver 或Mathlib的BitVec库中是否有现成的归纳原理如bitvec.induction_on可以使用。使用sat策略超时生成的 SAT 问题过于复杂。1. 尝试在调用sat前先用simp或手工have一些引理来简化目标减少变量和约束数量。2. 考虑将问题分解成几个更小的子问题分别用sat解决。3. 检查外部求解器如 Z3的路径是否正确版本是否兼容。定理陈述看起来正确但就是证不出来定理本身可能是假的或者你的形式化模型与直觉有细微差别。1.构造反例尝试用#eval命令或写一个小测试程序给定理的输入赋一些具体的值看看结论是否成立。这是发现建模错误最快的方法。2.简化问题尝试证明定理的一个特例例如将位宽n固定为 1 或 2。如果特例都证不出来那很可能定理陈述或模型有问题。3.寻求帮助将你的问题最小化后在 Lean 或 CircuitProver 的社区如 Zulip 聊天频道提问。提供完整的、可运行的代码片段。最后我想分享的一点个人体会是使用 CircuitProver 这类工具进行硬件验证其价值不仅在于最终那个“QED”证明完毕的标记。更重要的价值在于形式化思考的过程。为了写出能被 Lean 接受的定理你必须极端精确地定义电路的行为这迫使你提前发现规格中的歧义、接口定义的不完整、甚至设计逻辑的潜在漏洞。这个过程本身就是对硬件设计一次无与伦比的深度审查。即使证明没有完全自动化你在尝试形式化过程中获得的深刻理解也足以大幅提升设计质量。把它看作是一个与机器协作、共同进行深度设计思考的伙伴而不仅仅是一个自动化的证明生成器你会从中获得更多乐趣和收获。 基于Lean 4的硬件形式化验证：CircuitProver框架与可复用证明库实践
1. 项目概述当形式化验证遇见硬件设计最近在硬件验证的圈子里一个老生常谈但又始终绕不开的痛点就是如何确保我们设计的电路从RTL代码到最终的硅片其行为完全符合我们的数学规格传统的仿真和断言验证SVA覆盖了大部分场景但对于那些性命攸关或极端复杂的模块我们总感觉心里没底。仿真永远无法穷尽所有状态而形式化验证Formal Verification虽然理论上能提供数学上的完备性证明但其陡峭的学习曲线和工具链的复杂性让很多团队望而却步。这就是我接触到CircuitProver这个项目时感到兴奋的原因。它不是一个全新的验证工具而是一个构建在Lean 4定理证明器之上的、面向硬件验证的智能代理Agentic框架和可复用的电路证明库。简单来说它试图用程序员更熟悉的“写代码”的方式来“编写”和“管理”对硬件设计的数学证明。你不再需要去记忆那些晦涩的形式化验证工具的命令行选项和特定语法而是用 Lean 4 这种通用的函数式编程语言来描述你的电路规格并逐步构建证明。更关键的是它引入了“智能代理”的概念让证明过程本身可以部分自动化并能复用前人已经证明过的通用电路模块比如加法器、乘法器、状态机大幅降低验证工作的重复劳动。这个项目瞄准的正是那些对正确性有极致要求又苦于传统形式化工具难以上手的硬件设计团队特别是涉及密码学电路、处理器内核、航天级芯片等安全关键领域的工程师。如果你正在为如何证明一个复杂流水线控制逻辑的无死锁特性而头疼或者想为你设计的加密算法硬件实现提供一个可审计的数学证明那么 CircuitProver 及其背后的思路值得你花时间深入了解。2. 核心思路构建可复用的硬件证明“乐高积木”CircuitProver 的核心哲学是将硬件验证从“一次性、黑盒式的工具应用”转变为“可积累、白盒化的知识构建”。它的整体设计思路可以拆解为三个层次语言层、代理层和库层。2.1 语言层为什么是 Lean 4选择 Lean 4 作为基石是项目最根本也最巧妙的一个决策。Lean 本身是一个依赖类型Dependent Type的定理证明器这意味着它的类型系统强大到可以表达复杂的数学命题。对于硬件验证而言我们可以用 Lean 的类型来精确描述电路的行为。例如一个 32 位加法器在 Lean 中我们可以定义一个类型Adder32它的输入是两个BitVec 3232位位向量输出是一个BitVec 32和一个Bool表示进位。而加法器的正确性规格就可以表述为一个定理Theorem对于任意两个输入a和bAdder32的输出结果等于a b这里是数学上的整数加法但需要定义到位向量的语义上。-- 一个简化的概念性示例非实际 CircuitProver 代码 theorem adder_correct (a b : BitVec 32) : (Adder32 a b).sum bitvec_add a b : by -- 这里会进行证明 ...使用 Lean 4 的优势显而易见统一的环境规格描述、证明过程、甚至测试用例都在同一种语言Lean中完成。避免了规格用某种属性描述语言如PSL与证明工具如商业形式化工具之间的语义鸿沟。可编程的证明Lean 的证明本质上是构造一个满足类型的项。我们可以编写策略Tactics和元程序Metaprogramming来自动化证明步骤这就是“智能代理”能力的基础。严格的数学基础基于依赖类型理论整个证明链条可以被 Lean 内核严格检查最终保证证明的正确性只依赖于 Lean 公理与任何外部工具的可靠性解耦。活跃的生态Lean 社区有庞大的数学库Mathlib其中包含大量已被形式化的数学定理如数论、代数、分析这些可以直接被硬件验证借用例如证明一个加密算法实现的正确性时可以调用Mathlib中关于模运算的定理。注意Lean 4 的安装通常通过其版本管理器elan和包管理器lake完成。对于追求稳定性的工程环境建议使用elan安装一个稳定的 Lean 4 版本如elan default stable并通过lake锁定Mathlib等依赖的版本避免因社区库快速更新而引入的意外变更。2.2 代理层让证明“半自动化”“Agentic”智能代理是项目的点睛之笔。它并不是指一个具备通用人工智能的代理而是指一套在 Lean 证明环境中能够根据当前证明目标Goal自动选择并应用合适证明策略Tactic的自动化机制。在传统的交互式定理证明中工程师需要手动输入一系列策略命令如intro,apply,rewrite,simp来一步步推进证明。这要求工程师既是硬件专家又是证明专家门槛极高。CircuitProver 的代理层试图封装这些专家知识。其工作流程大致如下目标分析代理接收当前的证明目标例如要证明等式A B。策略检索代理根据目标的结构是等式是不等式涉及位向量操作和上下文已有的假设从一个预定义的策略库或通过学习历史成功证明检索可能有效的策略或策略组合。策略执行与回溯代理尝试应用检索到的策略。如果成功则进入下一个子目标如果失败或产生过于复杂的子目标则进行回溯尝试其他策略或组合。与用户交互对于完全自动化失败的关键步骤代理会暂停并提示用户给出当前目标和它建议的几种策略方向由用户做出决策。这形成了人机协同的证明模式。例如在证明一个多路选择器MUX的布尔逻辑性质时代理可能会自动识别出可以使用simp策略来简化基于if-then-else的表达式或者调用专门的bitblast位爆破策略将位向量操作分解为布尔逻辑。2.3 库层可复用的电路证明“零件盒”这是 CircuitProver 提升生产力的关键。想象一下每次设计一个新的芯片你都需要从零开始证明一个与门AND Gate的功能是正确的这无疑是巨大的浪费。CircuitProver 的核心价值之一就是构建一个不断增长的、可复用的电路证明库。这个库按照硬件设计的层次进行组织基础门电路层包含与、或、非、异或等基本逻辑门的定义及其基本性质如结合律、交换律、德摩根定律的证明。组合电路模块层包含编码器、译码器、加法器、乘法器、比较器、多路选择器等常用模块的规格定义和功能正确性证明。时序电路模块层包含触发器Flip-Flop、寄存器、计数器、有限状态机FSM等的模型及其时序性质如建立保持时间关系、状态转移正确性的证明。接口与协议层包含对常见总线协议如 AXI、APB、Wishbone的抽象模型和关键属性如无死锁、数据一致性的证明框架。当你要验证一个包含上述模块的新设计时你不需要重新证明它们。你只需要在你的顶层证明中像调用软件库函数一样“导入”import这些已经证明过的模块并声明你的设计是如何由这些模块互连构成的。然后你的证明任务就简化为证明这些模块在特定互连方式下整体行为满足你的顶层规格。这极大地缩小了需要人工干预的证明范围。3. 实操流程从电路描述到完成证明让我们通过一个相对简单的例子——验证一个 4 位行波进位加法器Ripple Carry Adder, RCA——来具体感受一下使用 CircuitProver 的工作流。这个例子涵盖了从环境搭建、电路建模、规格定义到交互式证明的全过程。3.1 环境准备与项目初始化首先你需要一个可用的 Lean 4 开发环境。安装 elanelan 是 Lean 的版本管理器。通过其安装脚本可以一键安装。curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh安装后重启终端或运行source ~/.bashrc或对应 shell 的配置文件。安装稳定版 Lean 4对于工程项目建议使用稳定版本。elan default stable这会将当前默认的 Lean 工具链设置为最新的稳定版。创建项目使用lake初始化一个新的 Lean 项目。lake是 Lean 的构建系统和包管理器。lake new MyHardwareProofs cd MyHardwareProofs配置依赖编辑项目根目录的lakefile.lean添加对CircuitProver库假设其已发布到某个 Git 仓库或包索引和Mathlib的依赖。-- lakefile.lean import Lake open Lake DSL package «my_hardware_proofs» where -- 更多包配置... require mathlib from git https://github.com/leanprover-community/mathlib4.git -- 假设 CircuitProver 库的地址 require circuitprover from git https://github.com/example_user/CircuitProver.git然后运行lake update来获取依赖。3.2 电路建模与规格定义在MyHardwareProofs项目的Main.lean或你新建的.lean文件中开始建模。导入库import CircuitProver.Core -- 导入 CircuitProver 核心定义 import CircuitProver.Gates -- 导入基础门电路库 import CircuitProver.BitVec -- 导入位向量库定义全加器Full Adder一个全加器是 RCA 的基本单元。我们可以直接复用库中的定义也可以自己定义以理解过程。-- 复用库中的全加器推荐 -- 库中可能已经定义了 full_adder 函数及其性质 -- 或者为了演示我们手动定义一个 def my_full_adder (a b cin : Bool) : Bool × Bool : let sum : xor (xor a b) cin let cout : (a b) || (b cin) || (a cin) (sum, cout)这里my_full_adder接受三个布尔输入a,b,cin返回一个二元组(sum, cout)。定义 4 位 RCA通过串联 4 个全加器来构建。def ripple_carry_adder_4bit (a b : BitVec 4) (cin : Bool) : BitVec 4 × Bool : let (s0, c0) : my_full_adder (a.getLsb 0) (b.getLsb 0) cin let (s1, c1) : my_full_adder (a.getLsb 1) (b.getLsb 1) c0 let (s2, c2) : my_full_adder (a.getLsb 2) (b.getLsb 2) c1 let (s3, c3) : my_full_adder (a.getLsb 3) (b.getLsb 3) c2 (BitVec.ofBits #[s3, s2, s1, s0], c3)这个函数逐位计算将低位的进位输出cout连接到高位的进位输入cin。定义规格定理我们想要证明这个 RCA 实现的加法与数学上的整数加法考虑进位结果一致。theorem rca_4bit_correct (a b : BitVec 4) (cin : Bool) : let (sum, cout) : ripple_carry_adder_4bit a b cin let a_nat : a.toNat let b_nat : b.toNat let cin_nat : if cin then 1 else 0 let total : a_nat b_nat cin_nat sum.toNat total % 16 ∧ cout (total / 16 0) : by -- 证明过程将在这里进行 ...这个定理陈述了将位向量a,b和进位cin转换为自然数后相加得到的总和total。RCA 计算出的sum对应的自然数应等于total对 162^4取模的结果而最终的进位输出cout为真当且仅当total除以 16 的商大于 0即发生了溢出。3.3 交互式证明与代理辅助现在进入最核心的证明环节。我们打开定理rca_4bit_correct下的by块开始构造证明。展开定义第一步通常是展开unfold或简化simp函数定义让证明目标变得更具体。unfold ripple_carry_adder_4bit unfold my_full_adder执行后目标会变成一系列基于布尔逻辑和位操作的复杂等式。调用位爆破Bit-blasting策略对于这种涉及位向量和布尔运算的证明CircuitProver 库通常会提供一个强大的策略比如叫bitblast。这个策略会自动将位向量操作分解爆破到每一位的布尔操作上。bitblast执行bitblast后证明目标会从关于位向量的陈述转化为关于 4 个独立布尔变量a的每一位、b的每一位和进位链的布尔等式集合。这时代理可能会介入自动应用一些布尔化简规则。使用simp和布尔化简对于布尔等式Lean 的simp策略结合布尔代数的引理如Bool.and_true,Bool.xor_false可以自动化简很多项。simp [Bool.xor, Bool.and, Bool.or, not] at *这里的at *表示对所有假设和目标进行化简。代理可能会智能地选择需要应用的特定化简规则而不是一股脑地全部尝试。分情况讨论Case Split有时化简后目标可能依赖于某些布尔变量的值例如cin是true还是false。这时可以使用cases策略进行分情况讨论。cases cin · -- 情况1: cin true ... · -- 情况2: cin false ...代理可以识别出何时需要进行分情况讨论并自动生成相应的子目标结构。逐一解决子目标在bitblast和分情况讨论后你可能会得到几十甚至上百个简单的子目标每个子目标可能只是一个布尔等式如x x或不等式。对于这些simp或trivial策略通常能直接解决。代理可以批量处理这些琐碎目标。all_goals { try simp; try trivial } -- 尝试对所有剩余目标使用 simp 或 trivial完成证明当所有子目标都被解决后Lean 会提示“Goals accomplished ”证明完成。在整个过程中CircuitProver 的“代理”能力体现在当你输入bitblast时它背后可能是一系列预编程的策略组合。当你使用simp时代理可能根据当前目标的形状从Mathlib或 CircuitProver 库中自动选择最相关的化简规则进行应用而不是盲目尝试所有规则这能显著提高证明效率并避免超时。在证明陷入僵局时集成开发环境如 VS Code 的 Lean 插件可能会在“策略建议”Tactic Suggestions面板中给出几个可能有效的下一步策略这就是代理交互的一种体现。3.4 证明复用与组合一旦我们完成了rca_4bit_correct的证明这个定理本身就成为了证明库的一部分。现在如果我们要验证一个使用了这个 4 位 RCA 作为子模块的更大电路例如一个 16 位加法器由 4 个 4 位 RCA 级联而成我们不需要重新证明 RCA 的内部逻辑。我们可以在新的定理中直接引用have或应用apply已经证明过的rca_4bit_correct定理。这体现了“可复用证明库”的巨大威力验证工作变成了模块化的、可组合的工程类似于用已经测试过的软件库函数来构建新程序。4. 深入解析CircuitProver 库的关键组件与设计模式要真正用好 CircuitProver不能只停留在调用几个策略上需要理解其库的核心组件和背后的设计模式。这能帮助你在遇到复杂电路时知道如何有效地建模和分解证明。4.1 硬件模型的抽象层次CircuitProver 库通常提供不同抽象层次的硬件模型以适应不同的验证需求。抽象层次描述适用场景示例行为级Behavioral用纯函数描述电路的输入输出关系忽略内部结构和时序。验证算法功能正确性、高级属性如等价性。直接用 Lean 函数定义adder a b a b。寄存器传输级RTL明确区分组合逻辑和时序元件寄存器。使用时钟和状态的概念。验证同步数字电路的具体实现包括时序和状态机。定义State类型和next_state函数用定理描述每个时钟周期的行为。门级Gate-level电路被描述为由基本逻辑门AND, OR, NOT互连而成的网络。验证综合后网表的功能、进行低功耗或故障分析。使用库中的Gate类型和connect函数来构建网表。在 CircuitProver 中你可以在同一项目甚至同一证明中混合使用这些抽象层次。例如你可以用行为级模型定义规格用 RTL 级模型描述实现然后证明两者在功能上等价。4.2 属性规范不仅仅是功能正确硬件验证远不止于证明“加法器能算对加法”。CircuitProver 库鼓励用户形式化更丰富的属性安全性属性Safety Properties某些“坏事情”永远不会发生。theorem no_buffer_overflow (state : SystemState) (input : Input) : (next_state state input).buffer_size ≤ MAX_BUFFER_SIZE : by ...证明缓冲区永远不会溢出。活性属性Liveness Properties某些“好事情”最终会发生。theorem request_eventually_served (initial_state : SystemState) : ∃ (n : Nat), (run_system_n_steps initial_state n).request_handled : by ...证明每一个请求最终都会被处理。这类证明通常需要引入时序逻辑或归纳法。等价性属性Equivalence Properties两个不同实现的行为一致。theorem rtl_equiv_behavioral (a b : BitVec 32) : rtl_multiplier a b behavioral_multiplier a b : by ...证明 RTL 级乘法器与行为级参考模型等价。资源约束属性证明电路满足面积、时序等约束这通常需要与外部工具结合或建立抽象模型。CircuitProver 库会提供描述这些属性的常用模式和辅助定理。例如对于时序属性库中可能定义了Always和Eventually等时序逻辑算子。4.3 策略库证明自动化的引擎“代理”能力的强弱直接取决于其背后的策略库。CircuitProver 的策略库可能包含bitblast如前所述将位向量操作分解为布尔操作的核心策略。sat或smt调用外部的 SAT 求解器或 SMT 求解器如 Z3, CVC5来处理当前子目标。这是处理复杂布尔/算术公式的有力武器。代理可以判断何时调用外部求解器是合适的。hardware_induction专门为硬件设计优化的归纳法策略。例如证明一个n位加法器的性质策略可以自动对位数n进行归纳。abstract_state用于处理状态机的策略可以帮助抽象掉不相关的状态细节简化证明。coverage与验证覆盖率相关的策略可以帮助检查是否所有重要的代码路径或状态都被属性覆盖到。一个高效的代理能够根据目标特征如包含大量位运算、是等式、是蕴含式等和历史成功案例自动组装和调度这些基础策略形成高效的证明搜索路径。5. 实战经验与避坑指南在实际使用 CircuitProver 或类似框架进行硬件形式化验证时我积累了一些经验教训这些在官方文档里往往不会明说。5.1 从简单开始迭代建模不要试图一开始就对整个 CPU 核心进行形式化。这会让你迅速陷入复杂性泥潭而失去信心。第一步从最小的单元开始比如证明一个与门AND的真值表或者一个 2 选 1 多路选择器MUX的功能。第二步用这些已验证的小单元搭建稍大的模块如 1 位全加器并证明其正确性。第三步用已验证的模块构建更复杂的模块如 4 位加法器、寄存器文件。关键在每一步都确保你的定理规格是清晰的证明是完整的。这样你的证明库就像搭积木一样稳健地增长。这种自底向上的方法能让你的建模和证明技能同步提升并及早发现抽象定义中的问题。5.2 精心设计抽象和接口硬件证明的难点一半在于证明本身另一半在于如何用数学语言优雅地描述硬件。避免过度具体在高层抽象中不要过早引入具体的位宽或硬件实现细节。例如先定义“一个加法器”的类型Adder (n : Nat) : BitVec n → BitVec n → BitVec n然后再用n : 32来实例化。这样你的定理和证明可以泛化到任意位宽。利用类型系统用 Lean 强大的类型系统来捕获不变量。例如定义一个类型NonEmptyList α来表示非空列表可以避免在证明中到处处理“列表可能为空”的边界情况。分离关注点将组合逻辑、时序逻辑、接口协议的定义分开。为时钟、复位、使能信号定义专门的类型和操作符而不是简单使用Bool。5.3 驾驭证明状态分解与聚焦交互式证明中你经常会面对一个包含许多假设和复杂结论的目标。感到无从下手是正常的。使用simp前先unfold如果simp没有效果可能是因为目标中的函数定义还没有展开。先用unfold function_name或dsimp展开定义。cases和induction是你的朋友对于归纳定义的数据类型如Nat,List, 自定义的枚举类型或带有析取∨连接的目标分情况讨论cases是打破僵局的基本方法。对于递归定义的结构或需要证明对所有n都成立的属性数学归纳法induction是标准工具。have引入中间引理如果证明过程很长可以手动have一个中间结论并先证明它。这不仅能理清思路还能让后续证明复用这个结论。CircuitProver 的代理有时也会建议引入某个关键的中间引理。关注当前目标Lean 界面会显示当前要证明的子目标。不要被长长的假设列表吓到一次只专注于解决当前这一个目标。使用{ }来聚焦到某个子目标上进行操作。5.4 性能调优与规模化当电路规模变大证明时间可能从几秒增长到几分钟甚至更长。策略选择simp可能会尝试大量重写规则导致变慢。尝试使用更具体的策略如simp [h1, h2]只使用h1和h2两个假设进行化简或者使用rw重写来定向替换。禁用无关规则simp可以配置为禁用某些规则simp [-rule_name]避免在不必要的方向上搜索。模块化证明将大定理的证明分解成多个独立的引理lemma。每个引理单独证明和缓存。当证明顶层定理时只需apply这些引理可以避免重复计算。利用外部求解器对于纯粹的大规模布尔可满足性问题SAT在策略中适时调用sat或smt策略链接到 Z3 等高性能外部求解器通常是最高效的方式。代理可以配置为在检测到目标是典型的 SAT 问题时自动调用。增量与缓存lake构建系统和 Lean 的编译内核会缓存已编译的.olean文件。合理组织你的代码文件使得修改一个模块时不需要重新证明所有不相关的模块。5.5 与现有工具链的集成CircuitProver 不是要取代现有的仿真或商业形式化验证工具而是互补。规格对齐可以用 CircuitProver 来形式化定义芯片的顶层接口协议如 AXI 一致性属性然后使用这个形式化规格作为黄金参考来编写 SystemVerilog Assertions (SVA) 或指导仿真测试点的生成。等价性检查的补充商业等价性检查EC工具能高效处理门级网表与 RTL 的等价性。但对于算法级变换如不同的乘法器架构或涉及复杂控制逻辑的等价性可以先在 CircuitProver 的行为级或高级 RTL 级进行证明为 EC 工具划定一个更可靠、更抽象的验证范围。形式化属性导出可以将 CircuitProver 中证明的关键属性以某种标准格式如 SVA 或 PSL导出直接嵌入到 RTL 代码中供仿真和动态验证使用实现形式化与动态验证的闭环。6. 常见问题与排查思路在实际操作中你肯定会遇到各种错误和卡点。下面是一些典型问题及其解决思路。问题现象可能原因排查与解决思路lake build失败提示找不到Mathlib依赖配置错误或网络问题。1. 检查lakefile.lean中mathlib的 Git 地址是否正确。2. 运行lake update强制更新依赖。3. 检查网络连接特别是访问 GitHub 是否顺畅。导入CircuitProver时报告未知标识符CircuitProver 库未成功安装或版本不匹配。1. 确认lakefile.lean中require circuitprover的路径正确。2. 运行lake build查看具体编译错误。3. 检查 CircuitProver 库所需的 Lean 版本是否与你安装的版本兼容。证明过程中simp或rw策略无效目标形式与规则不匹配或定义未展开。1. 使用unfold或dsimp展开目标中的函数定义。2. 使用set_option trace.Meta.Tactic.simp.rewrite true开启simp的详细跟踪看它尝试应用了哪些规则为什么失败。3. 检查你要使用的引理lemma的前提条件是否在当前上下文中满足。证明状态中出现大量无法自动解决的琐碎子目标自动化策略如bitblast产生了过多分支。1. 尝试使用;操作符批量应用策略如all_goals { try simp }。2. 考虑是否证明策略过于“暴力”是否需要手动引入更聪明的中间引理来简化问题结构。3. 对于布尔等式可以尝试调用decide策略它使用决策过程decision procedure来判定可判定的命题。证明一个关于BitVec n的性质但归纳法induction n失败对BitVec n直接进行归纳可能不直接因为它的定义可能不是简单的结构归纳。1. 尝试对索引i : Fin n进行归纳或者对自然数n本身进行归纳并在归纳步骤中利用BitVec的构造子如cons和tail来建立联系。2. 查看 CircuitProver 或Mathlib的BitVec库中是否有现成的归纳原理如bitvec.induction_on可以使用。使用sat策略超时生成的 SAT 问题过于复杂。1. 尝试在调用sat前先用simp或手工have一些引理来简化目标减少变量和约束数量。2. 考虑将问题分解成几个更小的子问题分别用sat解决。3. 检查外部求解器如 Z3的路径是否正确版本是否兼容。定理陈述看起来正确但就是证不出来定理本身可能是假的或者你的形式化模型与直觉有细微差别。1.构造反例尝试用#eval命令或写一个小测试程序给定理的输入赋一些具体的值看看结论是否成立。这是发现建模错误最快的方法。2.简化问题尝试证明定理的一个特例例如将位宽n固定为 1 或 2。如果特例都证不出来那很可能定理陈述或模型有问题。3.寻求帮助将你的问题最小化后在 Lean 或 CircuitProver 的社区如 Zulip 聊天频道提问。提供完整的、可运行的代码片段。最后我想分享的一点个人体会是使用 CircuitProver 这类工具进行硬件验证其价值不仅在于最终那个“QED”证明完毕的标记。更重要的价值在于形式化思考的过程。为了写出能被 Lean 接受的定理你必须极端精确地定义电路的行为这迫使你提前发现规格中的歧义、接口定义的不完整、甚至设计逻辑的潜在漏洞。这个过程本身就是对硬件设计一次无与伦比的深度审查。即使证明没有完全自动化你在尝试形式化过程中获得的深刻理解也足以大幅提升设计质量。把它看作是一个与机器协作、共同进行深度设计思考的伙伴而不仅仅是一个自动化的证明生成器你会从中获得更多乐趣和收获。