使用模型检验器不需要LTL

使用模型检验器不需要学习线性时序逻辑。Kani、CBMC和Alloy等工具允许你用普通的断言和关系约束来验证性质。你放弃了证明活性性质的能力，换来的是以小时而非周为单位的学习曲线，而对于大多数软件错误来说，这是一笔值得的交易。

时序逻辑是大多数模型检验器要求的守门人

经典的模型检验器，SPIN和NuSMV，要求你用时序逻辑公式或计算树逻辑来表达性质。你写诸如G(request -> F(response))这样的东西来表示”全局地，每个请求最终都会得到一个响应”。这很强大。它可以证明你的协议永远不会死锁，每条消息最终都会被确认，你的系统是公平的。

这也是大多数在职开发者不具备的专业技能。读一个时序逻辑公式不像读代码。算子是模态的，语义定义在无限路径上，而你在写单元测试时建立的直觉无法迁移。所以这个问题是合理的：如果你想要模型检验的错误发现能力，你真的必须先攀登那座高山吗？

不。另一类药物工具已经存在了几十年，它们用你已经在写的相同断言来检验代码。

有界模型检验器将断言转化为可满足性问题

有界模型检验器不要求你学习新的逻辑。它要求你编写测试支架。你声明非确定性输入，用假设来约束它们，并在宿主语言中断言性质。然后该工具将循环展开到一个界限，将程序编码为SAT或SMT公式，并让求解器寻找反例。

如果求解器返回UNSAT，那么你的性质在该界限内的所有路径上都成立。如果它找到反例，你会得到一个具体的追踪，准确显示哪些输入触发了错误。没有时间算子。没有无限路径。只有一个带有可复现输入向量的失败断言。

Kani是Rust最平易近人的有界模型检验器。它可以通过cargo install kani-verifier安装，并在普通Rust代码上运行。

真实示例：在Rust中检验状态机

这里有一个带错误的状态机。它跟踪一个简单的计数器，每次滴答递减，直到归零，然后转回空闲状态。

#[derive(Clone, Copy, PartialEq, Debug)]
enum State {
    Idle,
    Running,
    Stopped,
}

struct Machine {
    state: State,
    count: u32,
}

impl Machine {
    fn start(&mut self, initial: u32) {
        if self.state == State::Idle && initial > 0 {
            self.state = State::Running;
            self.count = initial;
        }
    }

    fn tick(&mut self) {
        if self.state == State::Running {
            self.count -= 1;
            if self.count == 0 {
                self.state = State::Idle;
            }
        }
    }

    fn stop(&mut self) {
        if self.state == State::Running {
            self.state = State::Stopped;
        }
    }
}

这个错误很微妙。看stop。它将状态设为Stopped，但让count保持不变。如果之后有东西假设state == State::Stopped时count == 0，那这个假设就是错的。

下面是一个能捕捉到它的Kani证明支架：

#[kani::proof]
fn check_stopped_implies_count_zero() {
    let mut machine = Machine {
        state: State::Idle,
        count: 0,
    };

    let initial: u32 = kani::any();
    kani::assume(initial > 0 && initial <= 10);

    machine.start(initial);
    machine.tick();
    machine.stop();

    assert!(
        machine.state != State::Stopped || machine.count == 0,
        "Stopped state should have count == 0"
    );
}

Kani会探索每一条路径。它发现如果initial == 2，在start之后机器是Running状态且count == 2。一次tick将count减到1，但状态保持Running。然后stop将状态设为Stopped而count仍为1。断言失败。Kani会报告这条确切的追踪。

这就是不用时序逻辑的模型检验体验。你写Rust。你用Rust写断言。工具告诉你哪些输入会破坏它们。

Alloy用关系逻辑发现设计层面的错误

有界模型检验器验证代码。Alloy验证设计。

Alloy是一个模型查找器，不是传统的模型检验器，但区别不如工作流程重要。你将系统描述为一组关系，将状态不变式描述为一阶逻辑约束，然后让Alloy寻找反例。它搜索用户定义范围内的所有可能实例，并向你展示失败示意图。

下面是一个简单有向图性质的Alloy模型：

sig Node {
    next: set Node
}

pred reachable[n1, n2: Node] {
    n2 in n1.^next
}

assert symmetric_reachability {
    all n1, n2: Node |
        reachable[n1, n2] implies reachable[n2, n1]
}

check symmetric_reachability for 3

该断言声称可达性是对称的。Alloy检验所有不超过三个节点的图，并立即画出一个反例：n1指向n2但n2没有出边的图。没有任何地方出现G、F或U算子。

你放弃的东西：活性与无限行为

这种便利性是有代价的。有界模型检验器只验证到循环界限或路径长度为止的行为。它不能证明请求最终会得到响应，只能证明坏事不会在前N步内发生。Alloy只检验其范围内的实例。它不能为任意大的系统证明性质，只能证明界限以下不存在反例。

如果你需要证明你的共识协议永远不会丢失已提交的写入，或每条消息最终都会被投递，你仍然需要时序逻辑和无界模型检验。像TLA+这样的工具将时序逻辑包装在更像数学而非模态逻辑的语法中，但底层语义仍然是时序的。

对于数据结构不变式、API契约强制，以及寻找只在第47条执行路径上触发的竞态条件，有界工具通常已经足够。它们捕捉到单元测试遗漏的错误，而且用的是不用教科书就能读懂的断言。

五分钟上手Kani

如果你已经安装了Rust，有界模型检验只需一个命令之遥。

cargo install kani-verifier
cargo kani setup

创建一个新的crate，写一个带有微妙错误的函数，然后添加一个#[kani::proof]支架。运行cargo kani。如果Kani找到反例，它会打印触发失败的具体输入。如果它报告VERIFICATION SUCCESSFUL，你的性质在默认界限内的所有路径上都成立。

从状态空间小且不变式清晰的函数开始。状态机、解析器验证和协议状态转移都是理想的首选目标。不要一开始就试图验证整个HTTP服务器。SAT求解器有限度，你的耐心也是。

常见问题：有界与无界、活性以及从何处开始

有界模型检验真的是模型检验吗？

从技术上讲，它是一种变体，将问题编码为可满足性查询，而非显式探索状态图。对于试图发现错误的开发者来说，这种区别只是学术上的。它系统地探索所有路径，这正是实践中模型检验的含义。

我能用Kani或CBMC证明活性吗？

不能直接证明。活性性质需要对无限行为进行推理，而有界工具明确限制了搜索范围。有时你可以通过展开足够多的步骤以达到不动点来编码有界活性检查，但那是高级技巧。

TLA+呢？它需要时序逻辑吗？

TLA+使用时序动作逻辑，所以从技术上讲是的。但Leslie Lamport设计的语法读起来像普通数学。大多数TLA+规范将90%的篇幅花在状态不变式和数据结构约束上，而不是时序算子。如果你确实需要无界时序推理，它是最易接近的路径。

我应该用Alloy还是Kani？

如果你有Rust代码并且想验证实现细节，用Kani。如果你还在设计系统，想在写代码之前探索你的不变式是否甚至可行，用Alloy。

选择匹配你问题的工具，而非匹配你野心的工具

时序逻辑优美而强大，但它不是形式验证的先决条件。有界模型检验器和关系模型查找器让你用已经会的语言表达性质。它们不会证明你的系统最终终止，但会发现那个破坏数据库状态机的差一错误。对于大多数团队来说，那才是要紧的错误。

从一个有状态的函数开始用Kani。写一个断言。让求解器告诉你遗漏了什么。