简介：形式化Z语言规格说明与Z-EVES辅助工具资源包，面向软件工程、安全关键系统设计与形式化验证方向的学习者及开发者。资料以Z语言建模和Z-EVES环境为核心，提供从Z语言基础概念到工具实际使用的完整支持。压缩包共5个文件，以可执行程序、PDF文档和HTML说明页为主：exe文件包含适用于Windows的Z-EVES安装程序及运行环境，PDF文档分别介绍用户指南与Windows平台使用指引，HTML为下载、安装和使用的图文教程。包体仅8.63MB，轻量易获取。已有820人学习，适合正在了解形式化方法并希望在真实工具中编写Z规格、进行证明和检查的学习者。借助这份资源，可以快速安装并上手Z-EVES，理解Schema、关系、谓词等核心建模元素，并通过官方指南减少环境配置弯路，为后续在航空、医疗等安全攸关领域应用形式化验证打下基础。
1. 为什么需要 Z-EVES：Z 语言规范的形式化验证不能只靠读代码
在民航、轨道交通这些对安全等级要求极高的领域，需求规格里的一个小漏洞，到编码阶段可能放大成一次事故。很多团队选择用 Z 语言把系统状态和操作写严谨，但写出来的规范怎么保证是对的？人眼很难排查一个两百行的模式里隐藏的类型错误或者不可满足的谓词。Z-EVES 就是在这个场景下被反复提起的辅助工具：它能把 Z 规范解析成数学结构，做类型检查，并对用户声明的定理执行交互式证明，不依赖任何商业授权。这篇文章面向那些想在真实项目里用 Z-EVES 但不知道怎么入手的工程师、学生和研究者，我会从原理讲到环境搭建、实际验证再到我踩过的坑。
2. 从集合论到证明器：Z 语言的数学基础与 Z-EVES 的验证机制
2.1 Z 语言的数学底座：集合、关系与函数
Z 语言的表达力植根于经典集合论和一阶逻辑。要用工具之前，先要建立两个基本认识。首先，Z 语言中所有的数据类型本质上都是集合。PERSON 是一个给定的基本类型，表示“人”这个论域；P PERSON 表示人的所有子集，也就是“所有人组成的集合”；而 PERSON → DATE 表示从人到日期的部分函数，对应“某些人有生日日期”的约束。凡是能出现在模式里的量，最终都可以被解释为某种集合关系。
其次，模式（schema）是 Z 语言组织信息的基本单元。一个模式由上下两半组成，上半部分是声明（signature），列出变量及其类型；下半部分是谓词（predicate），约束这些变量的取值。比如下面这段描述门禁系统初始状态的定义：
InitialAccessSystem ─────────────────── authorized : P PERSON inside : P PERSON ─────────────────── inside = ∅这种书写方式看起来简单，但精确到足以让机器判断：如果 inside 里有元素不属于 authorized，这个状态就不合法。Z-EVES 对规范的处理流程的第一步，就是把这些声明和谓词展开成带类型标注的一阶逻辑公式。
在实际使用中，Z-EVES 需要的是带 LaTeX 风格控制符号的源文件。对于同一段定义，在 Z-EVES 里我会写成：
\begin{schema}{InitialAccessSystem} authorized : \power PERSON \\ inside : \power PERSON \where inside = \emptyset \end{schema}这里的 \power 和 \emptyset 分别对应集合的幂集与空集。Z-EVES 内部维护着一个“数学上下文”，每加载一个模式，就把其中声明的变量加入上下文，谓词则作为后续证明可用的假设。这一步如果类型对不上，工具会在解析阶段直接报错，不会进入证明阶段。
声明顺序会对类型推导产生实质影响。把 inside 放在 authorized 前面，这里也能推导通过，因为两个变量互不依赖；但一旦后续定理里用 inside ⊆ authorized，Z-EVES 就要在上下文中找到 authorized 的类型。我的习惯是先声明被依赖的集合，再声明依赖它的集合，减少不必要的显式类型标注。
常见的一个误区是以为 Z 语言只适合描述数据库或者通信协议这类“离散系统”。实际上，Z 语言没有内置的时序概念，它描述的是状态和操作前后状态关系，所以被用在许多安全关键场景，包括航空电子设备的模式切换逻辑和银行核心系统的账户状态机。Z-EVES 正好承接这些场景的自动化验证需求，因此它才被叫做形式化开发的辅助工具。
关于名字容易望文生义的另一个点：Z 语言与“零知识证明（Zero-Knowledge Proof）”在英文缩写上沾边，但完全不是一个东西。零知识证明的形式化验证走的是 Coq、Isabelle 那套构造型理论路线；Z 语言走的是 Zermelo-Fraenkel 集合论路线。如果有人上来就拿着 ZKP 的论文问能不能用 Z-EVES 跑，答案是不能。
2.2 Z-EVES 的分层设计：类型检查、上下文与交互式证明
Z-EVES 本身可以拆成三个协作的组成部分：数学上下文（mathematical context）、检查器（checker）、证明器（prover）。上下文是一个全局知识库，记录所有已经定义的类型、常量和定理。检查器负责把规范文本解析成逻辑公式，同时执行类型检查。证明器再根据用户发起的命令，在上下文中搜索可用的定理和定义，对目标进行重写与归约。
这么设计的理由是：Z 规范通常很大，证明也往往复杂，把“规范本身是否正确”和“定理能否被证明”分成两个阶段，能大幅缩短排查链路。Z-EVES 的证明器并非全自动的 SMT 求解器，而是一个交互式证明助手。它接受用户的证明命令，比如展开某个定义、应用某条引理，然后逐步缩小待证目标。你直接让它“全自动证明”一条涉及集合包含的定理，它往往会卡在需要做 case analysis 的节点上。这时候由你告诉它按什么条件拆分情况，证明才能继续推进。
证明命令的粒度也反映在 GUI 界面上。Z-EVES 的 Windows 版提供一个编辑器，能高亮显示当前证明目标，并在证明树中展开每一步已经应用的规则。命令行版本则输出证明树状态。两边的内核是同一个，所以不必担心 GUI 与命令行结果不一致——这一点在第五章的坑里我会详细讲。
一个常见误用是拿 Z-EVES 当 model checker 用。Z-EVES 不会自动枚举状态空间，也不会告诉你一个操作模式能否到达某个状态。它只回答“在给定上下文里，目标公式是否可从假设推导出来”。功能边界想清楚，才不会在工具上浪费时间。作为辅助工具，Z-EVES 负责证明你声称的定理，不负责从模型里自动揪出反例。期望定得太高，往往会在用过一次之后就放弃整条形式化路线。
3. 搭建 Z-EVES 环境并跑通第一个规范：从下载到类型检查
3.1 获取与安装：Windows 与 Linux 的差异
Z-EVES 目前的开源版本可以在 SourceForge 的项目页直接获取，有 Windows 安装包和 Linux 二进制两个发行线。Windows 版本自带图形界面，安装后能直接打开 .tex 后缀的规范文件。Linux 版本更适用于自动化批处理脚本，我一般会在 CI 里调用命令行版的 z-eves 对规范做回归检查。
Windows 安装过程几乎无脑下一步，唯一要注意的是安装路径不要带空格，否则后续命令行的批处理调用会撞上引号解析问题。Linux 下更简单，解压后把可执行文件路径加到 PATH 里就行：
export PATH=$PATH:/opt/z-eves/bin z-eves --version输出里会显示版本号和版权信息。如果看到 “command not found”，先检查解压目录的 bin 下是否有 z-eves 这个可执行文件；有些发行版把可执行文件命名为 zeves，不是 z-eves。
在 Linux 下跑命令行时，Z-EVES 默认读取标准输入里的规范文本，并把结果写到标准输出。为了不把每一步交互都敲进终端，我习惯用脚本驱动：
z-eves < spec.tex > result.txt 2>&1这个命令把 spec.tex 交给 Z-EVES，所有证明命令、错误信息都进 result.txt。第二个参数 2>&1 把标准错误也合并到输出文件，方便一次性排查。执行完之后用 grep 过滤 ERROR 关键字，能很快定位到失败点。
grep -n "ERROR" result.txt | head -20这段过滤命令只保留含 ERROR 的行，并显示行号。第一次看到 Z-EVES 输出时，大概率会被满屏的提示信息吓到，但真正需要关心的只有 ERROR 和 WARNING 两类。把其他信息当成正常过程输出即可。
注意：如果你的 Linux 发行版缺少 X11 库，GUI 版可能无法启动。纯命令行模式不需要 X11，这也是我推荐在服务器上使用命令行版的原因。
3.2 第一个规范：声明基本类型与状态模式
先从最简单的门禁系统开始。第一步声明给定类型 PERSON，表示系统中所有人员标识；然后定义初始状态模式，并把“进门后必须已被授权”写成不变式。完整的规范文件里，模式定义通常放在前部，定理放在后部。
\begin{schema}{AccessSystem} authorized : \power PERSON \\ inside : \power PERSON \where inside \subseteq authorized \end{schema}接着定义初始状态：
\begin{schema}{InitialAccessSystem} AccessSystem \where inside = \emptyset \end{schema}InitialAccessSystem 通过包含 AccessSystem 继承了 authorized 和 inside 两个变量及其不变式，再额外约束 inside 为空。这种继承写法叫模式包含（schema inclusion），是 Z 语言里复用状态定义的标准方式。Z-EVES 在解析时会把继承关系展开成完整的声明和谓词集合。
写完两个模式之后，不要急着点证明。先用 Z-EVES 的检查功能把规范吃进去。如果直接运行证明命令，多数情况下会先收到 “not checked” 的提示，因为规范还没有进入上下文。正确顺序是：解析 → 检查 → 生成上下文 → 证明。在 GUI 版本中，选择菜单里的 Check 命令。命令行下可以执行：
z-eves -check spec.tex-check 参数只做解析和类型检查，不进入证明。输出没有 ERROR 就说明声明和谓词的类型都对上了。这一步是复现的关键动作，很多第一次用 Z-EVES 的人直接把例子粘贴进去就点证明，结果被 “unresolved reference” 卡住。原因通常是前面的类型没有加载进上下文，或者模式名拼写不一致。养成先 check、再 prove 的习惯，能省掉一半无意义的报错。
检查通过后，就可以开始第一条定理的证明。我在实践中会把初始状态和操作模式放在同一个文件里，这样上下文一建立，所有定理都能直接引用。项目再大一点，就按基础类型、状态模式、操作模式、引理、定理拆成五个文件，用 include 组织起来。include 路径用相对路径，避免不同机器上绝对路径不一致的问题。
\begin{theorem}{InitInsideAuthorized} InitialAccessSystem \implies inside \subseteq authorized \end{theorem}这条定理说的是：在 InitialAccessSystem 的假设下，inside 一定是 authorized 的子集。由于初始状态里 inside 是空集，而空集是任何集合的子集，它在数学上必然成立。真正的问题在于 Z-EVES 能不能自动发现这条证明路径，这要留给第四章展开。
4. 把规范变成可证明的定理：Z-EVES 的证明命令与回归流程
4.1 从应用场景推导定理：状态不变式与操作前置条件
规范本身只是描述了“系统应该怎样”，真正验证要做的是证明规范和我们的预期一致。以门禁系统为例，我关心两件事：初始化之后 inside 是否合法；执行进入操作之后，合法状态是否保持。第一件事可以直接写成定理：
\begin{theorem}{InitInsideAuthorized} InitialAccessSystem \implies inside \subseteq authorized \end{theorem}由于初始状态里 inside 是空集，而空集是任何集合的子集，这条定理在数学上必然成立。Z-EVES 能不能自动完成这条证明，取决于我们给它的命令。
第二件事需要定义“进入”操作。操作模式引入 Δ 约定，表示状态会发生变化：
\begin{schema}{EnterSystem} \Delta AccessSystem \\ person? : PERSON \where person? \in authorized \\ person? \notin inside \\ inside' = inside \cup \{person?\} \end{schema}这里 person? 带问号后缀，表示输入变量；inside' 带撇号，表示操作之后的新状态。ΔAccessSystem 展开后提供了 inside 和 inside'、authorized 和 authorized' 两组变量。EnterSystem 有前置条件（人已被授权、人不在场内）和后置条件（人进入场内）。
于是“进入操作保持不变量”就可以写成：
\begin{theorem}{EnterPreservesInvariant} AccessSystem \land EnterSystem \implies inside' \subseteq authorized' \end{theorem}这条定理是验证闭环里最典型的形态：前提是状态合法再执行操作，结论是操作后的状态依然合法。从直觉上讲，如果 authorized 不变化，而 inside 只是增加了一个原本就在 authorized 里的元素，inside' 当然还是 authorized 的子集。但机器不承认直觉，它需要从类型信息、集合成员关系和等式替换里逐步推导。此时正好演示 Z-EVES 的证明命令。
4.2 交互式证明命令：reduce、split、prove 的配合
在 Z-EVES 里，证明不是一次“运行”完成的，而是由一条条命令推进的。reduce 是最常用的起点命令。它把目标中出现的模式定义展开，并尝试利用上下文中的已知事实完成自动化简。
GUI 里操作的话，打开目标 EnterPreservesInvariant，先点 Prove，再点 Reduce。证明窗口里会看到待证目标被展开成：
inside' ⊆ authorized' where: inside ⊆ authorized person? ∈ authorized person? ∉ inside inside' = inside ∪ {person?}此刻 reduce 已经把模式里的 where 子句提取成假设，剩下的目标只是集合包含关系。接着，集合包含关系可以按定义拆开：X ⊆ Y 等价于对每个元素 e，e ∈ X 推出 e ∈ Y。Z-EVES 对这种拆解的自动推理能力有限，要么手动引入集合论引理，要么用 split 对目标做逻辑分支。
一个可用的证明脚本如下：
\begin{proof} reduce; split; prove; \end{proof}第一行 reduce 展开模式定义，第二行 split 按逻辑连接词把目标拆成分支，第三行 prove 在分支上调用自动推理。这个脚本能处理相当大一部分“状态不变式”类的定理。把脚本写在定理后面，Z-EVES 重新加载时会自动重放，不需要每次重新输入命令。
有些读者可能希望直接敲 prove 一把梭，在复杂规范上基本不可能。Z-EVES 的自动证明能力覆盖命题逻辑和简单的集合代数，但只要出现量词或函数相等，通常就要人工介入。我的经验是：先走到“目标展开、假设足够、卡在某个集合论事实”的位置，再判断缺引理还是缺拆分；而不是指望工具猜出全部路径。
4.3 把验证挂进日常循环：批处理回归
一个正式项目不可能只证明一条定理。更常见的做法是在规范里挂了三四十条定理，每次改动规范都要全部重放。Z-EVES 批处理模式正好适合这个场景。
写一个简单的 shell 脚本：
#!/bin/bash for f in theories/*.tex; do echo "checking $f" z-eves -check "$f" || echo "FAIL: $f" done这段脚本遍历 theories 目录下所有 .tex 文件，逐一做类型检查。如果任何一个文件返回非零退出码，就打印 FAIL。把这段脚本挂进 CI 工作流之后，每次提交规范都能自动得到类型层面的反馈，比等人肉眼 review 靠谱得多。
需要说明的是，批处理脚本只解决“检查”环节，要让证明也自动跑，需要把 proof 脚本写进每个定理文件里。Z-EVES 在处理 include 时会按先后顺序把各文件的定义纳入上下文，所以交叉引用不会出问题。唯一要注意的是文件排序——B 依赖 A，就必须让 A 先被 include。这也是第五章要详细展开的常见坑。
5. 避坑与排查：Z-EVES 使用中我记下的五个真实问题
把拆过的项目遇到的问题记下来，是最值得复用的资产。下面五条全部来自真实使用场景，每一条都按现象、原因、解决的顺序写清楚。
5.1 规范文件里出现中文注释导致解析失败
现象：在规范文件里写了中文注释，Z-EVES 打开后注释变成乱码，甚至解析报错，说某个字符不在字母表内。
原因：Z-EVES 的输入解析器严格按 LaTeX 兼容的字符集合识别内容，源文件默认按 ASCII 处理。中文字符在工具里不被识别为注释内容，而会被当成非法符号。
解决：规范源文件一律用纯英文注释；如果团队确实需要中文说明，放在单独的说明文档里，不要混进 .tex 规范文件。检查源文件传输时的编码转换，尽量另存为 UTF-8 无 BOM 或纯 ASCII。这个习惯帮我避开了大量毫无价值的编码报错。
5.2 类型检查报“变量类型未知”：声明顺序与上下文隔离
现象：检查某个模式 D 时，报错说变量 t 类型未知。单独看 D 的定义，t 的声明就在上面几行。
原因：Z-EVES 检查时只使用当前数学上下文。如果 t 在另一个文件里被声明，而那个文件没有被 include 进当前上下文，检查器就不认识它。还有一种情况是 include 顺序反了——B 文件里的模式引用了 A 文件的类型，但 B 先被加载。
解决：把所有公共类型和全局常量放在一个基础文件 base.tex 中，其他文件按依赖顺序 include base.tex。顺序用 Makefile 或脚本固定下来，避免手工排列。这样每次新增文件时，上下文依赖关系一目了然。
5.3 定理明显成立但证明不完：缺一条辅助引理
现象：定理 EnterPreservesInvariant 的证明走到中间步骤，目标变成只需证明 {person?} ⊆ authorized，但 prove 命令无法完成。
原因：Z-EVES 的自动证明不会主动引入“单元素集合包含等价于元素属于集合”这条集合论定理，而我们的规范上下文里也没有这条引理。工具不是不知道这条数学事实，而是不知道你需要在当前这一步使用它。
解决：先把 {x} ⊆ S 这类目标归纳成通用引理，在上下文里显式声明它。例如：
\begin{theorem}{SingletonSubset} \forall x : PERSON; S : \power PERSON @ (\{x\} \subseteq S) \iff x \in S \end{theorem}定理文件里先证明 SingletonSubset 并把它加入上下文，再证明 EnterPreservesInvariant 时，Z-EVES 就能检索到这条引理并自动使用。把频繁出现的集合论小结论固化成引理，是减少手工证明命令的关键。
5.4 证明脚本重放失败：上下文改动影响后续重写
现象：同一份 .tex 文件，昨天重放证明全部通过，今天改了一处类型定义之后，某条定理的证明脚本在第五步报错。
原因：Z-EVES 的证明重放严格按照脚本行的顺序与上下文状态执行。如果修改了前一个模式，那么后续定理的假设集合可能发生变化，原本能命中的重写规则不再可用。表面上“无关”的改动，实际改变了上下文中某个常量的定义。
解决：每次修改规范后，不只对修改处的定理重放，而是对全部定理做完整重放；如果失败，先看失败步骤的目标与前一次有何不同，再决定是补引理还是改脚本顺序。把证明脚本当作代码来管，提交前跑全量回归。
5.5 GUI 能过但命令行过不了：会话状态掩盖问题
现象：同一个规范文件，在 GUI 里点 Proof 菜单能通过，命令行执行同样证明命令却报错。
原因：GUI 可能已经加载过某些上下文或执行过某些命令，当前证明状态并不是从文件初始状态开始的。命令行每次都是全新解析，不包含任何 GUI 历史状态。两者内核一致，但 GUI 的会话状态会掩盖问题。
解决：在 GUI 里验证完任何证明，都要用命令行从零重放一遍。我个人的习惯是：GUI 只用来做交互式探索和阅读证明树，真正的验证结果以命令行批处理的输出为准。从那以后，我再也没有被“GUI 能过但 CI 挂掉”这种事困扰过。
6. 让 Z-EVES 更好用的三个习惯：引理拆分、命名体系与回归脚本
6.1 把大定理拆成小引理，每条证明控制在十条命令内
大型规范里，一条超过五十行的证明命令链是灾难。一旦某个模式改了，中间步骤全部失效且没有可读性。实践证明，把目标定理拆成三五个小型引理，每条证明控制在十条命令以内，是最容易维护的方式。例如要验证一个复杂操作，先证明前置条件满足，再证明类型不变，最后证明核心不变量。每个小引理独立重放，失败点定位到具体一条引理，而不是整条证明链。
6.2 给定理一套可读的命名前缀，让证明脚本变成文档
我会按用途给定理加前缀：init_、op_、inv_。op_EnterSystem_Pre 表示进入操作的前置条件引理，inv_InsideAuthorized 表示不变量相关。目录结构则固定为基础类型、状态模式、操作模式、引理、顶级定理五层。这样即使某个文件半年没打开，靠名字也能立刻知道它在验证链中的位置。配合全量回归脚本，Z-EVES 就能真正嵌入开发流程。
真正让我下定决心固定这套习惯的是一次返工：当时一个门禁项目里改了授权规则，我去掉了一条看似无关的引理，结果两天后才发现另一条定理的证明重放失败。从那以后，每次改规范，我都强制走一遍“改文件 → 全量 check → 全量重放证明 → 对比失败清单”的流程。希望这套流程对你也有用。
本文还有配套的精品资源，点击获取
