Reverify：让确定性工具替模型的事实断言签字

它要解决的不是「模型答错」，而是「模型答错还像事实」

语言模型读源码尚可，做逆向并不可靠。README 的描述很直接：让模型从二进制里重建一个结构体或算法，它会自信地编出偏移、大小和行为。在二进制分析里这个问题比源码分析严重得多，而「这句是不是模型编的」正是把 AI 用于真实逆向时最大的拦路石。

Reverify 的定位是给这种断言加一道裁决环节。模型提出 claim，确定性工具拿实际字节去核对，返回 VERIFIED、REFUTED 或 INCONCLUSIVE，并附上它实际观察到的字节。README 的原话是模型永远不能自己断言一个事实。目标用户是逆向工程、恶意代码分析、CTF 以及互操作性研究方向的工程师，前提是获得授权，SECURITY.md 对此有单独说明。

它顺手解决了第二个问题：长任务里上下文会漂。做法不是压缩摘要，而是 reverify rollover 把会话交接给一个文件、开一个新的，避免漂移，也不需要 /clear。v0.11.0 的发布说明把这条能力列为跨 Claude Code、Codex、Gemini CLI、OpenCode 的无损上下文交接。

claim 是唯一的接口，verifier 是唯一的裁判

整条回路围绕一个数据结构展开。一个 claim 就是对二进制的某个假设，写成 JSON，交给 reverify verify 裁决。README 给的例子是检查 4096 偏移处的指令助记符是否为 push、mov、sub，note 字段写「function prologue」。返回的是三态之一，外加工具实际观察到的字节。

claim 的种类决定了能问什么问题。字节级有 bytes_at、u16_at、u32_at、u64_at 这类类型化读取，省掉自己算大小端；pattern_present、string_present、import_present、export_present、section_present 面向特征与元数据；instructions 检查助记符和可选的操作数；emulate_result 在模拟器里跑一段代码再比对寄存器期望值，README 的示例用 b805000000b90300000001c8c3 在 x86 上期望 eax 等于 8。语义层还有 function_at、calls、references、reachable_from_entry。

地址空间这件事值得单独说：默认是文件偏移，claim 里写 space 为 rva 或 va 时，verifier 会通过节表换算，并把三种地址都回显出来。这个设计省掉了逆向里最容易出错的一类手工换算，也让 claim 可以被机器生成。

裁决结果可以被程序消费：claims 支持从 JSON 文件批量读取，只要有任何一条被 REFUTED，CLI 就以非零码退出。这意味着一个 agent 或一条 CI 任务可以直接把「重构是否成立」当成门禁，而不是让人去读模型的自述。

纯 Python 是默认档，成熟引擎是可选升级

确定性核心覆盖 PE/ELF/Mach-O 解析、x86/x64/ARM/ARM64 反汇编、AOB 模式扫描、CPU 模拟、Protobuf/TLV 解析、Frida hook 生成。README 强调开箱即纯 Python，不需要 Ghidra 就能装上。

升级路径是 extras。pip install "reverify[full]" 会把工具链就地换成 capstone 负责反汇编、unicorn 负责真实 CPU 模拟、lief 负责 PE/ELF/Mach-O、Z3 负责证明；pip install "reverify[angr]" 再加 angr，用于函数边界、调用图和交叉引用。没装这些依赖时，回退到纯 Python 核心。reverify backends 用来查看当前哪些后端是生效的。

这个分层是务实的，但代价要讲清楚：同一份 claim 在不同机器上可能走不同的判定路径。纯 Python 核心能覆盖字节读取、模式匹配、字符串和节表这类问题，而 emulate_result、prove_equiv 以及语义层的函数边界、调用图，从命名上看依赖 unicorn、Z3、angr。README 只说明「未安装则回退到纯 Python 核心」，没有逐条列出每个 claim kind 在降级后的具体行为。把验证结果写进 CI 门禁之前，先用 reverify backends 确认运行环境里的实际档位，否则你门禁的严格程度会随环境变化。

