企业官网建设流程全解析

打开搜索引擎找“模型检测”，前几条大概率是目标检测、版面检测、漏水检测这些深度学习视觉模型的新闻。但在形式化验证圈子，“模型检测”完全是另一套东西——不是训练神经网络找缺陷，而是用数学方法证明一个系统在所有可能执行路径下都不会出事。KeYmaera这个名字，就是这条冷门技术路线里一个挺特别的存在。

这工具全名是KeYmaera X，前身叫KeYmaera，卡内基梅隆大学那边维护的开源项目。我第一次接触它是在做无人车决策模块安全性评估的时候，当时需求很简单：想让自动驾驶系统在数学意义上“证明”自己不会撞车，而不是靠跑几万公里路测说“大概率不会撞”。这一搜就搜到了KeYmaera，也彻底改变了我对验证工具的认知——它不是传统意义上的状态穷举式模型检测器，而是一个基于微分动态逻辑的混合系统演绎验证工具。

这篇文章适合这几类人看：打算给机器人、无人机、汽车控制等带连续物理过程的系统做安全验证的工程师；已经用过NuSMV、SPIN、UPPAAL等经典模型检测器、想进一步处理连续变量的研究者；还有单纯好奇形式化验证怎么跟真实物理世界打交道的同学。我会从原理、实操、踩坑、选型这几个角度，把这几年用KeYmaera X的真实体感写出来。

1. 传统模型检测查不到的地方：连续世界与离散决策的交界

1.1 混合系统为什么让状态枚举失效

把“模型检测”这门学科打开，早期最辉煌的成果都是针对有限状态系统的。NuSMV把系统写成有限状态机，SPIN用Promela描述异步并发协议，UPPAAL通过时间自动机处理带时钟约束的实时系统。它们共同的内核是：把系统的所有可能状态构造成图，然后做图搜索——安全属性不成立，就给你一条反例路径；成立，就返回一个证明。

这个思路在数字电路、通信协议、并发软件里非常管用。但一旦系统里出现连续变量，状态空间就变成不可枚举的了。举个例子：一辆车以速度v行驶，制动时加速度是a，位置和速度都在实数空间里连续变化。你没法用有限个状态节点去穷举“速度每秒变化的所有数值”，因为它就是一条微分方程的解曲线。

这类系统有个专门的称呼——混合系统（Hybrid System）。离散部分负责决策，比如“当前距离小于阈值就刹车”；连续部分负责物理演化，比如“刹车之后车速按v' = -a衰减”。验证一个混合系统是否安全，要同时处理程序分支、循环、微分方程演化，传统状态搜索立刻失灵。

我刚入行时拿UPPAAL去建一个最简单的刹车模型，用离散时间步进模拟连续减速，代价是时间粒度必须足够细才能保证精度，而粒度一细状态数就爆炸。这个矛盾不是工程调参能解决的，是建模方式本身的数学缺陷。

1.2 仿真、测试与验证的边界

很多人问：我直接写一个仿真器，把各种极端工况都跑一遍，不也能说明系统安全吗？

仿真和测试确实能找到大量bug，但它们是“路径采样”，不是“路径证明”。一个控制器有100万个可能的初始状态和输入组合，仿真跑1万组，只能覆盖1万条轨迹；剩下99万个里只要有一条危险轨迹，就是重大事故隐患。对航天器、自动驾驶、医疗设备这种场景，“测过很多次”和“数学上证明安全”之间有本质区别。

形式化验证要填的就是这个坑。KeYmaera不是先跑一堆轨迹再统计结果，而是从公理出发，对“所有满足初始条件的执行路径”做逻辑推导。它给出的结果是：如果数学建模准确，那么安全属性在所有路径上都成立，或者给出一个数学意义上的反例。

这也就是为什么KeYmaera在学术圈里讨论度一直不低，但在工业界推开很慢——推导过程本身有门槛，而且建模环节的误差会直接影响结论可靠性。不过真要用到需要“可解释的安全证明”的场景，比如自动驾驶安全论证、飞行器控制适航评估，KeYmaera这条路几乎绕不开。

2. KeYmaera X的推理引擎：微分动态逻辑怎么“算”安全

