简介：一套围绕形式化Z语言及辅助工具Z-EVES的完整资源包，面向软件工程、安全关键系统方向的研究者、开发者和学生，解决Z规格建模与工具链搭建门槛高的问题。Z语言借助集合论与谓词逻辑精确描述系统状态，Z-EVES提供语法高亮、自动证明、模型检查和代码生成等能力，帮助使用者提早发现规格缺陷，提升软件可信度。包体小巧，共5个文件、约8.63MB，核心是两个可执行程序，另有PDF格式的用户指南、Windows专用安装说明和网页版快速上手文档；用户指南覆盖Z语言基础与Z-EVES操作，安装说明列出配置要点与排错思路，便于按需查阅。目前已有820人学习，无论初学者还是工程人员，都能快速搭建开发环境。通过程序与文档结合，读者可掌握域、Schema、谓词等核心概念，并利用交互式证明和模型检查验证系统性质，熟悉从规格到代码生成的衔接方式；这种从建模到验证的完整流程，可为航空航天、医疗或金融等可信软件设计提供坚实支撑。
1. Z-EVES：让Z语言从纸面规范走向可机器检查的证明工具
安全关键系统里，形式化规范写到一半，最怕的不是自己写错，而是所有人都只能靠肉眼评审去“感觉”有没有矛盾。Z语言表达能力强，Math 里的集合、关系、逻辑谓词写得很漂亮，可你越写越多，就越需要一个工具帮你确认：这些 schema 之间的推论到底成不成立、证明义务能不能每个都通过。Z-EVES 就是干这个的——它给 Z 语言提供语法和类型检查，再把规范翻译成集合论与一阶逻辑的谓词，交给证明器逐个验证。它不负责替你建模，只负责把你脑子里的逻辑漏洞结结实实挖出来。适合人群很明确：写过 Z schema 但没跑过证明器的人，以及被“手工审查太玄学、评审意见总在拍脑袋”折磨的工程师。我当年第一次把规范丢进 Z-EVES，它立刻指出一个我从来没注意到的偏序反自反性错误——从那天起，我就把这种检查当作写规范的下限而不是上限。
2. Z语言的形式化骨架：为什么Z-EVES能替你找出漏洞
2.1 从Schema到可证明的谓词：Z语言的最小样子
Z语言的核心构造是 schema，它把状态空间和约束打包成一个矩形块。一个最经典的例子是生日簿。用 LaTeX 风格写出来大概是这样：
\begin{zed} BirthdayBook known : \power NAME birthday : NAME \pfun DATE \where known = \dom birthday \end{zed}这里的\power NAME表示 NAME 的幂集，\pfun表示偏函数，\dom是定义域。整个 schema 声明了两个变量并规定不变量：已知的名字集合必须等于 birthday 函数定义域里的名字集合。单看这段文本，人眼很容易跳过“偏函数的定义域不包括未定义值”这一类细节，但 Z-EVES 会把known = \dom birthday当作一个谓词，在逻辑框架里展开成真正的等式约束。也就是说，它不关心你排版好不好看，只看每个符号对应的数学语义能不能自洽。
实际输入 Z-EVES 时，你大概率不会用这般高斯的 LaTeX 排版，而是用 ASCII 变体表示，比如%power NAME或者P NAME，具体取决于你拿到的版本把哪个输入语法当作默认。我的建议是：一开始就别选花哨的编辑器，先用最小 schema 去试工具认不认这套符号。我通常会准备一个只含一个空 schema 的文件，跑一遍语法检查，确认环境通了再开始写正经规范。
2.2 类型检查与证明义务是怎么来的
Z-EVES 的流水线可以拆成四步：解析、类型检查、规范化、生成证明义务。前两步和编译器很像——变量有没有声明、关系两侧的类型能不能匹配，这些基础错误在喂给证明器之前就被拦下来了。真正帮上大忙的是后两步。规范化会把 schema 翻译成一组逻辑谓词，然后根据你的命令生成 proof obligation，比如“初始状态是否满足不变量”“某个操作的输出类型是否合法”“某个前提是否能推出后置条件”。
这里我打一个比方：普通的类型检查器只能告诉你“你把日期塞进了名字里”，而 Z-EVES 的证明义务能告诉你“即使你把名字塞对了日期，可这个函数到底是偏的还是全的，相差的这页纸哪里漏了边界”。比如生日簿的初始状态定理可以写成∃ BirthdayBook' · known' = ∅，这看起来显然成立，但如果你忘了写birthday' = ∅或者没封锁两个变量的关系，证明义务就会露出马脚。它把每个隐含假设都强制摆上台面，这正是“辅助工具”可以成为“事后后悔药”的原因。
2.3 为什么普通文本编译器和人眼检查不够
有不少人说“Z语言我写得很小心，不需要额外工具”。说这话的人通常在第三个 schema 出现时就开始抱大腿了。Z语言的数学类型系统比大多数编程语言严格得多——一个关系到底是\rel、\pfun还是\ffun，语义差别能决定一条定理是否可证。普通文本编辑器根本不懂\dom和\ran的语义，你用一个宏展开错了它也不会报警。人眼检查的问题更实际：你会下意识读自己想读的语义，而不是规范真实表达的语义。我见过一个团队连续审了三天，所有人都认定某个集合包含关系成立，结果 Z-EVES 一跑就发现有个 case 漏了空集合。从那以后，我的习惯是所有核心 schema 必须至少过一遍语法和类型检查，这是最低底线，不是可选项。
2.4 把规范喂给Z-EVES的第一次检查
先别急着写大项目，把上一节那个生日簿存成birthdaybook.zed，然后跑一次检查。常见做法是调用 Z-EVES 的命令行入口做类型检查，命令大概长这样：
zeves -t birthdaybook.zed-t是 type-check 的常见约定，表示只做解析和类型检查，不生成证明义务。输出会逐行列出检查到的 schema 名称和状态。如果文件里出现未定义变量、类型不统一、数学运算符两侧类别不匹配，它会给出带行号的错误信息。第一次跑通后，你会对这个工具的基本盘有直接感受：它不会给你解释“为什么不合法”，但会精确告诉你哪个符号在哪一行有了嫌疑，剩下的推导要靠你查上下文。
为什么要先跑这一步？因为 Z-EVES 是一个黑匣子味很浓的证明器，越早把输入格式和类型系统摸清，后面调证明策略时越不容易把语法问题和逻辑问题混在一起。我一般会把这个最小文件保留下来，之后每次换环境、换版本，都先拿它回归一遍语法检查，相当于给工具本身做一次冒烟测试。
3. 跑通Z-EVES的最小操作：从安装到生成证明义务
3.1 获取Z-EVES的三种常见途径与选择建议
Z-EVES 不是近几年的新玩具，它更像是形式化方法领域的一把老式军刀。获取它的常见途径有三条：一是直接拿预编译好的可执行文件，适合只想要命令行功能的人；二是从源码编译，适合需要改输出格式、或者要放到旧版 Unix 环境里的人；三是在虚拟机里跑带图形界面的版本，适合想逐步查看证明树的教学场景。我个人会优先选预编译，因为 Z-EVES 的命令行接口干净，图形界面反而让批量检查变得啰嗦。
拿到工具后第一件事不是写规范，而是确认运行环境。Z-EVES 对环境的挑剔程度接近古董级——它依赖很多传统库，如果你在太新的 Linux 发行版上编译，可能会遇到ld链接错误或者X11头文件缺失。遇到这类问题不要慌，常见做法是装一个老一点的虚拟机镜像，或者静态编译。我曾经为了在一个容器里跑通它，花的时间比写证明脚本还长，所以别低估这一步。提前把环境问题解决，后面才能专心处理证明义务。
3.2 创建输入文件：编码与命名约定
Z-EVES 的输入文件本质上是一个纯文本的数学规范，我建议文件名一律用小写加下划线，后缀用.zed。文件里不要出现中文注释和全角符号，更不要在字符串里塞智能引号——这个工具的解析器对非 ASCII 字符的容忍度很低，乱码问题会直接伪装成“表达式解析失败”，排查起来非常难受。
一个完整的输入文件除了 schema 定义，还可以包含定理声明和证明脚本。最小结构是这样：
\begin{zed} BirthdayBook known : \power NAME birthday : NAME \pfun DATE \where known = \dom birthday \end{zed} \begin{theorem} \exists BirthdayBook' @ known' = \emptyset \end{theorem}先不要写证明脚本，只写定理声明。这里的\exists BirthdayBook' @ known' = \emptyset读作“存在一个生日簿状态，它的 known 是空集”。注意变量加了撇号表示这是操作后的状态，Z-EVES 会要求你用 schema 操作符来正确代入，不能自己徒手展开。保存之后，下一步就是跑生成证明义务的命令。
3.3 生成证明义务的常用参数与输出解读
类型检查过了，就可以要求 Z-EVES 把证明义务列出来。命令行常见的做法是使用-p参数生成证明义务，或者直接在交互界面里敲check和prove。假设我们要验证刚才那个存在性定理，命令可以写成：
zeves -p birthdaybook.zed运行结束后，终端里会列出每个证明义务的状态，比如proved、unproved或invalid。我第一次看到invalid时很困惑，以为工具出错了——后来才明白，它表示这个公式在逻辑上根本不是定理，你永远证不出来。这个状态比unproved更值得警惕，因为它意味着你的需求描述本身就有矛盾。
输出里通常还会提示未证明的 goal 长什么样。如果你看到某个 goal 里出现一堆集合成员关系，别急着手动证，先回到规格层想想是不是 schema 约束写得过强。辅助工具不是帮你硬证难题的，而是帮你在不可能的目标上尽早止损。
3.4 常用命令参数的速查参考
下表是我在实际使用中经常会用到的参数类别，具体拼写以你拿到的构建版本为准，但语义方向基本一致：
| 参数意图 | 常见形式 | 说明 |
|---|---|---|
| 解析并类型检查 | -t或check | 只做语法和类型检查，不生成证明义务 |
| 生成证明义务 | -p或prove | 对当前规范生成所有必须验证的谓词 |
| 增量处理 | -s或step | 只处理新增或修改的 schema，节省时间 |
| 输出详细信息 | -v或verbose | 打印每一步规则替换和策略使用情况 |
不要一上来就把所有参数都打开。尤其别直接开 verbose 跑大规范，输出量大到你会想丢掉重写。我一般先做一次干净的类型检查，确认没有低级错误，再单独生成证明义务，最后才针对过不了的那几个目标打开详细输出。
4. 在Z-EVES里证明一个定理：从断言到可复用证明脚本
4.1 一个能证得动的例子：定义域与已知集合相等
很多初学者一上来就想证高深的偏序完备性，结果被证明义务按在地上摩擦。我的建议是先证一个温和的引理：known = \dom birthday在生日簿的某个状态下成立。为了让证明负担足够小，我们可以把目标限定在一个具体实例上：
\begin{theorem} known' = \emptyset \implies \dom birthday' = \emptyset \end{theorem}这个定理读起来像废话，但它已经包含了一个真的证明义务：如果 known 是空集，那么 birthday 的定义域也必须是空集。从偏函数定义和 schema 不变量可以推出这个结果，但 Z-EVES 不会默认帮你展开不变量，你需要显式告诉它用哪条假设。
4.2 证明脚本的常见写法：simplify、normalize 与 prove
在 Z-EVES 里，证明是一段显式的脚本，不是打个勾就完了。常见做法是给目标应用一系列策略，让证明器逐步简化。一个典型的证明脚本长成这样：
proof te_domKnown: simplify provesimplify会把集合为空、定义域为空这类明显的替换先聚合掉，prove则是调用核心证明器处理剩余的谓词逻辑。整个过程很像给一个笨手笨脚的助手分配粗活：先做机械化简，再让它思考推导。很多时候，simplify一过，目标已经被压到一个平凡的前后件因果，prove立刻收工。
这个命令顺序不是玄学，它有实际理由。如果你反过来直接prove，策略会尝试各种规则组合，遇到存在量词时会做大量枚举，容易跑几分钟没有结果。先simplify可以减少搜索空间，这不是心理安慰，而是计算开销上的真实差别。
4.3 修改规范之后的增量验证策略
Z 规范最容易踩的坑就是你改了一个 schema 的约束，结果十几个下游 schema 的证明义务全部失效。这种情况下不要一个个手动重证，先看失败模式。如果失败目标是invalid，说明你的改动引入了不可满足条件；如果失败目标是unproved，说明约束变动砍断了某条推导链。
我的习惯是每次改动后，用一个单独的脚本文件只检查受影响的模块，而不是全量重跑。增量项通常会检查操作 schema 的前后状态是否兼容，以及新引理是否覆盖了旧引理没覆盖的 case。这里有个经验：把不变量尽量写在深层 schema 上，让上层操作通过 schema 演算继承约束，比把大谓词重复抄进每个操作里要干净得多，证明义务也会少一大半。
4.4 别把证明器当推土机：一个常见误用
很多刚接触 Z-EVES 的人把它当成自动推土机，觉得一个prove就能碾平所有目标。实际遇到第一个证不过的目标时，他们会下意识地加一条axiom，让它看起来秒过。这是最危险的翻车操作——axiom等于告诉工具“这条不用你证明，我说它对它就对”。一旦加了公理，后面的证明义务再多也是空中楼阁，一个隐藏矛盾会顺着公理扩散到整个规范。
我见过的血泪经验是：有人在一份 200 行的规范里塞了 11 条axiom，最后评审时被专家逐一追问来源，现场根本解释不了。辅助工具的意义在于帮你建立可信链条，而不是帮你伪造链条。如果你确实需要假设某条外部性质，应该用assumption类的声明并写清楚它等价于现实世界的什么约束，同时在文档里单独列出需要人工复核。
5. Z-EVES避坑指南：5个让我半夜改规格的翻车现场
5.1 坑一：类型不匹配但报错在莫名其妙的行号
现象：类型检查报告的出错行和你真正写错的表达式差了整整十几行，让你怀疑工具是不是坏了。原因：Z-EVES 的类型推断是全局的，某个地方的集合元素类型不匹配，可能直到它被用到另一个 schema 时才暴露出来。解决：把出错行附近的所有变量都加上显式类型声明，不要依赖推断；再就是分段检查，每个 schema 单独存一个临时文件跑一遍，收敛出真正有问题的位置。我吃了两次这种亏之后，学乖了：所有核心 schema 一律显式声明函数返回值类型，宁可多打几个字，不给自己留猜谜的时间。
5.2 坑二：改动一行不变量，几十个证明义务集体失效
现象：你只是在规范里把\pfun改成了\ffun，结果整个项目一半的证明义务变成unproved。原因：函数类型从偏变成全，意味着定义域性质完全不同，所有依赖原关系的命题都要重新推导。解决：改动前先全局搜索依赖这个 schema 的定理；改动后不要手工重证，而是写一个批量回归脚本，把失败的义务存档，一个一个去追问它们和改动点的因果链。很多时候你会发现旧证明里隐含使用了“偏函数不作用在未定义元素上”这条性质，而全函数没有这个说法。
5.3 坑三：证明命令的顺序会改变结果，同一条命令失败后加一条又能过
现象：同样的目标，先prove卡死，先simplify再prove立刻通过。原因：Z-EVES 的证明策略是启发式搜索，化简步骤会改变目标形状，影响后续规则匹配。解决：把证明脚本视为一个固定工艺，不要随意调整顺序；如果某条命令在某处失效，优先怀疑它在之前的状态上做了什么不可逆的改写。我会给每个关键证明加注释，记录为什么这个顺序是必要的，防止自己三个月后看不懂。
5.4 坑四：中文注释和全角符号让解析器翻车
现象：注释里写了中文，结果 Z-EVES 报出“字符不可识”或者干脆解析停在注释中间。原因：老牌证明器的词法分析器大多只支持 ASCII，多字节编码会把换行符拆得支离破碎。解决：所有规范和证明脚本一律英文注释、半角标点；如果确实需要中文，放在外部设计文档里，用 id 引用而不是塞进源文件。这是我被折磨得最惨的一次，整份文件编译不过，排查了半小时才发现注释里的一个“：”全角冒号惹的祸。
5.5 坑五：用 axiom 掩盖证明义务，最后信任链崩盘
现象：某个目标证不过去，顺手加一条axiom myClaim，然后所有下游证明全绿，你觉得万事大吉。原因：公理没有经过证明，它只是让你“以为”证了。解决：把axiom视为技术债，每一条都要登记到待验证清单中，写明它对应现实世界的哪条假设，并定期回到这些公理上补充独立验证。如果你发现自己需要三条以上公理才能跑通一个核心流程，大概率是规范建模有问题，而不是工具能力不足。
6. 进阶用法：用批处理脚本把Z-EVES嵌进日常验证流程
到了这个阶段，你应该已经能手动跑通单文件检查和证明。真正让 Z-EVES 产生长期价值的做法，是把它变成一个每天自动跑一遍的回归工具。我常用的批处理脚本只有十几行，核心是一个遍历所有.zed文件的循环：
for f in specs/*.zed; do echo "checking $f" zeves -t "$f" || echo "FAIL: $f" done这个脚本会在规范改动后的每次提交前执行。如果有任何一个文件类型检查不过，脚本直接以非零状态退出，阻断合并。别小看这道防线，形式化规范最容易在“只改了英文注释”这种看似无关的提交里悄悄破坏语法。我还习惯生成一个证明义务状态清单，把proved、unproved分别统计，存成proof-status.txt，方便对比每次改动前后数字的变化。
更高阶一点的做法是给 Z-EVES 写一个固定的策略文件，把常用证明序列封装成宏。你可以把simplify; prove定义为一个名为quickproof的局部策略，然后在每个证明脚本里直接复用。这样当工具版本升级导致规则变化时，你只需要调整策略文件，而不必改动几十个证明脚本。多年下来，我自己的策略文件积累了十来条这样的封装，每个都用注释写清楚适用场景，成了项目里最值钱的文件之一。
我还有一个个人习惯：每当我要新开一个需求模块，先写一个空的骨架规范，只包含 schema 名和最小不变量，在 Z-EVES 里跑通类型检查之后才填充细节。这相当于先搭好脚手架，再一层层加砖。比起写满一页纸再回来调试，这种方式能省掉大量重构时间。工具毕竟只是辅助，真正的门槛还是你对需求里数学关系的理解；但 Z-EVES 最大的好处是把你“以为理解”和“确实理解”之间的距离压缩到几乎为零。
我最后一次用它是在一个状态机规范上，当时所有证明义务全绿，我心里却总觉得有一个操作没有覆盖前置条件。最后查了一下，发现是那个操作的前置条件里少了一条关于输入集非空的约束。这问题要是靠人工评审，不知道要多久才能暴露。从那以后我养成了一个习惯：只要证明义务全绿，我会故意删掉一两条看起来显然的必要约束，观察是否有一个目标从unproved变成invalid——如果没有变得不同，说明我的证明链条可能没有真正依赖那条约束，这时就要回头检查约束是否被妥善集成。这种“故意破坏验证法”听起来有点自虐，但它是检验形式化规范质量的有效手段。希望这个习惯也能帮到你的下一个 Z 项目。
本文还有配套的精品资源，点击获取
