随着 AI 编程 Agent 被广泛使用，「代码看起来对」与「代码真的对」之间的鸿沟成为软件安全的新风险。reverify 的理念很直接：Stop your AI from making things up——it proposes, deterministic tools decide，每一个声称都由确定性工具对照事实核查并给出证据。

一、核心思路：让工具做裁判

reverify 把一个语言模型与一套确定性的纯 Python 逆向工程工具包配对，让工具包充当裁判。模型提出假设，工具负责验证。一条关于结构或算法的假设，只有在对照实际字节（反汇编、模式匹配或在模拟器中执行）检验之后才会被报告，因此输出扎根于二进制本身，而非模型的想象。

其确定性内核涵盖 PE/ELF/Mach-O 解析、x86/x64/ARM/ARM64 反汇编、AOB 模式扫描、CPU 模拟、Protobuf/TLV 解析、Frida hook 生成；纯 Python 开箱即用、无 Ghidra 依赖。安装完整后端（pip install "reverify[full]"）后可升级为 capstone（反汇编）、unicorn（真实 CPU 模拟）、lief（PE/ELF/Mach-O）与 Z3（证明）；安装 angr 后端还能获得函数边界、调用图与交叉引用。

二、不只是二进制

reverify equiv --lang python（或 C）会用一个候选实现和一份参考实现在共享输入上运行并检查二者是否一致，让 AI 的重写或重构被测试而非被信任——若不符，会连同触发输入和两份输出一并反驳回来。普通源代码同样适用这套严谨逻辑。

三、Agent 原生与安全边界

reverify 以 MCP server 形式交付，Claude Code、Cursor 等 Agent 可直接调用，同时也提供普通 CLI。验证循环正是其命名的由来：一个 claim 由确定性工具裁判，返回 VERIFIED、REFUTED 或 INCONCLUSIVE 及实际观察到的字节；CLI 在遇到被反驳的 claim 时非零退出，让 Agent 或 CI 任务可以据此把关重构的正确性。它面向授权逆向工程——恶意软件分析、CTF、互操作性研究以及你拥有或获准分析的程序。

对安全关键领域（嵌入式、自动驾驶、密码学、智能合约），这类工具尤其有价值——它们把「信任 AI」升级为「验证 AI」。reverify 的开源，标志着软件安全正从「人工 review」走向「人机协同的可证明正确」。