1. 项目概述当硬件验证遇上形式化证明最近在硬件设计特别是芯片和密码学电路验证的圈子里一个词被反复提及形式化验证。传统的仿真测试覆盖率再高也总有边角案例覆盖不到而一个微小的时序或逻辑错误在流片后可能就是灾难性的。我们团队在折腾一个高安全等级的密码协处理器时就深受其苦。仿真跑了成千上万个向量感觉稳了但心里那根弦始终绷着——真的没有隐藏的并发数据冒险吗那个精心设计的侧信道防御电路逻辑上真的无懈可击吗就在这时我们开始系统性地研究用定理证明器来做硬件的形式化验证。在众多工具中Lean 4及其强大的交互式定理证明环境吸引了我们。但很快我们发现了一个痛点硬件验证尤其是电路验证有大量重复性的、模式化的证明结构。比如验证一个加法器链的正确性或者证明一个状态机不会进入非法状态其证明思路和策略往往大同小异。每次为新电路从头开始写证明不仅效率低下而且容易因细节疏忽引入错误。于是CircuitProver这个项目的想法诞生了。它的核心目标不是从零开始教你怎么用Lean 4而是构建一个面向硬件验证场景、高度可复用的证明库Proof Library并探索如何用Agentic智能体辅助的方式来大幅降低定理证明的门槛和重复劳动。你可以把它想象成一个专为硬件工程师打造的“证明工具箱”和“智能证明助手”。它基于Lean 4预先封装了针对常见硬件组件如加法器、乘法器、多路选择器、有限状态机和常见属性如功能等价性、时序无关性、资源边界的证明策略和已证引理。当你需要验证自己的硬件设计用Lean 4或其它可导入的格式描述时可以直接调用或稍作适配这些“电路证明模块”而无需从最基础的逻辑规则写起。2. 核心设计思路库与智能体的双轮驱动CircuitProver的设计哲学建立在两个支柱上可复用的证明库和智能体辅助的证明流程。这两者相辅相成共同目标是让形式化验证变得像调用标准单元库一样自然。2.1 为何选择Lean 4作为基石在众多定理证明器如Coq, Isabelle/HOL, ACL2中我们选择Lean 4是经过一番考量的。首先Lean 4是一门真正的编程语言而不仅仅是一个证明脚本语言。它的元编程能力极其强大这允许我们以编程的方式组织和生成复杂的证明结构这是构建大型、结构化证明库的关键。其次Lean 4拥有活跃的数学社区和庞大的Mathlib库。Mathlib虽然主要面向纯数学但其严谨的基础设施如代数结构、范畴论为描述硬件特别是算术电路、代数电路提供了绝佳的理论基础。最后Lean 4的Elan版本管理器和Lake构建工具使得管理一个包含大量依赖的证明项目变得非常清晰和稳定。我们直接使用elan安装的稳定版Lean 4和lake来管理CircuitProver项目及其对Mathlib等依赖确保了开发环境的一致性。2.2 构建可复用电路证明库的核心理念这个库不是一堆零散证明的集合而是一个有层次、可组合的体系。基础层Primitive Layer这一层直接建立在Lean 4和Mathlib的基础上定义硬件验证的基本原语。例如我们定义了Bit类型虽然Lean本身有Bool但我们可能需要包装以表示电路中的一位信号、Signal n表示n位宽的向量信号、以及时钟、寄存器等概念。更重要的是定义硬件描述语言HDL的语义模型比如如何将Verilog中的一个always (posedge clk)块映射为Lean中的一个状态转移关系。组件层Component Layer这是库的核心价值所在。我们为常见的硬件模块预置了形式化规范和证明。组合逻辑电路如与门、或门、非门、加法器全加器、行波进位加法器、乘法器阵列乘法器、Booth编码乘法器、比较器等。对于加法器我们不仅证明其功能正确性a b sum还可能证明其输出延迟与位宽的关系作为属性之一。时序逻辑电路如D触发器、寄存器、计数器、有限状态机FSM。对于FSM我们提供模板来形式化定义状态集、转移条件并证明其不会进入死锁状态或未定义状态。接口与协议如简单的握手协议Valid/Ready、FIFO的抽象模型。证明其不会丢失数据或发生溢出。每个组件都以“模块Module”的形式提供包含该组件的接口声明输入输出端口、功能规范用Lean命题描述、以及一个或多个已经完成的证明Proof。用户在自己的项目中可以像导入软件库一样导入这些模块然后通过“实例化”来应用到自己具体的电路实例上。策略层Tactic Layer为了更方便地使用这些库我们封装了一系列自定义证明策略Tactic。例如一个circuit_simp策略可以自动化简由标准逻辑门组成的组合逻辑表达式一个verify_fsm策略可以引导用户完成状态机可达性分析。这些策略背后是大量对Mathlib和基础层引理的巧妙运用。2.3 Agentic证明从手动推导到智能辅助“Agentic”在这里指的是引入一个证明智能体的概念。这个智能体不是完全自动化的证明器而是一个交互式证明环境中的高级助手。它的工作流程可以概括为目标理解当你写下要证明的定理例如“我的这个8位加法器模块满足其功能规范”后智能体会分析该目标的结构。库匹配与建议智能体扫描CircuitProver证明库寻找与当前目标匹配的已证明组件或引理。例如它可能发现你的加法器结构与库中的“行波进位加法器Ripple Carry Adder”模板高度相似。策略生成与填充智能体会建议你应用库中的哪个证明模板并自动生成一部分证明脚本骨架。它可能会说“检测到您正在验证一个RCA库中存在通用证明策略prove_rca是否应用应用后将需要您为具体的位宽n8和输入信号a, b提供实例。”交互式补全在用户提供实例后智能体会尝试自动完成剩余的、可模式化的证明步骤。对于无法自动完成的部分通常是设计特有的逻辑它会停下来给出清晰的子目标提示并可能建议下一步可用的策略或引理。这个过程极大地减少了用户需要记忆的繁琐语法和策略名称将精力集中在高层的设计逻辑对应上。这个“智能体”本质上是我们编写的一系列启发式规则、模式匹配脚本和证明搜索算法的集合它运行在Lean 4的交互式证明引擎如VS Code的Lean插件之上。3. 实战从零验证一个简单电路让我们通过一个最简单的例子——验证一个1位全加器Full Adder——来直观感受CircuitProver的工作方式。全加器有三个输入加数a、b和进位输入cin两个输出和sum和进位输出cout。其逻辑关系是sum a xor b xor cincout (a b) | (b cin) | (cin a)。3.1 环境准备与项目初始化首先确保你安装了Lean 4的稳定环境。我们推荐使用elan来管理Lean版本。# 安装elan如果尚未安装 curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh # 重启shell或source环境变量后安装Lean 4稳定版 elan default stable # 使用lake创建一个新项目 lake new MyFullAdderVerification cd MyFullAdderVerification然后你需要将CircuitProver库作为依赖加入。假设CircuitProver已发布为一个Lake包你只需修改项目的lakefile.lean-- lakefile.lean require CircuitProver from git https://github.com/your-org/CircuitProver.git main运行lake update来获取依赖。3.2 描述电路与定义规范在MyFullAdderVerification项目中我们创建一个新文件FullAdder.lean。首先导入必要的库import CircuitProver.Core -- 导入基础类型定义如Bit import CircuitProver.Primitives.LogicGates -- 导入逻辑门模型 import CircuitProver.Components.Arithmetic -- 导入算术组件相关引理接着我们用Lean定义全加器的功能。在CircuitProver的框架下我们通常先定义电路作为一个函数或一个结构体-- 定义全加器为纯组合逻辑函数 def full_adder (a b cin : Bit) : Bit × Bit : let sum : xor (xor a b) cin let cout : or (or (and a b) (and b cin)) (and cin a) (sum, cout)这里xor,and,or是来自CircuitProver.Primitives.LogicGates的已定义函数它们是对Lean底层布尔操作的包装但带有电路语义的标签便于后续证明策略识别。然后我们定义全加器应该满足的规范。规范就是我们要证明的定理Theorem-- 全加器的功能正确性定理 theorem full_adder_correct (a b cin : Bit) : let (sum, cout) : full_adder a b cin -- 规范1sum的定义 sum xor (xor a b) cin ∧ -- 规范2cout的定义 cout or (or (and a b) (and b cin)) (and cin a) : by -- 证明过程将写在这里 sorry -- sorry表示此处证明尚未完成是一个占位符3.3 应用证明库与智能体辅助现在到了关键步骤证明full_adder_correct这个定理。对于一个如此简单的电路我们可以手动展开定义来证明。但这里我们演示如何使用CircuitProver库的策略。首先我们尝试使用库中为组合逻辑电路提供的简化策略circuit_simp。这个策略知道如何处理and、or、xor等逻辑门函数的化简规则。theorem full_adder_correct (a b cin : Bit) : let (sum, cout) : full_adder a b cin sum xor (xor a b) cin ∧ cout or (or (and a b) (and b cin)) (and cin a) : by -- 展开full_adder的定义 unfold full_adder -- 此时目标变为 (let sum : xor (xor a b) cin; let cout : or (or (and a b) (and b cin)) (and cin a); (sum, cout)) ... -- 使用circuit_simp策略进行化简。该策略会自动处理let绑定和逻辑等式。 circuit_simp -- 经过circuit_simp处理后目标可能直接变为 True 或一个显然的等式 a a。 -- 如果是True我们可以用trivial策略结束证明。 trivial在实际的交互式开发中在VS Code中编辑并打开Lean Infoview当你写下circuit_simp并执行时Lean服务器背后有我们的库策略支持会进行一系列重写和化简。如果库的策略足够强大它可能会直接完成证明。对于这个例子circuit_simp很可能足以完成。但如果电路更复杂呢这就是“Agentic”部分发挥作用的时候。假设我们有一个更复杂的8位加法器它由8个全加器级联而成。我们可能这样定义def ripple_carry_adder (a b : BitVec 8) (cin : Bit) : BitVec 8 × Bit : ...对应的定理可能想证明它等价于整数加法。这时我们可以尝试调用库中为“行波进位加法器RCA”预置的证明策略theorem rca_correct (a b : BitVec 8) (cin : Bit) : let (sum, cout) : ripple_carry_adder a b cin (sum.toNat (cout.toNat 8)) a.toNat b.toNat cin.toNat : by -- 尝试应用通用RCA证明策略 apply_proof_template «RippleCarryAdder» (width : 8) (a : a) (b : b) (cin : cin) -- 应用后智能体会自动分解目标可能剩下一些需要用户提供的关于BitVec和toNat转换的引理。 -- 此时智能体可能会在Infoview中提示“需要证明引理 BitVec.toNat_inj...”并给出一个使用library_search策略的按钮建议。apply_proof_template是一个我们设想的智能体高级命令。它会根据你提供的组件名称和参数从库中提取对应的证明模板并实例化自动填充大部分证明步骤。用户只需要处理模板参数与当前上下文的适配问题。3.4 验证结果与解读当Lean的Infoview显示所有目标Goals都已解决出现“Goals accomplished ”或类似提示时证明就完成了。这意味着在Lean的逻辑框架内你的电路描述full_adder或ripple_carry_adder完全符合你写下的功能规范full_adder_correct或rca_correct。这不仅仅是“测试通过”而是数学上严格的“证明成立”。对于硬件工程师来说这个结果的可靠性是极高的。它意味着只要你的顶层规范定理陈述正确地刻画了硬件应有的行为例如加法器的输出等于输入的算术和并且你的电路描述Lean函数忠实地反映了RTL设计那么你就获得了该电路功能绝对正确的保证覆盖所有可能的输入组合。4. 深入核心证明库的架构与实现细节要构建一个实用的CircuitProver其证明库的架构设计至关重要。它必须兼顾灵活性、可扩展性和性能。4.1 分层抽象与接口设计库采用典型的分层架构每一层都提供清晰的接口API。最底层Lean 4 Mathlib。我们重度依赖Mathlib中的Data/Bitvec、Data/Fin、Algebra等库。例如我们用BitVec n类型表示n位宽向量其底层是Fin n → Bool。Mathlib已经为BitVec提供了丰富的算术和逻辑运算引理这是我们证明的基础。核心抽象层定义了Circuit类型类Typeclass。这是一个关键设计。我们不强制规定电路必须用某种特定方式如函数表示而是通过类型类来声明一个类型α可以视为电路。class Circuit (α : Type) where inputType : Type outputType : Type simulate (c : α) (i : inputType) : outputType -- 可能还有时序、面积等属性这样一个纯组合逻辑函数、一个带状态的状态机、甚至一个外部Verilog文件的抽象模型只要实现了这个类型类都可以被纳入我们的验证框架。模型层提供了几种具体的电路模型实现。Combinational (input output : Type)将纯函数input → output包装成电路。Sequential (state input output : Type) (next : state → input → state × output)用状态转移函数定义时序电路。Netlist一个更接近底层门级网表的结构化表示用于与外部EDA工具链对接。属性层定义了要验证的电路属性Property。例如-- 功能等价性电路c的行为等价于规范函数spec def functionally_correct (c : Circuit α) (spec : α.inputType → α.outputType) : Prop : ∀ i, c.simulate i spec i -- 时序无关性电路的输出只依赖于当前输入对组合电路而言 def combinational_property (c : Circuit α) : Prop : ...策略与自动化层这是用户直接交互的部分。我们构建的策略如circuit_simp、verify_combinational、induction_on_clock等内部会调用下层提供的引理和抽象接口。4.2 可复用证明模块的构造技巧如何让一个证明“可复用”核心在于参数化Parameterization和引理泛化Lemma Generalization。参数化证明我们不为一个特定的8位加法器写证明而是为一个抽象的n位加法器写证明。theorem ripple_carry_adder_general (n : Nat) (a b : BitVec n) (cin : Bit) : let (sum, cout) : ripple_carry_adder_n n a b cin (sum.toNat (cout.toNat n)) a.toNat b.toNat cin.toNat : by induction n generalizing a b cin with | zero ... | succ n ih ... -- 在这里归纳假设ih就是可复用的关键这个定理对任意位宽n都成立。当用户需要验证一个具体的8位加法器时只需用n : 8来实例化这个通用定理即可。构建证明“积木”将大证明分解成小引理。例如先证明1位全加器正确性full_adder_lemma再证明如何用full_adder_lemma和归纳法来证明n位加法器。这些小引理就是“积木”用户可以用它们搭建更复杂电路的证明。使用类型类进行重载对于常见的操作如“将电路转换为布尔表达式”我们定义一个类型类ToBoolExpr并为不同的电路模型Combinational、Netlist提供不同的实现。这样上层的策略如circuit_simp就可以通过类型类系统自动选择正确的化简方法无需关心底层具体是哪种电路表示。4.3 与现有硬件设计流程的集成CircuitProver不是一个孤立的工具它需要融入硬件设计流程。前端HDL导入。我们提供解析器或转换器将子集的Verilog/VHDL转换为Lean 4中的电路模型如Netlist。这是一个有挑战但并非不可行的任务可以从简单的、综合风格的RTL子集开始。中端属性描述。用户需要在Lean中编写形式化属性定理。为了降低门槛我们可以开发一种领域特定语言DSL让用户用更接近硬件断言如SystemVerilog Assertion的语法来编写然后由DSL编译器生成Lean定理。后端证明生成与检查。这是CircuitProver和Lean的核心工作。证明过程是交互式的但最终会生成一个完整的证明项Proof Term。这个证明项可以被独立地、高效地检查确保验证结果的可信性。输出证明成功则给出确定性结论证明失败则给出反例Counterexample或无法证明的子目标帮助用户定位设计或属性描述中的问题。5. 常见挑战、排查技巧与实战心得在实际使用Lean 4和构建CircuitProver的过程中我们遇到了不少坑也积累了一些经验。5.1 性能问题证明膨胀与编译时间Lean在编译大型项目尤其是包含Mathlib时时可能会比较慢。CircuitProver库本身也会变得庞大。应对策略模块化将库精细拆分使用lake的require机制按需导入。确保每个文件只导入它最小依赖集。增量编译利用lake build的增量编译特性。一次全编译后后续修改通常只编译受影响的部分。避免过度展开Unfolding在证明中谨慎使用unfold命令展开定义。过度展开会导致目标表达式急剧膨胀降低后续策略效率。优先使用已有的化简引理simplemmas或重写引理rewriterules。使用native_decide对于纯粹基于布尔代数和线性算术的有限位宽电路性质可以尝试使用Lean的native_decide策略。它调用外部求解器能非常快地解决一大类问题。5.2 证明困境目标复杂且无头绪面对一个复杂的验证目标不知从何下手。排查流程分解目标使用apply、intro等策略将顶层目标分解为若干个子目标。apply用于反向推理从结论找前提intro用于引入假设。查看定义对目标中不熟悉的符号使用#print命令或编辑器中的“跳转到定义”功能查看其精确定义。尝试simp和library_searchsimp尝试用已有的化简规则简化目标。library_search是神器它会在当前已导入的库中自动搜索能解决当前目标的引理。利用Mathlib很多硬件问题可以归结为数学问题。例如证明两个位向量相等可能转化为证明它们对应的自然数相等。多想想能否利用Mathlib中强大的代数、数论库。使用calc模式对于等式链证明calc模式能让证明过程清晰如演算纸。calc (a b) c a (b c) : by ring _ a (c b) : by simp [add_comm] ...5.3 与外部工具链的协同问题如何将芯片设计中的真实网表导入Lean进行验证当前实践我们开发了一个从简化版Verilog到LeanNetlist模型的转换器。它只支持一个RTL子集连续赋值assign、always (*)组合块、always (posedge clk)时序块的基本形式。对于更复杂的设计我们建议抽象建模在Lean中为关键模块如算法单元、控制通路建立更抽象但功能等价的模型进行验证而非验证每一个门。分层验证在高层用Lean验证算法正确性在底层用传统EDA工具验证时序、功耗等。Lean的证明提供功能正确性的“黄金参考”。5.4 团队协作与知识管理定理证明项目对代码和证明的严谨性要求极高团队协作需要规范。版本控制所有.lean文件必须用Git管理。lakefile.lean确保依赖一致。证明风格指南制定团队内部的证明书写规范比如何时用by块何时用tactic模式 vsterm模式如何命名引理lemma_about_thing风格。文档与注释为库中的关键函数和定理编写详细的文档字符串/-- ... -/。复杂的证明步骤需要注释说明意图。持续集成CI设置GitHub Actions在每次提交时自动运行lake build和lake test确保所有证明仍然有效防止回归。5.5 给硬件工程师的入门建议如果你是一名硬件工程师想尝试CircuitProver或Lean验证我的建议是心态转变这不是写测试而是写证明。你需要像数学家一样思考关注“为什么成立”而非“如何运行”。从小开始不要一开始就验证整个CPU。从一个1位全加器、一个简单的FSM开始感受定理证明的过程。善用社区Lean社区非常活跃。遇到问题在Lean Zulip聊天室或相关论坛提问时清晰地描述你的目标Goal和当前上下文往往能得到快速帮助。理解错误信息Lean的错误信息有时很晦涩。关键看最后几行它通常指出了类型不匹配、找不到实例或无法合成某个类型类等问题。逐步缩小问题范围。将证明视为设计的一部分形式化验证最好与设计同步进行。当你用Lean描述电路时这个过程本身就在强迫你更精确地思考设计这常常能提前发现模糊或矛盾的需求。构建和运用CircuitProver的过程是一个将硬件工程的严谨性与数学证明的精确性深度融合的旅程。它开始可能有些陡峭但一旦你习惯了这种思维并拥有了可复用的证明库和智能体辅助你会发现它为高可靠性硬件设计带来了前所未有的信心。这不仅仅是找到一个工具更是引入了一种新的、更坚实的设计方法论。