AI 说你对，形式化说你错

一段代码，测试全绿，代码评审也过了。上线三个月，某天两个请求同时进来，账目对不上。

这类 bug 测试很难抓到，因为它不是某一行写错，而是几个操作的顺序不对。而顺序这件事，代码里通常没人写清楚。

一、发生了什么

10 月 16 日，Stack Overflow 的播客请来了 Gabriela Moreira。她是 Quint 的 CEO，她所在的团队把 TLA+ 那套形式化方法包了一层，做成工程师能直接上手的工具。

节目的话题很具体：为什么在 AI 大量写代码之后，形式化规格反而更重要。

TLA+ 是一套用来描述系统行为的语言，擅长刻画并发、消息延迟、节点故障这些情况。它的价值在于，你不需要把每种场景都写成测试，只要把「允许发生什么」写成规则，模型检查器会在给定的状态空间里搜索可能的执行序列。搜到违反规则的那条，就给你一条完整的反例路径。

问题是门槛高。它看起来像数学，不像代码，多数工程师不愿意学。Quint 的做法是保留 TLA+ 的语义，换一套接近日常编程的语法，并且让规格可以执行：能跑、能模拟、能在模型检查器里验证。它还有一层更实用的能力——把模型产生的轨迹拿去对照真实系统的运行记录，看实现有没有偏离设计。这叫轨迹验证。

Moreira 在节目里把这套东西和 AI 生成的代码直接挂上了钩：当实现由模型产出，人很难靠「看起来对不对」来判断，规格就成了那个可以对照的基准。

二、跟你有什么关系

写分布式系统的。 锁、重试、选主、幂等，这些地方的 bug 大多不在代码里，在设计里。规格能覆盖测试覆盖不到的顺序组合。

用 AI 写核心逻辑的。 模型很擅长写出「能跑」的版本，也很擅长漏掉你没想到的边界。让它对着规格改，比让它对着你的口头描述改可靠。

做代码评审的。 评审能看出风格和明显错误，看不出状态机有没有死锁。这类问题需要另一种工具，不是更仔细的眼睛。

三、怎么开始，不用先成为数学家

1. 挑一个地方，不要挑全部。 选一条真正会出事的链路：下单、扣款、锁租约。一个小模型，五六个状态变量，就够找出问题了。
2. 先写不变量。 不要一上来描述所有行为。先写「任何时刻都不能发生什么」，比如「两个客户端不能同时持有同一把锁」。这句话比十页设计文档有用。
3. 让模型检查器去找反例。 它会给出一条走到违规状态的步骤序列。这条序列就是你缺的那个测试。
4. 把反例变成回归测试。 让真实代码重放这条路径，比对每一步的状态。改完之后再跑一次，防止改回去。
5. 用真实日志做轨迹验证。 生产环境跑出来的事件序列，拿去问「这符合规格吗」。不符合，要么实现有问题，要么规格漏了情况，两种都值得查。
6. 让 AI 写规格初稿，人来定对错。 起草可以外包，判断「什么算正确」不能。这是用这类工具时比较稳妥的分工。

四、三个别信的说法

「测试覆盖率够高就不用形式化。」 覆盖率衡量的是你跑了哪些代码，不是你想过哪些顺序。并发 bug 往往藏在两条测试都没走到的交错里。

「形式化等于证明代码完全正确。」 它证明的是「模型符合规格」。规格本身写错了，证明再漂亮也没用。规格是人和机器之间的契约，契约要人来定。

「AI 能写代码，也能自己写规格。」 可以起草，但不能自己拍板。哪些失败可以接受、重复投递算不算问题、降级到什么程度，这些是产品决策，不是语法问题。

五、一句话结论

AI 能把代码写得像对的，规格才能说明它是不是对的。

信息来源

• AI says you're right, formal methods say you're wrong，Stack Overflow Blog，2026-10-16
• Adopt formal methods with Quint: a practical guide for AI-driven teams，ReasonCore，2026

功能与价格以官方公告为准。本文写于 2026 年 10 月 19 日。