2.1 dL的一种直觉理解：把程序和微分方程放进同一个公式

KeYmaera X的理论基石是微分动态逻辑（differential dynamic logic，简称dL），由André Platzer系统提出。这里不打算堆数学符号，我说一种便于建立直觉的理解方式。

普通霍尔逻辑里，我们用前置条件、程序、后置条件来描述“如果执行前满足P，执行完程序α之后一定满足Q”，写成P → [α]Q。dL做了一件很自然的事：让程序α除了普通赋值、if-else、循环之外，还能包含连续的微分方程演化，比如(x'=v, v'=-B, t'=1 & v≥0)，意思是“系统按照这组微分方程连续运行，直到v≥0这个域约束不再成立为止”。

这样的话，一个带刹车的汽车模型可以写成类似这样的公式：

v≥0 ∧ x≤D → [ (x'=v, v'=-B, t'=1 & v≥0) ] (x≤D)

翻译成人话就是：在车速非负、初始位置在安全距离D之内的前提下，只要车辆开始以减速度B连续刹车，那么在任何时刻位置x都不会超过D。方括号带公式符号的意思是“所有执行路径、所有到达状态都满足后件”，这正是安全属性的逻辑表达。

有了这种表达方式，KeYmaera就能把“验证系统安全性”转化为“在逻辑演算系统里证明这个公式”。dL还设计了一整套证明规则，比如对微分方程要找到微分不变式（differential invariant）、对循环要找循环不变式（loop invariant），这些规则把连续系统的验证问题拆成一系列代数与逻辑子目标，就像数学归纳法一样——“初始情况成立，且每一步演化保持成立，于是永远成立”。

2.2 KeYmaera X的工作方式：证明树与交互式战术

KeYmaera X和很多自动定理证明器一样，采取的是“与用户协作构建证明树”的方式。

你写一个.kyx文件，里面分三段：ProgramVariables声明变量，Problem描述要证的公式，Tactic给出证明策略。然后KeYmaera X根据策略自动挑规则去化简公式。能自动消解的子目标直接消掉，消不掉的就把当前节点留在证明树上，等用户指定下一步用哪条规则。

这就引出了工具的第一个显著特点：交互性极强。它不像NuSMV那样敲一条命令然后等结果，更像你在跟一个非常聪明但需要引导的助手一起解题。助手能熟练执行几百条推理规则，但你得告诉它往哪走。

Tactic脚本是这个工具最需要适应的地方。新人拿到的第一个例子，官方都会提供一个写好的策略，通常几行就能跑通：

tactic auto

这句的意思是让系统尝试自动搜索证明。对入门级模型，auto往往真能一路推完，这一步比很多人的预期自动化程度高不少。但等模型复杂一点，auto就会卡在中途，此时需要拆出子目标，针对某个ODE专门使用diffInvariant规则引入不动点的不变式，再用diffSolve求解微分方程、用QE做量词消元。

“auto能跑通一切”是新手常有的幻觉。真实项目里大半工作量都在反复打磨Tactic策略，把一个大而难的问题分解成若干能自动证明的小目标。

2.3 为什么需要人在回路上：自动程度的真相

有朋友问，既然是证明器，为什么不设计成完全自动，像模型检测器一样输入模型自动出结果？

问题的根源在于不可判定性和复杂性。带微分方程的实数算术逻辑本身就没有完整的自动化算法，哪怕限制到多项式系统，量词消元的计算代价也高得离谱。KeYmaera X选择了“人机协作”这一中间路线：机器负责精确执行推理规则，人负责提供关键的不变式和证明结构。这跟Coq、Isabelle/HOL这类通用证明助手的思路一致——机器不会让你蒙混过关，但也不会替你想出全部证明思路。

所以别把KeYmaera X当成“自动验证按钮”。把它当成一块白板加一个计算能力极强的推理引擎，你出思想，它出精度。

3. 从零跑通一个KeYmaera X验证任务

3.1 环境准备：JDK、sbt与KeYmaera X安装

KeYmaera X的安装路径非常“极客”：源码托管在GitHub上，基于Scala生态，启动方式跟很多JVM项目一样。我建议在Linux或macOS上面跑，Windows虽然也能弄，但容易在sbt下载依赖时遇到各种小麻烦。

最基础的依赖是JDK、sbt和Git。版本上我用JDK 11或17都正常，更老的版本可能编译报错，太新的版本偶尔会跟Scala编译器有兼容问题。装好之后把项目克隆下来：

git clone https://github.com/KeYmaeraX/KeYmaeraX.git cd KeYmaeraX sbt run

第一次编译会下载一大堆依赖，国内网络环境下这一个步骤就能劝退不少人。两个缓解办法：一是挂好镜像源，二是耐心等，sbt下载依赖断断续续时重跑sbt run一般能续上。

启动成功后会出现图形界面。左边是模型浏览器，打开自带的demo文件就能看到大量验证好的例子，右边是证明管理区。这一步对新手非常友好，比纯命令行友好太多。如果只想跑批处理，也可以用命令行加参数指定.kyx文件，我在CI脚本里跑回归测试时经常这么干。

3.2 第一个模型：水箱水位的连续切换控制

接下来做一个非常经典、但我认为特别适合入门KeYmaera逻辑的水箱水位控制模型，能直观展示混合系统的“连续演化+离散切换”是怎么回事。

问题是这样：一个水箱里水量为x（归一化到0到M之间），底部持续排水，排水的速度视为常值，即x' = -1。控制器在监测到水位低于某个阈值low时打开进水阀，进水时水位以x' = 1的速率上升；水位高于上限high时关阀。要证明的是：只要初始水位在[low, high]区间内，并且阈值设置得合理，水位永远不会降到低于low、也不会超过high。

这本质上是一个连续时间、事件触发切换的混合系统。用dL的语法描述，离散部分是控制器根据水位大小决定阀门开关，连续部分是微分方程x' = -1或x' = 1。我们把这个过程反复执行很多轮，要证明无条件安全。

如果写成近似KeYmaera风格的模型骨架，大概长这样（为了便于理解，忽略一些语法装饰，真实运行时请参考官方示例调整）：

ProgramVariables real x; End Problem x >= 0 & x <= M -> [ { f(x); }* ] (0 <= x & x <= M) End

这里f(x)里描述一次控制周期：if x < low then { x' = 1 } else { x' = -1 }。验证的核心目标是循环不变式：0 ≤ x ≤ M。只要初始状态满足它，且一次控制周期执行完后仍然满足，那么不管循环多少次都安全。

这看起来像废话，但正是形式化验证的日常——所有推理都围绕“找不变式”展开。

3.3 证明中的关键一步：找不变式

真正动手证明时，最大的挑战不是理解语法，而是找出那个足够强又足够简单的不变式。

水箱模型里，最直接的不变式是0 ≤ x ≤ M，但它不够。因为在关闭阀门、水位持续下降的阶段里，如果控制器的阈值low离0太近，水可能在阀门打开的瞬间之前就耗尽。所以实际证明里要分析清楚“关阀和开阀这两个离散分支的最低点”：

• 当x≥high时关阀，x以斜率-1下降；安全要求是x不会在下一次被检测到低于low之前跌破0。
• 当x<low时开阀，x以斜率+1上升；安全要求是x不会超过M。

如果这个控制器是连续监测、瞬时切换的，其实很简单：关阀后x最多降到low，只要low>0就永远不会到0；开阀后x最多升到high，只要high<M就永远不会溢出。但实际系统里往往存在检测周期和处理延迟，把这些延迟建模进去之后，不变式就得改成“水位在一轮控制周期内最多下降δ·1的距离”，于是low必须大于δ才能保证不干涸。

这个例子想说明的是：不变式不是天上掉下来的，它来自对物理过程和安全边界的量化分析。KeYmaera X只是帮你验证“这个不变式是否成立”，而寻找不变式始终是人的工作。这也是我目前认为KeYmaera最核心的思维门槛。

3.4 运行与观察：证明树、战术、批处理

模型写好后，在KeYmaera X界面里点“Run Tactic”，会在窗口底部生成一棵证明树。树的根是要证的公式，每个分支是一次推理规则的应用，所有叶子节点都是“closed”时，证明完成。看到这个状态，你就能非常有底气地说：这个模型在这个性质上是数学可证明安全的。

我们还可以把证明结构导出为PDF或文本，作为工程文档的一部分提交给评审。这一点在涉及功能安全的项目里价值很大——你给专家看的不是“测了很多次”，而是一棵结构清晰的数学证明树。

如果要在自动化流程里批量验证多个模型，可以写sbt命令行任务：sbt "runMain edu.cmu.cs.ls.keymaerax.launcher.KeYmaeraX test.kyx"，脚本里跑完检查退出码就能接进CI。我在做模型参数回归时会把多组阈值写成多个.kyx文件，循环调用，一旦某个参数组合导致证明失败，立刻能定位到是哪组阈值破坏了安全条件。

4. 真实项目里容易踩的五个深坑

4.1 不变式猜错，证明卡死：差在哪？

最典型的失败现场：你写了一个看似完美的不变式，auto策略跑了几秒，然后卡在一个代数子目标上怎么都过不去。

这时候别急着怀疑工具。回到物理过程去检查，八成是不变式遗漏了某个边界条件。比如刹车模型里，你只用了“位置不超过D”做不变式，却忘了考虑刹车过程中速度不能为负，于是微分方程在速度降到0之后继续反向加速（因为模型里没限制v≥0），就会推出一个反直觉的反例。KeYmaera X特别喜欢用这种“反例”打脸粗糙建模。

我的经验是：每写一个不变式，先在纸上把“初始成立、演化保持、安全推出”三个方向都写清楚，再丢给工具验证。工具不会给你讲情面，它只会精确地告诉你哪一个步骤断裂了。

4.2 非线性连续动态：证明器也有力所不及

KeYmaera对线性ODE、多项式ODE的处理能力很强，但加入非线性项之后问题会变得极为困难。比如一个带空气阻力（速度平方项）的刹车模型，v' = -B - c·v²，很多证明规则会失效，因为微分不变式在非线性项下很难闭合。

这不是你使用姿势不对，而是数学本身困难。KeYmaera社区的普遍处理办法是：证明阶段先用保守的线性模型得到结论，再把非线性因素作为扰动边界纳入考虑；或者结合数值可达性分析（比如Flow*），用近似方法补足非线性部分的可信度。纯逻辑验证能做，但代价和门槛会大幅上升。

4.3 建模假设与真实代码的语义鸿沟

这是我认为KeYmaera最需要警惕的坑：你在.kyx里把控制器建模成“瞬时检测、瞬时切换”，但真实控制器是跑在单片机或Linux进程里的，有采样周期、计算延时、执行器响应时间。模型里的“瞬时”在真实世界里根本不存在。

应对方法是把非理想因素显式建模进模型里：把延时建模成一个计时器变量ε，在连续演化过程中不断增长，控制器的决策只在ε达到某个值时发生。这样KeYmaera证明出的安全结论才真正覆盖了带延时的物理系统。

还有人会忽略浮点数和实数的差异。dL里的变量都是实数，数学上连续、精确；实际代码里的浮点运算有舍入误差。理论证明并不自动覆盖这个误差。工业实践中要在硬件模型里加入误差界，或者退而求其次说明“在误差界足够小的情况下，安全边界仍有裕量”。

4.4 自动机思维惯性：把离散系统经验硬套到连续系统

用过SPIN或者NuSMV的人，很容易把KeYmaera X想象成“一个能处理连续变量的模型检测器”，然后拿建模离散并发系统的方式去写混合系统模型，误以为给每个连续变量设定几个离散档位就能近似。

这是方向性错误。KeYmaera的价值恰恰在于不需要对连续变量做离散化近似，它直接在实数连续域上进行推理。强行离散化既丢精度，又会让状态空间复杂度失控。建模时应该尊重“微分方程与实数变量”这套世界观，用物理定律写出演化过程，而不是用枚举法去模拟它。

4.5 工具链与协作：版本、环境和团队门槛

KeYmaera X目前还不太像工程软件，没有一键安装包，也没有公司提供商业支持，版本更新时API和Tactic语法可能不兼容。团队协作时最好统一锁版本，把整个项目用一个Docker镜像固化下来，避免某人本地的sbt缓存不同导致证明结果不一致。

还有团队门槛问题。让团队里每个人快速学会dL和Tactic不算容易，建议至少有一名熟悉逻辑或定理证明的“种子选手”先跑通一个完整案例，再给团队做一次内部分享。形式化验证这种东西，靠个人埋头学很容易放弃，有个人带一带效率完全不同。

5. 横向对比：KeYmaera在工具谱系里的准确位置

5.1 工具型录：模型检测器、定理证明器与可达性分析器

我列了一张表，是这些年做选型时常用到的对比思路：

这里面很容易有的误区是把Flow和KeYmaera当同一类东西。Flow给出的是一个数值上近似可达集，计算速度快很多，但结论受误差影响；KeYmaera给的是逻辑上严格的证明，更重，结论更强。两者不是替代关系，工程上经常搭配使用：先用Flow*做快速探索、找反例，再用KeYmaera把关键安全边界“锁死”。

5.2 选型决策链：什么情况选哪把刀

我现在做选型，基本按一条决策链走：

1. 系统里有没有微分方程描述的物理量？没有的话，优先考虑传统模型检测器，不要杀鸡用牛刀。
2. 有连续动态，但只想要近似结果或快速找反例？用Flow*、SpaceEx这类数值可达性工具。
3. 有连续动态，且必须给出绝对数学意义的安全保证？优先KeYmaera X，或泛化到某个定理证明环境。
4. 团队里有没有人能在几周内上手逻辑证明？没有而项目又着急出结果，就必须认真评估时间成本；KeYmaera的学习曲线不是线性，而是有一个明显爬坡阶段。

另外别忘了仿真测试的位置。KeYmaera证明“模型安全”之后，仿真和路测仍然必要——毕竟模型是现实的近似，最终还是要回到真实代码、真实硬件上做回归测试。形式化验证替代不了现实的最后一道检查，但它能把大量危险情况挡在路测之前。

6. 给后来者的学习路径与我的体感

6.1 入门资料怎么选

KeYmaera X最该看的不是零散博客，而是官方Wiki和Platzer那本《Logical Foundations of Cyber-Physical Systems》。这本书从零开始建立dL，前几章没有复杂数学背景也能跟上，配套的课程练习直接对应KeYmaera X里的例子，边看书边跑工具，效果极好。

还有一个我推荐反复读的官方例子集，里面涵盖直道驾驶、转弯控制、空中交通管理等经典模型。每读完一个模型，不要让auto一键证明完就关掉，手动把证明树展开看看每一步都在干什么，等你能预测“这个循环需要用什么不变式”时，才算真正上手了。

6.2 阶段式学习路线

我建议三条阶段式路线：

• 第一阶段：跑通官方tutorial的界面操作，熟悉建模语言和Tactic基础，做到能给自己的小模型写一个简单证明。
• 第二阶段：手动给一个经典模型设计并证明不变式，比如把水箱控制增加采样延时，观察证明难度如何变化。这一步能建立对“建模粒度”的敏感性。
• 第三阶段：把工具接入自己的工程场景，用Docker固化环境，在CI里跑回归验证，形成可维护的模型库。到这一步，你才算从一个工具使用者变成一个能长期交付验证成果的工程师。

如果只想评估这个工具值不值得学，我建议直接跳到第二阶段，花一个周末把水箱模型加延时改造一遍。在这个过程中你就能体会到，这个工具最大的成本不是安装和语法，而是逼你把系统想清楚、把不变式找出来的那份“数学洁癖”。

就我个人的体会，KeYmaera X做起来是有种痛苦又上瘾的状态：痛苦在建模不完整时，它会一遍遍用失败提醒你“你的系统里有你根本没意识到的漏洞”；而上瘾在你真正发现一个用测试很难察觉的安全边界问题时，那种“这台机器帮我证明了一件只靠直觉完全推不出的事”的成就感，确实值得为之投入。无论你最后用不用这个工具，这轮训练建立的“把每个控制决策都当成可证明断言来审视”的习惯，都会在后来的技术生涯里持续起作用。