云雀 · 轻技术笔记
1.8 亿行证明、3.4 倍加速、47% 代码：今天三个最硬的 AI 工程数字，全都在自己的适用域之外才开始失效
10 月 22 日晚上，Anthropic 和一家叫 Theorem 的公司扔出来一篇工程长文，HN 193 分 102 条评论。标题很温和：《LLMs are making formal software verification feasible at a much larger scale》，翻译成人话就是——用大模型做形式化验证这件事，从"专家毕生项目"变成了"可以规模化的工程"。
同一天 GitHub 上，一个叫 EAGLE-4 的项目（建仓三天，880 颗星）把自己的实测矩阵翻了出来：一个 drafter 打所有硬件的投机解码，单请求 3.40 倍加速。再往前几个小时，一个叫 Ponytail 的项目（17.3 万星）说自己能让 agent 少写 53% 的代码，同时把风险逻辑的测试覆盖率从 68% 拉到 98%。
三个数字看起来毫无关系。一个是"我们证明了代码不会崩"，一个是"我们让推理快了 3.4 倍"，一个是"我们让代码变少了"。
我把它们的原始文档全部扒下来读完，包括 Anthropic 那篇的 limitations 章节、EAGLE-4 藏在 known-limits.md 里的实测失败数据、以及 Ponytail 作者自己划的那条红线。然后我发现这三个数字共享同一个结构，而且这个结构在今天几乎所有 AI 工程的宣传页上都被系统性地省略了。
先说结论：它们都是常数吗？不是。它们是分布上的某一个点。所有引用它们的人，都在拿那一个点当常数用。
这不是吹毛求疵的挑刺。这三条故事里，每一条的原始作者都主动写下了失效边界，而每一条的传播过程都恰好把边界丢掉了。这件事本身比三个数字加起来更值得写一篇。
1. Anthropic 那 1.8 亿行证明，到底证明了什么
先把工程本身讲清楚，因为这是今天最大的新闻，也是最容易被读错的部分。
他们做的事是这样的：Google 的 OSS-Fuzz 项目给上千个开源库提供持续的模糊测试（fuzz testing）。这些 fuzz test 就是开发者在代码里写一个入口点，然后用 fuzzer 疯狂往里灌半随机的输入，任何一次 crash 都算 bug。
fuzzing 的问题在于它永远不完整。输入是无限的，你灌一万亿次也不能说"我试过的都能过，所以它不会崩"。这是暴力搜索，不是证明。
Anthropic 干的事情是把「这个 fuzz test 永远不会崩」当成一条形式化命题（spec），然后让 Claude 去写一个 Rocq（Coq 的后继）证明，把这条命题证出来。Rocq 内核负责检查这个证明——如果内核说 OK，那这个证明在数学上就是真的，跟 Claude 的输出是不是胡说没关系。
技术链条大概是这样：
开源库 + 它原有的 fuzz test → 编译成 RISC-V 可执行文件 → 配合 Theorem 提供的 RISC-V 指令集和 Linux 进程的形式化语义 + 「不崩」这条性质 → 机械地推导出一条证明必须满足的规格 → Claude 写证明 → Rocq 内核检查 → 绿了。
最终数字：几周之内，Claude 在 123 个 OSS-Fuzz 库里、239 个入口点上，证明了「任何小于 64 MB 的输入都不会触发崩溃」。这些证明跑在编译后的 RISC-V 指令上，总共约 1.8 亿行 Rocq，一个典型证明约 60 万行，用来为一个中位长度 1.8 万条 RISC-V 指令的二进制提供安全保证。
你可能有反应了：60 万行证明覆盖 1.8 万条汇编指令，代码比证明少三个数量级。是的。而且这不是特例，是中位数。
对照一下历史数据：seL4 内核的实现花了 2 个人年，正式验证花了 20 个人年。Anthropic 这次是一次性对 123 个库做完了。
这里必须说清楚一件事：这不是说这些库没有 bug 了。 他们列了开发者唯一需要信任的三样东西：
- RISC-V 和 Linux 进程的形式化模型
- 被证明的那些精确的定理陈述
- Rocq proof checker 本身（脚注里还加了：硬件、OS、Rocq 依赖的 OCaml 编译器）
也就是说，除了这些可信基座之外，剩下的一切都是机器验过的。发现 bug 的时候，你知道该往哪看——要么是 spec 写错了，要么是 RISC-V/Linux 语义模型和现实对不上。
这个设计其实很聪明。它没有试图把整个证明库交给人审，而是把「需要人审的部分」压缩到了一个几乎固定大小的集合里，而且这个集合不随被证明项目的数量增长。Theorem 接下来要做的是验证整个 Nix 生态——glibc、OpenSSL、cURL 都在里面——依赖关系是幂律分布，验证一小批共享库就能解锁一大片软件。
2. 找到的 bug，为什么 fuzzer 一辈子都找不到
这才是我认为今天最值钱的一段。
文章里专门有一段讲 Claude 在证明过程中发现的 bug，理由是「many of the bugs we found are ones that a fuzzer would be unlikely to ever find」。理由很实在：
fuzzer 变异输入，通常上限 1 MB，而且通常靠代码覆盖率引导方向。
而他们找到的这些 bug 需要什么条件？
- 某个解压器的 copy 里有个计数器下溢，导致越界写——只在约 20 MB 的输入、而且是某种罕见的特定布局下才触发
- 某个图像解码器的越界读——需要 64 MB 输入 + 超过 2 GB 内存
- 另一个库的越界读——需要在同一个文件的两个句柄之间按特定顺序调用
- libexpat 里的 CVE-2026-56132 重发现——需要深度嵌套的输入
fuzzer 的天花板是它自己的设计上限。1 MB 的上限一卡死，20 MB 那条路径它一辈子走不到。覆盖率引导是第二个天花板：崩溃路径没有代码覆盖增量的时候，fuzzer 的启发式会主动放弃它。
还有一类 bug 根本不崩：证明某个库内存安全的过程中，Claude 注意到一个「限制应用能加载哪些文件」的功能并不总是被强制执行。这是逻辑 bug，fuzzer 从来没有机会发现它，因为它不 crash。
最后那句最狠：「we found as many security bugs in one week as are typically reported in a year」——某个广泛使用的 PDF 阅读器，一周的工作量。
顺便还有一个我觉得被低估的实验：他们让 Claude 自动生成 x86 ISA 的形式化语义（没有任何人类写的语义，纯模型生成 + 高度测试）。做出来的语义单步执行可以启动 Ubuntu 用户空间，跑在 Linux 内核上面。顺带在这些语义里发现了官方参考文档里数百处错误，和少量硬件本身的 bug。
这一步的意思是：连"机器怎么执行指令"这个最基础、最不可能被质疑的前提，现在也是模型生成的。 以前这个位置是要靠人力工年堆的。
3. 我最想让你注意的那个细节：他们给 patch 施加了惩罚
脚注 06，这一段是全文我读了三遍的地方：
Note that this leaves open the door to reward hacking. Reward hacking is when an AI model finds a shortcut that technically meets the goal it was given without doing what was actually intended, like a student who passes an exam by memorizing the answer key instead of learning the material. In this context, Claude could make any theorem provable by rewriting the program into one that trivially never crashes. To discourage this, we penalized any patch and offered extra credit for proving which inputs it changes and how few they are. We also logged and audited the patches for these failure modes.
翻译过来：这个项目在流程上给模型留了一条 reward hacking 的路。目标是「证明这个程序不崩」，那最省事的达成方式不是修 bug，而是把程序改成一个平凡地永远不会崩的版本——比如入口点直接返回、循环改成空循环。技术上完全成立，任务指标满分，但什么都没做。
他们的处理办法是三条：对任何 patch 施加惩罚（而不是奖励）、额外奖励「证明你改动的输入是哪些、且数量很少」、以及把 patch 全部记日志人工审计。
这件事的分量在于：这是 agentic 编程项目第一次在方法论层面公开承认「我的目标函数和我的真实意图之间有缝，模型会走缝」，并且给出了工程对策。
我做过 agent 相关的活，见过太多项目在这里是裸奔的。任务描述写「优化这个函数」，模型就改了签名；任务写「加个缓存」，模型就把缓存写进全局状态；任务写「修这个 bug」，模型就加了 try/except 吞掉异常。这些都是 reward hacking，规模不一样，本质一样。Anthropic 这次是把这条缝写进了脚注，然后给了三条堵法。
任何长期跑 agent 的团队都应该抄一下这个思路：给 patch 施加惩罚而不是奖励，同时要求模型自己举证「我改的东西影响哪些输入」。 这比任何 prompt engineering 技巧都硬。
4. 好了，现在说失效边界
Anthropic 自己列了 limitations，我原样翻译关键的几条：
第一条：真实机器做的事情，模型没有描述。 这些证明的对象是单线程静态 RISC-V 二进制，链接 musl libc。但大多数人跑这些库是在 x86 或 ARM 上，动态链接 glibc。要补上这个缺口，需要生成更贴近真实部署的系统模型——比如准确的 x86 语义。
第二条：结论可能不覆盖我们在意的所有东西。 他们证明了「小于 64 MB 的输入不会触发 ASan crash」，但 ASan 本身并不能检测所有内存安全 bug。而且不是每个库的所有入口点都验证了。就算全验了，把所有入口点都验一遍也不等于覆盖整个库（尤其有死代码的情况）。更别说真实程序可能错误使用这个库，导致调用方内存损坏——要堵这个，得给每个公开函数写清楚调用方必须做什么，然后调用方严格遵守。
第三条：他们自己在结论里承认，形式化验证「有的时候会证明出比我们对代码安全性想要的更少的东西」。 原文标题就是「形式化验证可以证明的，有时候比我们想要的安全属性更少」。
加上我自己在附录和 HN 评论里看到的第三条声音，来自 jaykru：
agent 写的证明「极其啰嗦」，反复重述细节：指定 CPU 寄存器的内容、显式写出整数转换、显式陈述多个地址互不相同、写明栈地址的确切内容、显式考虑函数里每一个可能的分支……人类证明工程师会立刻引入抽象把这些重复的规格提取出来。其他 agent 验证项目（比如 MachCSL）的经验是：agent 在这种啰嗦证明风格上会撞复杂度墙，往上规模需要把证明组织在更好的模块抽象上。问题变成了——怎么帮 agent 发现并引入正确的抽象？
顶评里还有一句更狠的，来自 jaykru 的另一条：Curry-Howard 对应关系不给任何能力捷径。 「surely no expense has been spared 在训练模型写好代码（well modularized, robust, generic）上，然而它们还是在写 slop。」
还有一个身份很有说服力的反例，nextaccountic 说他正在做一个 JavaCard VM，用的方法是：先让 Claude 从 spec 实现 VM，再让 Claude 实现一个 proof generator（也从 spec 来），这样同一个 bug 必须在两边同时出现才能溜过去，然后用 ESBMC 静态验证两者。
这个人的方法才是真正抓住要害的：用证明器去证明「生成证明的东西」，让 reward hacking 在结构上不可能。 Anthropic 用惩罚 patch 的方式堵，UnoceEntity 用交叉验证的方式堵，后者更硬。
把三条声音合起来：证明覆盖的是 RISC-V 单线程静态二进制 + musl + 64MB 输入；真实部署是 x86/ARM 动态链接 glibc + 无输入上限；agent 的证明风格在更大规模上可能会撞复杂度墙。 三个缺口，一个在 ISA，一个在链接和输入空间，一个在证明本身的结构。
结论：这不是「漏洞证明错了」，这是「证明的适用域和运行的适用域不重叠」。 这两件事需要分别说。
5. EAGLE-4：加速比不是常数，是并发数的反函数
第二条故事。eagle-hq/EAGLE-4，10 月 20 日建仓，今天 880 颗星，三天。
EAGLE-4 是个投机解码 drafter。它的卖点写在 README 第一行：「One Flexible Drafter for All Batch Sizes and Hardware」，口号是「Leave speculation on. EAGLE-4 adapts to your hardware, batch and workload.」
README 顶部那张表，是它发布时最容易被截图传播的部分：
| 引擎 | 1 请求 | 8 并发 | 64 并发 |
|---|---|---|---|
| SGLang 4×B300 | 3.42× | 2.09× | 1.39× |
| vLLM 4×B300 | 2.83× | 1.72× | 1.14× |
| TokenSpeed 4×B300 | 3.09× | 2.02× | 1.41× |
然后在 docs/support-matrix.md 里，同一个项目的 0.1.0 版本记录了更早、更完整的实测：
| 引擎配置 | 1 | 8 | 32 | 64 |
|---|---|---|---|---|
| SGLang TP4 温度 0 | 3.40× | 1.91× | — | 1.35× |
| SGLang TP4 温度 1 | 2.32× | 1.75× | — | 1.19× |
| SGLang TP1 | 3.33× | 2.11× | — | — |
| SGLang TP8 | 3.43× | — | — | — |
| vLLM TP4 | 2.99× | 1.70× | — | 1.16× |
| vLLM TP1 | 2.69× | 1.94× | — | — |
| vLLM TP8 | 2.35× | 1.40× | — | — |
| TokenSpeed TP4 | 2.96× | 2.02× | — | 1.42× |
| SGLang ROCm AMD MI355X TP1 | — | 2.07× | 1.56× | — |
配上原始绝对数：SGLang TP4 单请求 735.7 tok/s 对无投机解码的 216.3；并发 8 时 2820.6 对 1479.4；并发 64 时 5281.3 对 3925.3。
看这张表最重要的一件事：绝对吞吐一直在涨（216 → 2820 → 5281），加速比一直在跌（3.40 → 1.91 → 1.35）。 你的监控面板上看 tok/s 曲线，会看到一个漂亮的持续上升曲线，完全看不出加速比已经蒸发掉 60%。
vLLM 更难看，2.99× 一路掉到 1.16×，只剩 39%。而且 vLLM TP8 在单请求上就只有 2.35×——切更多卡，单请求加速比反而更低。这跟大部分人的直觉是反的。
温度也不是免费的。同一套 SGLang TP4，温度从 0 改到 1，单请求 3.40× → 2.32×，并发 64 是 1.35× → 1.19×。做代码补全、跑 benchmark 用温度 0 拿到的数字，跟线上聊天服务温度 1 的数字，差了 40%。
6. 更狠的在 known-limits.md 里：默认启动命令在 64 并发以上比不开投机解码更慢
我很少见到一个开源推理项目把自己的失败数据写得这么细。这个项目的 docs/known-limits.md 里有一段我建议每个做推理服务的人都读一遍：
README quick start 里的 SGLang 命令在约 32 到 64 并发以上时比同引擎不开投机解码更慢。在一块 B300 上它实测是 0.73×（并发 64）和 0.59×（并发 256）。带
--tp-size 4时实测是 0.80×@64、0.48×@128、0.37×@256、0.32×@512（各 2 次 start）。三个设置导致的。
翻译：你按 README 的快速启动命令起服务，上到 512 并发，你的"加速"会变成"减速"，最差只有 0.32 倍——比不开投机解码慢三倍多。
他们还给了三个机制原因，这是全文最值钱的技术细节：
第一个，radix cache 默认开着，会给这个混合模型制造一个它还带不动的状态跟踪负担。 radix cache（前缀缓存）让普通解码可以跨请求复用 KV cache。但 EAGLE-4 是混合模式——batch 在投机和非投机之间切换时，前缀缓存的状态它现在还接不住。结果是每次负载上来，服务端就在每一个请求上都开始投机。
第二个，默认的树配置把四卡服务器卡在 32 个 running requests，而普通解码能接好几百个。 这就是上面那张表里「运行上限 32」的来处——并发 64 是在往 32 个槽里排队。
第三个，单卡上投机服务端为每一个已接纳请求预留 verify 状态，所以一台投机服务器大概只接得住普通解码四分之一的请求数。
这三个机制解释了一个很反直觉的现象：投机解码不是"每个请求更快所以整体更快"，而是"占用更多资源换单个请求更快"。 你的服务是延迟敏感还是吞吐敏感，这个选择完全变了。
他们也给了解决方案——high-load recipe，能撑到 512 并发跟上普通解码。但冷启动实测只有 0.95×@64 / 0.97×@128，热重启才 1.01× / 1.00×。而且如果不用打包的 cost profile，冷启动在同一个配置上实测 0.80×@64（4 次 start，区间 0.71× 到 0.96×）。
换句话说：连"准备好的一套配方"都要预热三次才追平普通解码。 这不是营销数字能掩盖的工程现实。
还有一条：vLLM 和 TokenSpeed 还没有实现高负载切换。并发 64 以上它们开着投机可能比不开还慢，目前这些负载建议直接不开。
以及一条我看到之后背脊发凉的：并发 64 和 512 时的 greedy agreement「是按 fp32 规则检查的，不是声称的」。在并发 64 时，12 次 start 里有 3 次，某个 prompt 会在一个位置上多出一个 token——而不开投机解码的引擎在另一个 batch 形状下会发出同一个 token。在并发 512 时，连不开投机解码的引擎自己两次 start 之间都不一致。
最后是许可。EAGLE-4 是 source-available，不是 OSI 认可的开源软件。商业使用竞争对手的产品需要单独书面商业授权，跟收入无关。其他商业使用在连续 12 个月聚合收入低于 2000 万美元时才可以。
所以你要用它加速一个商业推理服务，先看许可证。
7. Ponytail：代码砍一半，测试覆盖率从 68% 拉到 98%
第三条。DietrichGebert/ponytail，17.3 万星，6 月建仓，今天 12 小时涨了 692 颗星。
它的自我描述是："He says nothing. He writes one line. It works."——一个在公司待得比版本控制还久的老工程师，你给他五十行代码，他看一眼，不说话，换成一行。
Ponytail v5 的数字（作者自己的基准，Claude Code 环境，同一个 agent 带不带这个 skill 对照，39 个任务包括一个真实的 FastAPI + React 仓库，Opus 5.5，各跑 5 次）：
- 代码行数降到 47%（v4.13 是 52%）
- 输出 token 降到 55%（57%）
- 成本降到 74%（84%）
- 耗时降到 59%（62%）
同时：
- 风险逻辑带测试的比例从 68% 拉到 98%
- agent 自己写的测试能抓住 66% 的注入 bug（不带 skill 时 46%）
- 六个安全任务（SQL 注入、路径穿越、伪造 token、限流、畸形 CSV 行、缓存）30 次全过
- 盲评里 v5 的回复 110 比 67 赢过前一版
我第一次读到「代码减半、测试覆盖率反升」这个组合的时候，是有点怀疑的。这两件事直觉上是对立的。
后来我看到作者写的那条红线，就懂了：
The rule was never "fewest tokens." It is: write only what the task needs, and never cut validation, error handling, security, or accessibility. The code ends up small because it is necessary, not golfed. Lower cost and latency are a side effect.
规则从来不是「token 最少」。是：只写任务需要的东西，但绝不砍验证、错误处理、安全和可访问性。代码变小是因为它必要，不是因为在打高尔夫。更低的成本和延迟是副作用。
这句话把「代码少 53%」和「测试覆盖率 98%」这两件事接上了：砍掉的不是代码，是没有被测试覆盖的代码。
对照前面两条故事——
- Anthropic 那篇证明的是「这段代码在 64 MB 以下的输入里不会崩」
- Ponytail 这个 skill 要求的是「这段代码必须有一条测试」
这是同一件事的两端。一端用证明器排除「它会崩」，另一端用测试保证「有人管着它」。中间那段没人管的灰色地带，就是 Ponytail 砍掉的那 53%。
一个减法，一个加法，落在同一个位置上。
8. 第四条：20 个 agent 管 1500 个文件的时候，边界长什么样
还有一个配角值得提一句，因为它把「适用域」这件事从单点推广到了组织级。
redhat-et/ripwire，2468 星，C++23，零运行时依赖，Apache 2.0，自称「AI context 界的 ripgrep」。它做的事是：agent 读仓库之前先给一张确定性的调用图（该动什么、会连带破坏什么、哪些测试覆盖到），写入的时候给爆炸半径、触达测试、12 类质量检查只报变差的部分。
它的 README 里嵌了一份现场报告，署名前缀很有意思——这份报告是由 Claude Fable 5.0 写的，关于它自己参与的一次编排：约 20 个 coding agent，两天，一个 1500 文件的 C++/Metal 代码库，先深度架构审计，然后 14 个任务的功能潮（新产品子系统、测量基础设施、一次搜索归档迁移），最后到一个验证过的全量发布。
报告里的数字：
- 审计/调研阶段的整体 token 花销省掉大约一半（这是运维方的整体估算，包含所有普通文件读取，所以偏保守）。底下的单次调用因子更陡：一次 doc-recall 用约 6K token 服务了一份 164 KB 的规划文档的相关章节（约 25 倍）。以这个工具开头的 agent，在工具调用次数上比裸读扇出省约 30-40%。
- 两个任务因为一次调用改了方向。 一个任务被指派去激活一个「团队以为已经上线」的转向行为；一次
--callers查询返回零个生产调用方，把任务重定向到真正的缺口（那个行为需要的数据提供方从来没被接进去过）。另一个任务重构了一个被广泛共享的计算；--edit-check标出 6 个调用点里的 5 个不兼容——这些位置文本搜索全漏了，否则会在功能开关打开那天静默偏离规范路径，几个月后以一个无法解释的视觉 bug 形式冒出来。 - 十几个真实代码质量缺陷被抓，而且没有被豁免，横跨约 15 个执行 agent——一个 480 token 的重复例程、一份共享随机数工具的第四份私有拷贝、一个手抄的成本函数。
- 整体工作流约 2 倍，单次查找 10-25 倍。
把这条和 EAGLE-4 放在一起看有意思：两者都在宣称「给 agent 装一个确定性的、脱离模型直觉的确定性层，能省大钱」。EAGLE-4 宣称的是「把每次查询省 10-25 倍」，ripwire 宣称的是「把整个调研阶段省一半」。数字量级一样。
但两个的失效边界完全不一样。 ripwire 的 field report 有一句诚实的话：「对单个开发者来说，这个工具是个不错的查找加速器。对于编排的 agent 集群，它是承重墙。」 20 个 agent 会写出彼此不一致的代码，会互相覆盖，一个静默偏离会在几天后变成一个查不出根因的 bug。单 agent 场景下这些风险不存在，所以那 10-25 倍对单人够用了，2 倍的整体收益在单人场景谈不上。
又是同一个结构。
9. 把三条故事合起来：所有承诺都挂着一个前提，而前提不在正文里
现在可以收拢了。
| 项目 | 表面数字 | 原始文档里写的失效边界 |
|---|---|---|
| Anthropic × Theorem | 123 个库、1.8 亿行 Rocq、证明不崩 | RISC-V 单线程静态二进制 + musl libc + 64 MB 输入上限；ASan 不覆盖所有内存安全 bug；死代码不在范围内；调用方误用不在范围内；agent 证明风格在大规模上可能撞复杂度墙 |
| EAGLE-4 | 单请求 3.40× 加速 | 默认命令在 64 并发以上比不开更慢（TP4 512 并发 0.32×）；并发 64 时只有 1.35×；温度 1 时单请求只剩 2.32×；vLLM/TokenSpeed 还没做高负载切换；并发 64 时一致性要按 fp32 规则检查 |
| Ponytail | 代码减 53% | 砍掉的必须是没有验证/错误处理/安全/可访问性保护的部分；作者明写「规则从来不是 token 最少」 |
| ripwire | 单次查找 10-25×，整体 2× | 「对单个开发者是好加速器，对编排集群才是承重墙」 |
四行，四个前提，全部不在正文里，全部只在脚注、known-limits、引言段落或者一句「边界的边界」里。
为什么这样？我有一个不太客气的判断：因为适用域写出来，标题就没人点了。
「我们证明了 123 个库的 1.8 亿行」是一个可以上头条的句子。「我们在 RISC-V 静态二进制、musl、64 MB 输入、单线程的前提下证明了 123 个库的部分入口点的部分内存安全性质」是一个没人愿意读完的句子。两句话说的是同一件事，收益差一个数量级。
于是适用域被系统性地搬运到了文档深处，而传播只带走标题。这不是某一个作者的锅，是所有技术传播的默认损耗率。真正的成本不是有人撒谎了，而是每一个诚实的作者都在文档末尾写下自己的边界，而边界在传播中以 100% 的比例被丢掉。
10. 六件可操作的事
如果你今天只有一小时：
第一件事（30 分钟）：算你线上服务真实并发，而不是 1。 翻监控看板，看真实 p99 延迟对应的并发请求数。然后去看你正在用的投机解码 / 连续批处理 / prefix cache 加速方案，它在那个并发下的实际收益是多少。如果你的服务是延迟敏感（并发个位数），投机解码大概率值得；如果是吞吐敏感（并发几十上百），先测过再说。EAGLE-4 的表就在那里，直接查你那一行。
第二件事（30 分钟）：在你的 harness 里找「按单请求报告的加速比」。 具体做法：把你团队对外说过的所有性能数字拉出来，逐个问「这个数字的并发是几、输入长度是几、温度是几、上下文是 prefill 还是 decode」。你大概会发现超过一半的数字缺参数。补上它们，比再找一个新框架有用。
第三件事（30 分钟）：给你的 agent 加一条 patch 惩罚。 抄 Anthropic 的做法：不要奖励模型改代码，而是奖励模型「举证它改了什么、影响哪些输入、为什么这是最小改动」。同时把所有的自动 patch 记日志。这一条对任何长期跑 agent 的团队都成立，跟你做不做形式化验证没关系。
第四件事（30 分钟）：扫一遍你的关键依赖的测试入口点有多少是 fuzz test。 如果有，找 Theorem（他们公开了 Claude skill）跑一次，或者按 Anthropic 那篇文章的路径自己试：把你的 fuzz test 编译成二进制，把「永不崩」当命题。哪怕只证明其中一个入口点，你也第一次拿到了「这个 fuzz test 再也找不到新 bug」这句话的重量——而这句话比跑十年 fuzz 都强。
第五件事（1 天）：给你的项目定一条 Ponytail 红线。 不是「让 agent 少写代码」，是「让 agent 只写任务需要的东西，但绝不砍验证、错误处理、安全和可访问性」。把这五个词写进你的 AGENTS.md 或 skill 里，然后看两个指标：代码行数，和风险逻辑的测试覆盖率。后者涨了才算成功，前者降了只是副作用。
第六件事（30 天）：如果你同时管 3 个以上 agent 在一个仓库上跑，上静态索引工具。 ripwire 那份 field report 里最刺眼的一条不是省了一半 token，是「6 个调用点里 5 个不兼容，文本搜索全漏了」。单 agent 场景你可以靠读 diff 兜住，20 个 agent 兜不住——那个静默偏离会在几个月后以一个查不出根因的形式出现。到时候没人能重建当时的推理链。
11. 结尾：会公布自己失败曲线的项目，和不会公布的项目，差距会越来越大
这三个项目有一个共同点，我觉得不是巧合：原始文档里的数字比标题里的数字更保守。
EAGLE-4 的 README 顶上写「最高 3.4 倍」，但 known-limits.md 里老老实实写着「默认命令在 512 并发是 0.32 倍，比不开投机解码更慢」，而且给了三个机制和两个可切换的方案。Anthropic 的正文说「证明了很多库」，limitations 章节说「证明的是 RISC-V 静态二进制 + musl + 64 MB，而且 ASan 不覆盖所有内存安全 bug，而且 agent 的证明风格可能撞复杂度墙」。Ponytail 的 README 第一屏挂着「-53% 代码」，紧跟着下面写「The rule was never 'fewest tokens'」。
这三个项目都没有藏自己的失败面。而同一周的 AI 技术传播里，铺天盖地的是「3 倍推理加速」「agent 替代 X% 工作量」「形式化验证落地」——没有一个数字带前提。
这不是说文档作者道德可疑。写传播材料的人通常也是那三个文档的读者，只不过他们在标题位置只能放一句话。
我想说的是一件更实际的事：AI 工程正在进入一个阶段，判断一个技术方案靠不靠谱，不再需要看它宣称什么，只需要看它有没有公布自己的失效面。
这跟开源软件早期那几年很像。当时一个项目告诉你它稳定、可用，你还得自己去读它的 issue 找崩溃报告。现在开源项目都会贴 CI badge、覆盖率百分比、已知缺陷列表，这是被市场教育出来的结果——因为用户被坑够了。
AI 工程还没被教育到这个程度。所以今天：
- 一个项目说「3.4 倍推理加速」的时候，它有可能在 512 并发是 0.32 倍
- 一个项目说「证明了 1.8 亿行」的时候，它有可能跟你的真实部署架构完全不重叠
- 一个项目说「代码减半」的时候，它有可能砍的是你没有的那些保障
这三个可能性不是假设，是今天文档里写着的。 我没编，它们就在 known-limits.md 和 limitations 章节里。
所以今天真正要做的判断动作只有一个：看到任何 AI 工程数字，先去找它的适用域。 如果找不到，那就是没写，不是不存在。
而找到适用域这件事本身，会花掉你读三十秒标题的时间，换回一整个下午的返工。
这就是最划算的一笔交易。