v0.9.1 的发布说明里有一条 ARM64 路由修复，以及「没有引擎也能保持 soundness」的描述，说明作者在意无引擎环境下的判定正确性。但具体到哪些 claim 会从 VERIFIED 变成 INCONCLUSIVE，材料里没有给出清单。

逆向只是证明场，equiv 把同样的规矩挪到普通源码

二进制逆向是幻觉最严重的地方，所以基准数字从这里出。README 给出的实验设置是：在 71 个真实 Windows 系统文件上，模型的教科书式回答错了 97% 的时间；reverify 全部拦下，没有接受任何一条错误 claim，71 条里 0 条被误判为通过。同一道门禁在每次 push 时跑在 Linux 和 macOS 的 CI 上，另有一次独立的 aarch64 运行得到相同结果。相关材料在 EXAMPLE.md、BENCHMARK.md，复现命令是 python benchmarks/prologue_prior.py。

这里要克制地读：71 个文件、单一任务类型（函数序言先验）、单一模型行为，样本面很窄。它证明的是「这道门禁在特定任务上不会放行错误 claim」，不是「Reverify 在任意逆向任务上都可靠」。v0.10.0 的发布说明提到 evidence at top spec、三平台 CI 门禁基准、混淆矩阵、可复现语料和 receipts，说明作者在往可审计方向补材料，但材料本身没有给出跨任务类型的泛化结论。

另一条路径是 reverify equiv，用法是 reverify equiv <reference> <candidate> --lang python，也支持 C。它把候选实现和参考实现跑在同一批输入上，比对结果是否一致。README 的说法是 AI 的重写或重构应该被测试而不是被信任，被证伪时会连输入和两边输出一起返回。这条路径的意义在于：同一套「工具裁决」的思路并不绑定二进制，只要你能提供参考实现和可执行的输入集，源码级重构也能被证伪。

装起来要跑的命令，以及会被忽略的坑

从 PyPI 安装 CLI 与 MCP server：pip install reverify，或者用 pip install "reverify[full]" 带上 capstone、unicorn、lief。不装任何东西也能从检出目录直接跑，README 强调这是纯标准库路径：python reverify/cli.py auto sample.bin --json，python reverify/cli.py parse-pe sample.exe --json，python reverify/cli.py disasm 90505831C0C3 --arch x86_64。

验证一条 claim 的基本形式是 reverify verify sample.bin --claim，后面跟 JSON。批量时用 --claims-file claims.json。退出码是门禁的关键：只要有任何一条被 REFUTED，进程就以非零码退出。写 CI 的时候要区分 REFUTED 和 INCONCLUSIVE，前者是明确的证伪，后者按 README 的三态定义是证据不足，而退出码规则只对前者做了说明。把 INCONCLUSIVE 当成通过，等于门禁上开了个洞。

作为 agent 工具使用时，它同时是 MCP server 和普通 CLI。README 提到 Claude Code、Cursor 等 agent 可以直接调用这些工具。MCP 的具体配置键、server 名称和启动参数在给定材料里没有展开，需要以仓库中的实际配置为准。

还有一个容易踩的点：claim 里的 offset 默认按文件偏移解释，只有显式写 space 为 rva 或 va 才会走节表换算。模型生成的 claim 如果漏了这个字段，验证会落在错误的地址上，结果可能是 REFUTED，也可能碰巧通过，而后者更危险。

拿它和什么比：单元测试、以及「让模型自查」

最接近的替代品不是另一个反幻觉框架，而是你自己写的断言脚本。区别在于抽象层次：断言脚本里每条检查都是手写的，你知道它在查什么；Reverify 把检查抽象成 claim kind，模型可以生成 claim，工具负责裁决。代价是判定逻辑藏在工具内部，你得到的是三态结果加观察到的字节，而不是自己写的布尔表达式。如果某个检查很关键，自己写断言仍然更可控。

另一类做法是让模型自我复核，或者用第二个模型当裁判。这条路线的根本问题是裁判和被裁判共享同一套先验，模型编出的偏移，另一个模型同样可能编出来，而且不会给出实际字节。Reverify 的差别在于裁判是确定性的：反汇编器、模拟器、节表解析，它们不参与猜测，只报告观察结果。README 里 97% 错误率的那组数字，恰恰说明模型自查在这个任务上不成立。

