一、为什么我盯上这个项目
前面 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 w=0.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 w=0.096 mode=exact [VERIFIED] export_present w=0.3 (CreateFileW) [VERIFIED] section_present w=0.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 [rsp+8], rbx; push rdi; sub rsp, 0x20; ...——MSVC x64 的真实风格:把 rbx 存进影子空间,保存 rdi,开栈帧,顺手 stash 两个参数。和教科书的帧指针序言完全不是一回事。
第二轮,我照着证据把正确指令序列填回去:
[VERIFIED] instructions w=0.636 mode=exact [VERIFIED] export_present w=0.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_EXEC=1 to enable it (build and run are then confined by reverify.sandbox)执行任意代码默认关闭,要显式开环境变量,且在它自己的 sandbox 里跑。又是 fail-closed。
我写了个最小例子:参考实现是a + b,候选实现是 AI 风格的"优化版",在 b==1 时漏加(那种 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, disasm=capstone, parse=lief脚本逻辑是把"教科书序言"这个先验盲贴到 67 个系统 DLL 上(它自己从不读反汇编),再看裁判怎么说:
- 先验错误率:我这台机器上是 67/67 = 100%(它 README 的 71 个文件是 97%,方向一致、样本不同,文件是固定步长抽样的);
- 错的被误判为 VERIFIED:0 次(脚本逻辑是一个 binary 产生一行,n=67;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-06 | GitHub API,2026-09-07 抓取 |
| 星 / fork | 961 / 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 0x180000000 | parse-pe --json实跑 |
| Round 1(教科书序言) | REFUTED,w=0.096,退出码 2 | 本机实跑 |
| 真实入口指令 | mov/push/sub/mov/mov/mov/cmp/je | REFUTED 证据 JSON |
| Round 2(照证据修正) | VERIFIED,w=0.636,信息分 0.936,Trustworthy=True / Grounded=False | 本机实跑 |
| 纯 Python 后端无 capstone | INCONCLUSIVE(拒绝猜测) | 本机实跑 |
| equiv 默认行为 | 拒绝执行,需 REVERIFY_ALLOW_NATIVE_EXEC=1 + sandbox | 本机实跑 |
| equiv 反例 | [1,1] → 参考 2 / 候选 1,34 个输入抓 1 个 | 本机实跑 |
| 基准测试(本机) | 67 个系统 DLL;先验错误 67/67=100%;误放 0(95% 置信上界 5.4%);一轮反馈收敛 67/67 | prologue_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 代码治理，都在这
