在 Isabelle 工程项目里待过一段时间的人大概都经历过这样的时刻昨天还能顺利done的证明今天因为某个函数定义增加了一个分支、某个递归结构变了重新跑一次却红掉大片。此时我们要面对的不是“这个证明怎么从零开始写”而是“一个已经过期的证明还有没有机会抢救回来”。这个问题在定理证明领域里有一个专门的名字Proof Repair。当它前面再加上 Contract-Aware也就是“基于合约感知的证明修复”理解角度又会不一样。CAPRI 这个名字本身其实把 Isabelle 开发中的一个长期痛点给点了出来证明不是写完就结束它会在代码与规范不断演进的过程中持续损坏而真正昂贵的不是第一次书写证明而是后续没完没了的修补。这不是一篇 CAPRI 的官方使用手册更多是基于主题本身的工程化拆解。如果你正在用 Isabelle、Coq 或其他交互式定理证明器又经常被“代码一改、证明全红”折磨这篇内容也许能给你一个更结构化的应对思路。1. Proof Repair 要回答的不是“证明怎么写”而是“证明坏了以后怎么救”1.1 为什么 Isabelle 里的证明会随代码变更一起“过期”Isabelle 对正确性的验证是机器检查的。你的定理、引理、证明脚本只要通过内核检查就说明在当前的定义和逻辑环境下它是成立的。问题在于这个“当前环境”不是静止的。真实项目里函数定义会变数据类型会加构造子引理签名会调整前置条件会收紧或放宽。每一次这样的变化都意味着所有依赖旧版本的证明都需要重新经过内核检查。许多证明脚本看着像一段文本但里面大量步骤其实建立在对某个递归定义具体形态的假设之上。比如auto能不能自动闭合目标取决于函数定义的等式形状induct能不能顺利推进取决于归纳原则是否还覆盖新增的分支。定义一改这些隐性依赖全部落空。更麻烦的是定理证明器的报错不像普通程序那样会告诉你“这里空指针了”。很多证明脚本的失败误差来自几十行之前某个策略的展开结果。你要同时理解原来的证明在说什么又得知道新定义和目标状态之间发生了什么冲突。这不是简单的 debug 思维能解决的问题。1.2 传统调试思维的三个坑我刚接触 Isabelle 时总喜欢拿运行时 debug 的经验去处理证明失败结果连续踩了三个坑。第一个坑是“看到失败就删证据”。很多开发者的第一反应是删掉中间的引理或步骤但一个引理往往不是孤立存在的它可能被后续七八个证明共同依赖。删除之后失败点会像多米诺骨牌一样蔓延。第二个坑是“只盯着出错的那一行”。证明脚本是状态依赖的目标能不能闭合取决于前面每一步是否生成出正确形态的子目标。真正的问题常常在出错位置之前的函数定义变体或归纳策略上。第三个坑是“试图在一个过期的上下文里做局部修补”。旧证明之所以失败通常不是因为某一个策略用错了而是证明所依赖的语义环境已经变了。这种情况下盲目用try、sledgehammer或手动堆策略也许能碰巧通过但你可能并不理解自己为什么通过。这也正是 Proof Repair 和普通证明补丁最大的区别。前者关心的不是“这一条引理怎么补”而是如何识别哪些证明步骤已经失去效力哪些可以复用哪些需要调整为新的合约形态。1.3 Promise: 把修复问题提上议程所以当我看到 CAPRI 强调 Contract-Aware 时我的第一反应是它尝试把“证明修复”从一件完全依赖个人经验的事变成一种可以被描述、被定位、被自动化辅助的工程流程。虽然名字里的 “Repair” 听起来像是事后补救但它真正解决的问题其实是 Isabelle 开发过程中长期被忽略的“证明维护成本”。2. Contract-Aware 究竟感知了什么变更合约才是修复地图2.1 合约在定理证明里的三层含义Contract 这个词很多读者可能更熟悉来自 JML、Dafny 或者设计契约理论它通常指前置条件、后置条件和对象不变量。但在 Isabelle/HOL 的语境里合约还可以有更宽泛的理解。一层是“定义层合约”。函数定义里每一个分支、每一条递归方程都可以理解成这个函数和外界之间的契约。调用者得明白它处理哪些输入也会大致猜到它产生什么输出。新增一个分支相当于修改了这条契约。第二层是“定理层合约”。一个lemma的陈述本身是一份合约它描述了什么条件下什么性质成立函数的输入输出约束都在这里体现。证明只是用来证明这份合约确实被当前代码满足。第三层是“证明脚本内部的局部合约”。一些中间引理承担着局部推导桥梁的作用它们通常不像主定理那样被文档化却常常是自动化证明能继续推进的关键。代码一改很多这类隐式中间引理最先失效。2.2 先看合约差异再谈修证明如果契约没有被显式表达修复旧证明就像是让维修师在不看图纸的情况下处理一台机器。他只能从报错和证明脚本反推原来的设计意图工作量大且容易出错。Contract-Aware 的核心思路是先把“变更前和变更后的合约差异”当成最重要输入。例如旧函数对某个输入返回完整列表新函数则增加了一个过滤条件。接下来要考虑的不是怎么让旧引理继续通过而是识别旧引理的结论在新合约下是否还成立。如果不再成立任何局部的策略修补都只是自欺欺人。真正的修复路径应该是先承认旧引理失效分析失效是因为新合约引入了新的边界情况还是因为旧合约的某些假设已被修改。接着再决定是否需要引入新引理或者是否可以把旧引理泛化成一个更一般的形式。2.3 CAPRI 的方法论启示给自动化修复补上“上下文”从名称和方向上看CAPRI 这类工作的一个重要价值是尝试把“合约差异”纳入自动修复的搜索过程。如果“修复程序”只学习语法层面的补丁很容易错过真正的语义变化。但如果它能先感知到哪里变了、变化边界是什么它就可以更有针对性地生成修复方案。这里需要区分事实与推测。至少从概念上“Contract-Aware Proof Repair”这个定义给 Isabelle 开发者提供了一个很好的提醒在你动手修复之前先给当前证明重新建立一份和代码对齐的上下文地图。地图不是证明本身但决定了修复从哪里开始。一个实用的经验是当新代码导致多个证明失败时不要立刻去改失败文件而是先整理一份从旧合约到新合约的差异清单哪怕它只是几行注释也能减少大量无效尝试。3. 一个最小可理解的证明损伤链过滤函数加了分支之后3.1 一次从可证明到不可证明的转折为了让“证明修复”更具体我举一个 Isabelle/HOL 里很常见的例子。先看一个简单的列表函数它保留列表里的全部元素fun collect_all :: nat list ⇒ nat list where collect_all [] [] | collect_all (x # xs) x # collect_all xs lemma collect_all_len: length (collect_all xs) length xs by (induction xs) simp_all这个引理很容易证明。收集完所有元素列表长度当然不变。现在需求变化了我们不想要0新函数collect_nonzero会把所有值为0的元素过滤掉。fun collect_nonzero :: nat list ⇒ nat list where collect_nonzero [] [] | collect_nonzero (x # xs) (if x 0 then collect_nonzero xs else x # collect_nonzero xs)这时候原来的collect_all_len已经无法直接迁移。因为collect_nonzero [0, 1]返回的是[1]长度显然不等于原始列表长度。如果你继续尝试用induction xs加上auto去证明同样的引理会失败在最根本的结论上。这里就是 Proof Repair 真正要处理的问题。旧证明之所以会失败不是因为哪一个证明策略写错了而是因为合约发生了变化新定义引入了“过滤语义”。3.2 自动化修复通常要经历的四步动作从工程角度看一个 Contract-Aware 的修复流程大致可以拆成下面四步这也比较接近我在理解 CAPRI 方向时的模型。第一步是“合约对比”。找出旧函数和新函数定义之间的差异。这里能看到if x 0这个新条件因此旧引理中“长度不变”的合约不再成立。这个动作看起来简单却是整个修复中最重要的一步。没有它后面的搜索都像蒙着眼睛打靶。第二步是“失效定位”。找到证明脚本中真正依赖旧合约的点。对于collect_nonzero失效点并不一定是最终的by命令而是归纳过程中对递归方程形态的依赖。定义多了分支自动化简规则就不再能覆盖所有情况。第三步是“修复决策”。判断旧引理应该被替换、泛化还是只能删除。在这里与其继续尝试一个错误命题不如把旧引理泛化成一个更精确的关系length (collect_nonzero xs) length (filter (λx. x ≠ 0) xs)。这个新引理不仅描述了新函数的行为也弥补了旧引理无法继续成立的空缺。第四步是“生成补丁并重新验证”。把新引理接入证明文件运行 Isabelle 内核检查。如果补丁通过才算修复完成。自动化工具在此过程中需要不断尝试不同的引理形态所以成本并不低。3.3 这里最难的其实不是语法补丁而是语义决策很多人会把 Proof Repair 想象成“找一条能通过的证明脚本”。但如果只是追求“能通过”Sledgehammer 加上随机策略也能碰出一些结果。真正困难的是判断结论是否与开发意图一致。继续用上面的例子。原目标length (collect_nonzero xs) length xs在函数增加过滤后本来就不应该成立任何让这条错误引理通过的修复都意味着问题的隐藏或误诊。Contract-Aware 的价值在于它能提前识别出这种语义冲突而不是让你浪费时间去寻找一个永远不会成立的证明。这个点也解释了为什么人工经验在 Isabelle 开发中仍然如此重要。工具的职责是帮助定位失效点、生成候选引理、压缩搜索空间但“这条性质是否仍然应该是代码的不变量”这个判断暂时仍然需要人来完成。4. 把 Proof Repair 变成日常工程能力的四条建议4.1 维护一份“合约变更日志”大多数 Isabelle 项目都有注释说明函数和定理却很少维护一份专门的“合约变更日志”。它不需要很长只需要记录每次关键定义变化时哪些函数签名、递归分支或定理陈述被修改哪些下游引理可能受影响。这份日志最大的意义是帮你建立增量修复顺序。如果函数 A 的改变会影响引理 B 和 C而 B 又是 C 的依赖那么先修 B、再修 C通常比随机修文件要快得多。它也能让后续加入项目的人知道为什么某些引理会呈现出奇怪的前提条件。4.2 每次批量修证明时按依赖顺序分诊真实项目里一次改动往往会让十几个证明文件变红。此时最忌讳的是“哪个先报错就先修哪个”。你需要先把所有失败任务按依赖关系排个序底层定义优先其次是直接依赖底层性质的中间引理最后才是靠这些引理撑起来的高层应用。这个过程很像系统故障排查不要先打表面补丁而是先定位哪一层坏了。如果基础定义层的变化导致大量后续引理需要重新表述那么顶层修复就要晚一点再做否则你很可能白修一遍。一个可以复用的排查顺序是确认代码变更是否真的被 Isabelle 正确加载。比较旧定义和新定义中函数签名的变化。找出失败引理中是否直接使用了旧的函数名、构造子或递归谓词。检查是否存在已经被用户删除或改名的中间引理。小规模运行单个失败证明观察当前目标和错误信息。判断是因为结论本身不再成立还是定义形态变化导致现有策略无法闭合目标。4.3 把修复后的证明提交成回归样本很多开发者在手工把证明修好后就当作任务结束。但这类问题几乎一定会再次出现。如果每修一次都只留下一个“现在能通过”的状态下一次问题复现时你还是得重新经历完整的定位过程。更稳妥的做法是在修复完成之后提交一个最小化的失败样例并让它进入回归集合。以后只要再有类似定义变化你就能通过回归测试第一时间发现哪条性质又被破坏而不是等到部署前才集中爆发。不要急着删掉那些曾经失败的引理痕迹。它们是后续修复最重要的参照样本。真正漂亮的 Isabelle 工程不是永不失败而是每次失败都能被快速归类、快速定位、快速修复。5. 适用边界什么项目适合 Contract-Aware Proof Repair5.1 真正适合它的是“长生命周期、规范频繁演进”的项目CAPRI 这类工作最有价值的地方可能不是帮你从零开始证明第一个定理而是减少“后续每改一次规范就得陪着一个历史证明文件打地鼠”的痛苦。如果一个项目满足以下条件那么引入 Contract-Aware 的修复思路会很有收益需要长期维护大量已经通过的证明例如操作系统模型、编译器形式化验证、协议安全证明。规范本身还在演进经常有性质调整、边界条件增加或函数结构变化。对证明的可追溯性有要求不只是“能通过”还希望知道每个证明在为什么契约负责。多个开发者协作维护 Isabelle 代码彼此对旧证明的意图不熟悉。在这种场景下自动修复能帮你快速定位“新合约和旧证明之间冲突在哪里”再配合人的判断来完成决策。5.2 需要谨慎的场景与两个前置条件也有很多场景不适合追求自动化 Proof Repair。第一类是不稳定探索阶段。如果你还在快速尝试各种定义证明本身就处于随时可能推翻的状态这时候投入精力维护可复用的修复流程有点为时过早。先跑通最小样例确认方向和目标后再开始沉淀证明资产。第二类是合约表达不清晰的历史项目。如果一个库里的函数和引理之间没有任何文档或结构化的合约说明自动化修复很难判断哪些差异是用户有意的哪些只是草稿遗留。使用 CAPRI 或类似工具前至少要确认两个前置条件当前 Isabelle 版本与工具版本兼容能在一个小仓库跑通最小修复样例并且你有能力判断工具生成的“通过补丁”是否包含不合理的删证或削弱结论行为。即使工具声称是自动化你仍然需要理解它为什么这样修。场景适合程度原因库长期演进有大量稳定证明高证明维护成本最高修复收益最明显代码原型探索定义频繁推翻低维护修复流程成本可能超过直接重写证明安全协议、编译验证等项目要求强追溯性高契约变化是关键证据需要记录修复动机单次教学演示、一篇论文里的示例低用例规模太小不值得引入额外工具流程6. 从 CAPRI 看定理证明工具链的下一个方向证明也需要维修经济6.1 证明资产的复用取决于你对失败原因是否有可解释的诊断Isabelle 的项目经验积累得越久越会发现证明资产的价值不在于单个工具能跑通而在于它可以被后续维护者理解和修改。如果失败时只能看到满屏红色而没有任何诊断信息说明“这条性质曾经对应哪份契约、为什么现在开始失效”那项目会越来越难维护。Contract-Aware Proof Repair 的更大意义是它把失败原因和合约差异联系起来了。它对“为什么这个证明需要修复”给出了一种可解释的回答而不是只给一个修复补丁。这种可解释性也是后续自动化工具真正的护城河。6.2 合约会成为人与自动修复工具之间最自然的对齐边界未来定理证明器的自动修复方式大概率不会越来越像一个神秘黑盒。相反人类开发者、AI 辅助工具和证明器之间会形成一个三角开发者维护契约工具在契约约束下搜索证明路径证明器负责最终检查。合约就成了人和机器之间最自然的接口。从这个角度理解 CAPRI你就不会只把它当成一个单纯为了“省几分钟修证明”的研究。它代表的是下一阶段交互式证明工具的开发方式让机器去承担那些可以被合约描述的重复修复工作让人去处理语义意图和性质取舍。6.3 最后的建议先从最小失败样例开始不要急于全自动如果你想让自己的 Isabelle 项目也获得类似收益我建议不要急着把希望寄托在某个全能修复工具上。先把一次失败的最小样例跑通记录从合约变化到证明失败之间发生了什么再尝试手工或半自动地完成一轮修复。这个最小闭环跑通之后再慢慢扩大范围。真正成熟的工作流不是给你一把能把所有红证变绿的神奇钥匙而是让你在代码演进的同时能快速知道每个证明和契约之间还有没有保持一致性。当你开始把证明当成需要随合约一起演化的代码资产而不是一次性通过的“字数兑换结果”CAPRI 这个方向才算真正用对了地方。