第三种是直接用 Ghidra 或 IDA 的脚本接口。它们有更强的交互式分析能力，但把结果接进 agent 回路需要自己搭桥。Reverify 的取舍是牺牲交互深度，换取可脚本化的 claim 接口和 MCP 集成。

什么时候它是错的工具

第一类误用是把它当成通用的事实检查器。claim 的种类全部锚定在可观察的产物上：字节、指令、节表、导入导出、模拟结果、两个实现的一致性。如果你的问题是「这段业务逻辑的设计意图是什么」或者「这条架构决策是否合理」，没有可被字节或输入输出证伪的 ground truth，三态判定无从下手。

第二类误用是在未授权的目标上使用。README 明确写了它面向授权的逆向工程，包括恶意代码分析、CTF、互操作性研究，以及你自己拥有或获准分析的软件。这不是免责声明式的客套，工具的定位就是分析二进制，越界使用是使用者的问题。

第三类是把它当作覆盖率的替代品。claim 只覆盖你写出来的那些断言。模型如果压根没提出某个假设，验证回路不会主动去查它。也就是说，它能拦住「说错了」，拦不住「没说」。把 reverify verify 接进流程，不等于对一份逆向报告做了完整审查。

第四类是环境不一致带来的假安全感。同一份 claim 在装了 unicorn 的机器上可能被模拟执行验证，在纯 Python 核心上可能只能走到 INCONCLUSIVE。如果你的团队里有人本地装了 extras、CI 里没装，两边的门禁强度并不相同，而 README 没有给出逐 claim kind 的降级对照表。

维护成本、许可证，以及开工前该确认的三件事

许可证是 MIT，仓库根目录有 LICENSE 文件。MIT 允许商用和修改，义务集中在保留版权与许可声明。这里不给法律意见，涉及分发或与闭源产品集成时，按你所在组织的流程确认。

维护成本主要来自两处。一是可选引擎的版本漂移：capstone、unicorn、lief、Z3、angr 都是独立演进的依赖，reverify[full] 和 reverify[angr] 的实际行为会随它们的版本变化，而纯 Python 回退路径又必须与引擎路径保持判定一致。v0.9.1 那条 ARM64 路由修复说明这类不一致确实出现过。二是 claim 种类的扩张：从 v0.9.1 到 v0.11.0 的发布说明看，语义层和基准材料都在持续变动，claim 的字段语义需要跟着仓库文档走，不能只依赖某一次读到的 README。

升级前建议确认三件事。用 reverify backends 记录当前环境实际生效的后端，把它和 CI 环境对齐。拿一条你已知答案的 claim 走 reverify verify，确认退出码和判定结果符合预期，尤其是 REFUTED 与 INCONCLUSIVE 的分界。最后，如果要用 rollover 做长任务交接，先在 Claude Code、Codex、Gemini CLI 或 OpenCode 中挑一个你实际在用的，验证交接文件的内容是否满足你的审计要求。这三点都无法从 README 直接推出结论，必须在你自己的样本上跑一遍。

编辑结论

如果你的工作流里模型会输出结构体偏移、指令序列或函数边界这类可被字节证伪的断言，Reverify 值得先在一个真实样本上跑一遍：装 pip install reverify，用 reverify backends 确认哪些引擎真正生效，再拿一条你已知答案的 claim 走 reverify verify，看它返回 VERIFIED 还是 REFUTED。反过来，如果你的问题主要是自然语言层面的推理或产品文案，这套工具没有可裁决的 ground truth，装上也只是多一层空转。先验证的是引擎回退行为：在没装 capstone、unicorn、lief、Z3 的环境里，claims 里那些语义 kind 会走到哪一步，README 只说了「回退到纯 Python 核心」，没有逐条说明每个 claim kind 的降级结果，这一点必须自己确认。

官方来源

1. 2akouwu/reverify on GitHub
2. Issues
3. License: MIT
4. README
5. Releases