Anthropic 10 月 22 日发了一篇文章，讲他们和 Theorem 合作，用 Claude 给 100 多个开源库做形式化验证：先把“什么绝对不能发生”写成规则，让 AI 去写证明，再交给机器逐条检查。
我第一遍读完，确实没太看懂。
Rocq、RISC-V、OSS-Fuzz、ASan，一个术语接一个术语。读到最后，我也说不清它跟我有什么关系。
后来实在头疼，就偷懒让 AI 帮我看完全文再总结，又跟 AI 聊了几轮，我才知道这篇文章对我们大多数人有价值的点，是它的做法：
我们给 AI 定规矩，让 AI 按规矩去做，再让 AI 去找出违反规矩的反例。
跟 AI 协作，我越来越觉得，关键问题是：规则该怎么找。
它到底做了什么？
平时写单元测试，像是抽查几道题：输入 A，应该得到 B。
模糊测试更进一步，让机器随机出海量的题去撞 bug。但题是出不完的，撞得再久，也不能说“没有了”。
形式化验证换了个思路：先把“什么算对”写清楚，这叫规格；再给出一份证明，说明所有输入都满足它。证明卡在哪里，就顺着那里去找 bug。
以前很少有人这么做。证明比代码本身大得多，只有极少数专家写得了。
这次他们让 Claude 来写。起点是 Google 的 OSS-Fuzz 平台上，开源项目开发者已经写好的模糊测试。他们把每个测试的规格定成一句话：任何小于 64 MB 的输入，都不会让程序崩溃，不出现内存错误，也不出现断言失败。
注意这句话的写法。他们没有写正面的要求，没有去描述程序应该做对什么；他们写的是反面的要求：什么绝对不能发生。
换成我们跟 AI 说话的方式，这是一条负面提示词。
Claude 负责写证明，一个叫 Rocq 的证明检查器负责逐条验收。证明写出来非常长，但人不用读。按原文的说法，人只需要信三样东西：机器和操作系统的数学模型、定理本身是怎么写的、检查器本身。
Claude 自己说“我证完了”不算数，检查器说了才算。这跟我上一篇写的是同一件事：干活的那个，不能自己给自己判卷。
检查器只管程序满不满足规格。规格写得对不对，还得人来看。
附录里有两个数字，我印象很深。
第一个，在一类证明任务里，Claude 几乎都会先自己写一份简短的规格，再去证明。规格的中位数大约 110 行，对应的程序中位数大约 86 KB 代码。
第二个来自另一个实验。研究者让 Claude 用 Rust 写一个能运行 Python 程序的解释器，覆盖 Python 的很大一部分语法；一边写，一边证明它的行为和一篇论文里定义的 Python 规则一致。
为了比一比测试和证明各能抓到多少问题，研究者在这个解释器的早期版本里，故意埋了 7 个 bug。
先用随机生成的测试去跑：7 个 bug 里只发现了 2 个，另外 5 个没被发现，程序照样通过了测试。
再用证明去查：7 个 bug，每一个都让证明过不去，全被发现了。
测试只能发现它碰巧撞上的问题。证明要求所有情况都符合规则，哪一处不符合，都会卡住。
证明的过程中，Claude 也找到了一些模糊测试很难碰到的 bug。比如一个解压程序里，有个计数器会减过头，导致往内存里不该写的地方写数据。它只在大约 20 MB、结构很特别的输入上才会触发，而模糊测试一般只喂 1 MB 以内的小输入。
看着很好是吧？好像 bug 很容易就能找出来。但实际上，一个证明要花几亿 token，作者也说，成本是眼下最大的门槛。
审规则，不审实现
AI 写的代码越来越多，人一行行审，肯定审不过来。
这篇文章给了一个很清楚的分工：规格只有一百来行，人审得过来；几十 KB 的代码，交给 AI 去证明，检查器负责判卷。
这也是我一直以来的看法：人不用亲手写每一行，也不用逐行读懂每一行，但什么算对，得由人来定义。
规则写成“不能发生什么”，AI 才有东西可撞。
你跟 AI 说“把这个函数写好”，它不知道该往哪里找反例。你说“任何输入都不能让它崩”，它就有了明确的目标：去找那个能让它崩的输入。找到了，那是 bug；找不到，而且能证明找不到，这份证明就成立了。
原文有一段把这层关系讲得很直白：很多模糊测试本来就在检查更高层的规律，比如压缩再解压，结果必须和原来一模一样。规律一旦不成立，程序就会崩。所以证明它“永远不崩”，等于证明了这条规律本身。
还有一个细节，我很喜欢。
为了不让 Claude 每遇到一个 bug 就停下来等人，他们允许它在证明途中自己修 bug。但这就留了一个口子：Claude 完全可以把程序改成一个什么都不做、所以永远不会崩的程序，定理就轻松证完了。
所以他们又加了一条规矩：任何改动都扣分，能证明这次改动影响了哪些输入、而且影响得很少，才额外加分；所有改动都要记录、审计。
规矩会被钻空子，所以规矩还得管住“怎么满足规矩”。
人不用读懂每一行实现，但“什么绝对不能发生”，必须由人说了算。
今天就能上手：8 条单测全过，一条规则 0.14 秒找到 bug
形式化证明我们跑不动，但它的“抽查版”谁都能跑，叫属性测试（property-based testing）。
普通单测写的是例子：“输入 A，得到 B”。属性测试写的是规律：“对所有输入，这件事都必须成立”。工具会自动生成大量输入去撞，撞到反例后，还会把它缩到最小。Python 里有 Hypothesis，JS/TS 里有 fast-check。
Anthropic 今年 1 月也发过一篇思路相近的文章：让 Claude 读代码、猜规律、写 Hypothesis 测试，在 NumPy、SciPy、Pandas 里找到了 bug。
我拿一个分和元互转的小函数试了一下：把以“分”为单位的整数，转成“¥1,234.56”这样的字符串，再解析回来。
defformat_yuan(fen:int)->str:yuan,cents=divmod(fen,100)returnf"¥{yuan:,}.{cents:02d}"看起来没毛病吧？
先写 8 条普通单测：0、5 分、整元、千分位、百万级、解析带不带角分，最后一条是几个手挑的往返例子。
结果：8 passed。
再换成属性测试。不写任何具体例子，只写一条规矩：任何整数，格式化以后再解析，都不能变。
@given(st.integers())deftest_roundtrip(fen):assertparse_yuan(format_yuan(fen))==fen跑一次，0.14 秒，失败。Hypothesis 给出的最小反例是这样的：
E AssertionError: assert -199 == -1 E + where -199 = parse_yuan('¥-1.99') E + where '¥-1.99' = format_yuan(-1) E Failing test case: test_roundtrip( E fen=-1, E )退款 1 分钱，显示成了 ¥-1.99，解析回去变成了 -199 分。
原因是 Python 的divmod对负数向下取整：divmod(-1, 100)得到的是(-1, 99)。
8 条单测为什么全过？因为里面全是 0 和正数，一个负数都没有。测的都是写测试的人想到的情况，bug 恰好藏在没想到的地方。
我又换了 50 个随机种子，各跑一次。50 次都失败，每次都缩到同一个最小反例：fen=-1。
修复只要两三行：先取符号，再对绝对值做divmod。修完以后，属性测试和原来的 8 条单测一起跑，9 passed。
| 单元测试 | 属性测试 | 形式化证明 | |
|---|---|---|---|
| 写的是什么 | 几个例子 | 对所有输入都成立的规律 | 规律，加一份证明 |
| 能说明什么 | 这几个例子是对的 | 抽查没找到反例 | 所有输入都满足规律 |
| 今天谁能用 | 所有人 | 所有人 | 极少数项目 |
负面提示词，为什么好用？
拿我自己来说，我给 AI 写的要求，越来越多是这种形状：“不要编数据”“不要改已经确认的部分”“不要自己放宽验收标准”。这比“请认真写”“请保证质量”管用。
原因在于，一句“绝不能”，天然是一句对所有情况都成立的话。
“不能编数据”，意味着文章里每一个数字都得有出处。它是一条规格，一个不变量。AI 可以拿着它，一条一条去对，去找反例。
“写得专业一点”呢？它只是一种感觉。AI 只能猜你想要什么样，你也没法拿它去检查，到底哪一句违反了它。
单测和属性测试的区别也是这样。“输入 123456，得到 ¥1,234.56”是一个正面的例子；“任何整数，转过去再转回来，都不能变”是一条规矩。前者只覆盖你想到的情况，后者逼着工具、逼着 AI 去找你没想到的情况。
所以我会认为，负面约束好用，是因为它把一个模糊的期望，变成了一条可以被撞、可以被检查的规则。
那么，跟 AI 协作的时候，规则该怎么找？结合这篇文章和这个 demo，我整理了五条可以直接用的做法。
第一，先问“对所有输入，什么必须成立”
让 AI 写代码、写测试之前，先让它回答这个问题，而不是先列几个例子。答案写出来，人只审这几行。
第二，从几种常见的规律里找
原文列过模糊测试常检查的几类规律，下面这四种最好上手：
- 往返：编码再解码、格式化再解析，必须拿回原样。demo 里抓到 bug 的正是这一条。
- 幂等：同一个操作做两次，和做一次的结果一样。
- 不变量：比如排序前后，元素个数不变。
- 对照：新实现和旧实现、和参考实现，给同样的输入，结果必须一致。
第三，写一份“绝不能出现”清单
Anthropic 的规格本身是一条“绝不能”：任何输入都不能让程序崩。放到自己的项目里，可以是“金额转一圈不能变”“已经确认的结论不能被改掉”“引用不能没有出处”。每一条都要具体到，能检查出是不是被违反了。
第四，规矩要连“怎么满足”一起管
AI 也会走捷径。只写“测试必须通过”，它就有动机去改测试；只写“不能崩”，它就有动机把程序改成什么都不做。所以要像 Anthropic 那样，再补一条：每次改动都要说明改了什么、影响了哪些输入，并且留下记录。
第五，人定规则，AI 去撞，机器判卷
定规则是人的活，找反例是 AI 的活，判卷交给机器：测试框架、类型检查、证明检查器。别让写代码的那个 AI，自己给自己判卷。
规则写成“不能发生什么”，AI 才知道该去哪里找反例。
别人怎么看？
这篇文章出来以后，也有不少冷静的声音。
Hacker News 的讨论里，有一类常见的质疑：你怎么知道 AI 证明的，正是你想要的？规格和你真正的意图之间，隔着一段距离。
这恰好说明了人该站在哪。证明可以交给 AI，判卷可以交给检查器，“这条规格是不是我想要的”，只能人来回答。
threatline 的分析更直接：文章里唯一能独立核对的 libexpat 漏洞，四个月前就已经作为 CVE 公开了。他们的结论是，应该把这次看作“验证吞吐量的跃升”，而不是“这些库都安全了”的保证。
Dragonfly 的 Haseeb Qureshi 说得也中肯：它不是万能药，但比凭感觉测过强得多。
审不过来，靠什么验收？
上一篇我写 Lauren Tan 一个月 2000+ 个 PR，结论是：靠人一行行审，审不过来，但独立验收这一环不能消失。
这篇文章让我看到了验收的另一种做法：人不去追着几十 KB 的实现看，而是把一百来行“什么绝对不能发生”写清楚，让 AI 去找反例，让机器判卷。
AI 写代码的速度已经上来了，跟不上的是验证。
上一篇最后我说，能放手多少，取决于验收靠不靠得住。现在我多了一个答案：验收靠不靠得住，先看规则有没有写清楚。
- 本文读的原文：Anthropic《LLMs are making formal software verification feasible at a much larger scale》，https://www.anthropic.com/research/formal-verification
- 原文附录：https://www-cdn.anthropic.com/files/4zrzovbb/website/6867eadf760258fa8b42a504600cd3c036d16358.pdf
- 公开的证明仓库：https://github.com/theorem-labs/oss-verify-proofs
- Anthropic 的属性测试文章：https://www.anthropic.com/research/property-based-testing
- Hypothesis：https://hypothesis.readthedocs.io/ ，fast-check：https://fast-check.dev/
- Hacker News 讨论汇总（daily.dev）：https://daily.dev/posts/llms-are-making-formal-software-verification-feasible-at-a-much-larger-scale-oarwz7iku
- threatline 的分析：https://agentblog.threatline.io/posts/claude-formal-verification-123-libraries/
- Haseeb Qureshi 的评价转引自 WebProNews：https://www.webpronews.com/anthropic-theorem-claude-formal-verification-oss-fuzz/
