确定性刹车实测:agent 说的每句话,先过工具这一关

一、为什么我盯上这个项目前面 DseWiki 那篇我拉了那个废弃 wiki 上的 14,591 条留言,结论很冷:agent 之间会自己交接、自己定规矩,没有一条想到通知人类。当时稿还没发,OpenAI 官方就确认了这起事件(前后不到 48 小时),说在搞披露框架。官方在补制度,工程侧在补工具。今天说的这个工具叫 reverify,2026 年 8 月 31 日建仓,我 9 月 7 日抓取时 961 星、207 fork,MIT 协议。它的口号一句话能说完:“Stop your AI from making things up.”模型只负责提出断言(claim),关于二进制的每个结构性陈述都由一个纯 Python 的确定性工具对照真实字节检查,返回 VERIFIED / REFUTED / INCONCLUSIVE,外加证据。模型永远不能自己宣布一个事实。它选的切入点很刁:二进制逆向。这是幻觉最重的地方——模型读源码还靠谱,对着二进制猜结构体偏移、猜函数序言,错得理直气壮。二、第一次跑:它不敢判clone 下来,核心只用标准库(capstone、lief 这些都是可选增强,不装就回退到纯 Python),Python 3.12 直接能跑 CLI。先看后端状态:$ python reverify/cli.py backends disassembly pure-python emulation pure-python binary_parsing lief 0.12.3- proof none semantic pure-python我机器上本来就有 lief,反汇编和模拟走的是自带的纯 Python 实现。拿系统里的 kernel32.dll 开刀,先自动分诊:$ python reverify/cli.py auto C:\Windows\System32\kernel32.dll Auto-Triage: kernel32.dll (836208 bytes) Detected Type: Windows PE Binary (EXE/DLL/SYS) Architecture: x86_64 (64-bit) [parser: lief] Sections: .text, fothk, .rdata, .data, .pdata, .didat, .rsrc, .reloc解析 PE 头拿到入口点 RVA 是0x2c500。现在扮演模型。教材里最经典的函数序言是帧指针风格:push rbp; mov rbp, rsp; sub rsp, N(x86 时代刻进肌肉记忆的那种写法)。模型被问到入口序言长啥样时,这个先验几乎是条件反射。我把这个教科书答案写成 claim 提交:[INCONCL.] instructions w0.8 the pure-Python decoder does not handle these bytes; install capstone to judge this claim注意这个反应。它没有猜。自带的纯 Python 反汇编器啃不动入口那段字节时,它给的是 INCONCLUSIVE,并告诉你装 capstone,而不是看着像 push/mov 就算你对。我装过不少 agent 工具,这种判不了就明说判不了的设计是少数。pip install capstone之后(实际装上 5.0.7),重跑同一条 claim。三、REFUTED,附带真实字节$ python reverify/cli.py verify kernel32.dll --claims-file claims_round1.json [REFUTED ] instructions w0.096 modeexact [VERIFIED] export_present w0.3 (CreateFileW) [VERIFIED] section_present w0.2 (.text) Verified 2/3. Trustworthy: False Grounded: False进程退出码是 2——只要有一条被 REFUTED 就非零退出,这意味着它可以直接当 CI 门禁用。REFUTED 不是一句你错了。--json输出里带着它实际读到的东西:actual_mnemonics:[mov,push,sub,mov,mov,mov,cmp,je],actual_operands:[qword ptr [rsp 8], rbx,rdi,rsp, 0x20,edi, edx,rbx, rcx,edx, 1,edi, edx,0x1031]真实的入口是mov [rsp8], rbx; push rdi; sub rsp, 0x20; ...——MSVC x64 的真实风格:把 rbx 存进影子空间,保存 rdi,开栈帧,顺手 stash 两个参数。和教科书的帧指针序言完全不是一回事。第二轮,我照着证据把正确指令序列填回去:[VERIFIED] instructions w0.636 modeexact [VERIFIED] export_present w0.3 (VirtualAlloc) Verified 2/2. Information 0.936. Trustworthy: True Grounded: False这里有个细节值得停一下:全部 VERIFIED 了,Grounded仍然是 False。因为全对太容易刷了——断言文件以 MZ 开头、.text 段存在,这种废话永远正确。它给每条 claim 打了信息权重:只重复已知 fact sheet 的、重复的、全二进制到处都是的模式(比如空 padding、满大街的序言),权重趋近于零;权重从二进制本身实测——内容出现几次、熵多高。信息分过了阈值(默认 1.0)才算 grounded。我这轮 0.936,差一口气。这个设计防的是用废话糊弄裁判,思路明说来自 FActScore 的 CORE 改进:只给真实、有信息量、不重复的断言记功。四、不只是二进制:AI 改的代码,跑一遍才算数README 里有个命令我更感兴趣:equiv——把参考实现和候选实现(比如 AI 重构后的版本)喂同一批输入,输出不一致就返回反例。第一次跑,它又拒绝了:INCONCLUSIVE running candidate code is off by default; set REVERIFY_ALLOW_NATIVE_EXEC1 to enable it (build and run are then confined by reverify.sandbox)执行任意代码默认关闭,要显式开环境变量,且在它自己的 sandbox 里跑。又是 fail-closed。我写了个最小例子:参考实现是a b,候选实现是 AI 风格的优化版,在 b1 时漏加(那种 code review 一眼扫过去很容易漏的边界错误):$ python reverify/cli.py equiv demo_ref.py demo_cand.py --lang python REFUTED candidate differs from the reference on 1/34 inputs witness: input [1, 1] - reference 2, candidate 134 个输入里抓到 1 个反例,把输入和两边输出都摆给你。结论措辞也留了分寸:通过时说的是“tested, not proven”(测过,没证明);想要证明得开 Z3 后端做符号等价,那是另一档强度。验证强度是分层的:proven tested observed,每层都说自己是哪层。五、我自己跑了一遍它的基准测试README 最响的数字是:71 个真实 Windows 系统文件上,模型的教科书答案错 97%,工具全部抓住、0 次放行。这种数字我不替它复读,自己跑:$ python benchmarks/prologue_prior.py --per-dir 40 results binaries tested : 67 prior wrong (hallucination rate): 67/67 100% false VERIFIED (must be 0) : 0 (95% upper bound on the rate: 5.4%) true bytes after 1 feedback round: 67/67 100% environment: reverify 0.11.0, python 3.12.7, Windows-11-10.0.26200, disasmcapstone, parselief脚本逻辑是把教科书序言这个先验盲贴到 67 个系统 DLL 上(它自己从不读反汇编),再看裁判怎么说:先验错误率:我这台机器上是 67/67 100%(它 README 的 71 个文件是 97%,方向一致、样本不同,文件是固定步长抽样的);错的被误判为 VERIFIED:0 次(脚本逻辑是一个 binary 产生一行,n67;Wilson 95% 上界 5.4% 是按 67 算的)。这是安全底线,CI 里每次提交都拿已知错 claim 绝不能 VERIFIED当门禁;拿到一轮反馈后收敛到真实字节:67/67。我对这个数字的理解:它说明的不是AI 多蠢,而是先验在真实世界的分布和教科书完全不同——编译器生成的入口序言本来就不长教材那样。而这类错误,模型自己永远发现不了,因为它听起来完全合理。这正是需要一个外部裁判的原因。六、没测的部分,如实交代三样东西我这篇没碰:MCP 接入:它能作为 MCP server 让 Claude Code / Cursor 直接调用,但 CLI 的verify走的是同一个 Verifier 类,核心裁决逻辑我已经实测;rollover上下文交接:这是它的第二大功能——长任务不靠模型摘要压缩(摘要会丢状态),而是把已验证事实写进 ledger 文件,新会话从文件恢复。安装它会改~/.claude/settings.json等四个 harness 的配置,我没在自己日常环境里动刀。这个思路和我本系列 ARC-AGI 实测的发现正好对上:模型自觉写笔记式的滚动交接会丢记忆,而 ledger 里只存工具验证过的东西,模型的猜测一律不进——幻觉搭不上上下文的便车;angr 语义层 / Z3 证明层:需要额外装重依赖。它对这类分析得出的结论也老实,语义裁决单独标DERIVED档,排在 VERIFIED 下面。另外两处文档与现状的小出入,一并记下:README 的 Status 节还写着 v0.9.0,代码里_version.py已经是0.11.0;包内共 51 个 Python 文件、约 15,510 行(含 tests/ 和 plugins/;README 称有 208 个单元测试)。七、它在 agent 安全版图上的位置这一系列写到第五篇,线索慢慢接上了:DSH 插件市场那篇讲有规矩不等于有人把关;DseWiki 那篇讲agent 会自主行动,且没有任何刹车;ARC-AGI 那篇讲harness 是超参,换个壳分数天差地别;上一篇 SkillSpector 讲扫描工具当线索生成器、不当裁决器——它能挑出嫌疑,但判不了;到这一篇,是工程侧给出的一种刹车形态——把断言权和裁判权分开。模型保留它最擅长的:提出假设、读写代码、组织语言。但这是不是真的这个动作,交给一个不会产生幻觉的东西:字节本身、CPU 模拟器、一次真实运行。裁判不需要很聪明,它只需要确定,并且判不了的时候说判不了。reverify 现在的领地还是逆向工程这一亩三分地(外加 Python/C 的行为等价),claim 的种类也是为二进制分析设计的。但这个模式是通用的:agent 说这个 API 存在,就让它去查真实的包;agent 说重构后行为没变,就跑一遍。凡是能找到 ground truth 的地方,都不该让模型自己当裁判。agent 管不住自己的嘴——那就别让它的嘴直接说了算。附录:核验数据项目数值来源仓库创建 / 最近推送2026-08-31 / 2026-09-06GitHub API,2026-09-07 抓取星 / fork961 / 207同上协议MIT仓库 LICENSE本机版本0.11.0(_version.py;README Status 节写 v0.9.0,文档滞后)本机实跑包内代码规模51 个 Python 文件,约 15,510 行(含 tests/、plugins/;README 称 208 个单元测试)本机统计kernel32.dll 入口点RVA 0x2c500,image base 0x180000000parse-pe --json实跑Round 1(教科书序言)REFUTED,w0.096,退出码 2本机实跑真实入口指令mov/push/sub/mov/mov/mov/cmp/jeREFUTED 证据 JSONRound 2(照证据修正)VERIFIED,w0.636,信息分 0.936,TrustworthyTrue / GroundedFalse本机实跑纯 Python 后端无 capstoneINCONCLUSIVE(拒绝猜测)本机实跑equiv 默认行为拒绝执行,需 REVERIFY_ALLOW_NATIVE_EXEC1 sandbox本机实跑equiv 反例[1,1] → 参考 2 / 候选 1,34 个输入抓 1 个本机实跑基准测试(本机)67 个系统 DLL;先验错误 67/67100%;误放 0(95% 置信上界 5.4%);一轮反馈收敛 67/67prologue_prior.py --per-dir 40环境reverify 0.11.0 / Python 3.12.7 / Windows 11 26200 / capstone 5.0.7 / lief 0.12.3基准输出未实测MCP 接入真实 agent、rollover 钩子安装、angr 语义层、Z3 证明层见第六节相关实测《我用 NVIDIA SkillSpector 纯静态扫了一遍 GitHub 最火的 agent skills能挖出多少注入0 个》—— 纯静态规则为什么一上来全是误报《让大模型给 6,208 条答案打分判对率 94%逐字正确率 6%》—— 和 LLM 当裁判比确定性校验差在哪、强在哪《Sepia 实测我让 agent 自己给自己去 AI 味结果它比我的工具严多了》—— 同一个验收命题在文本上是怎么做的完整导航博客导航agent 安全 / RAG 实测 / AI 代码治理都在这