Reverify：讓確定性工具當裁判，把 AI 對二進位的斷言逐條核對

它要解的是「模型講得像事實」這個問題

語言模型讀原始碼很行，讀二進位不行。README 把病灶寫得很直白：模型會發明一個 API、一個 struct 欄位、一個 offset，或一個函式的作用，並且用陳述句講出來。在二進位分析裡這種幻覺比原始碼嚴重得多，而「這句是不是模型掰的」正是把 AI 用於真實逆向工程時最大的阻礙。

Reverify 的定位不是又一個反編譯器，而是一道閘門。模型的角色被壓縮成「提出假設」，確定性工具才是裁判。一個關於結構或演算法的假設，只有在被拆解、被樣式比對、或在模擬器裡跑過之後，才會被當成結果輸出。README 的說法是模型永遠不能自己斷言一個事實。

目標使用者輪廓清楚：做惡意程式分析、CTF、互通性研究，或分析自己擁有或獲授權軟體的人。README 與 SECURITY.md 都強調這是給授權情境用的逆向工程。如果你的工作不涉及二進位，這個專案的另一半功能（equiv 子命令）才是重點。

驗證迴路：claim 進、證據出

整個設計圍繞一個叫 claim 的物件。claim 是任何關於二進位的假設，欄位包含 kind 與對應參數。以 README 的例子來說，一個 instructions 類的 claim 長這樣：kind 為 instructions、offset 為 4096、mnemonics 為 push、mov、sub，note 寫「function prologue」。工具讀出該 offset 的實際指令，比對助憶符，然後回傳三種結果之一：VERIFIED、REFUTED 或 INCONCLUSIVE，並附上它真正觀察到的位元組。

第三種結果值得注意。INCONCLUSIVE 的存在意味著作者不打算把「工具答不出來」硬塞進二元分類，這比只有通過與否的閘門誠實，但也代表呼叫端必須自己決定 INCONCLUSIVE 要當成阻擋還是放行。

claim 可以從 JSON 檔批次送入（--claims-file claims.json）。CLI 的退出碼設計是關鍵：只要有任何一項被 REFUTED，退出碼就非零，所以 agent 或 CI job 可以直接拿它當 gate。這讓「有依據的重建」變成可自動化的條件，而不是人工看報告。

offset 的語意有明確定義：預設是檔案偏移，除非 claim 裡寫了 "space": "rva" 或 "va"，此時驗證器會透過 section table 換算，並在輸出裡把三種位址都回報出來。這種顯式宣告減少了「這個數字到底是哪一種位址」的誤解，而誤解位址正是逆向工程裡最常見的低級錯誤之一。

claim 種類與語意層的分界

README 列出的 claim 種類可以分成幾層。最底層是原始位元組與型別讀取：bytes_at、u16_at、u32_at、u64_at。後三者被描述為 typed reads，不需要自己做 endianness 換算，這省掉一類很容易寫錯的手工計算。

往上一層是樣式與字串：pattern_present、string_present，以及結構層級的 import_present、export_present、section_present。這些檢查的對象是解析後的結構，而不是原始位元組流。

再往上是反組譯與執行：instructions 可比對助憶符，並可選地比對運算元；emulate_result 則把一段機器碼放進模擬器執行，然後檢查暫存器。README 給的例子是 x86 的 b805000000b90300000001c8c3，期望 eax 等於 8，也就是 5 加 3。

最上層是語意類：function_at、calls、references、reachable_from_entry，README 稱之為語意層（functions, calls and cross-references），並指向專門的章節。這一層的可行性取決於後端：angr 提供函式邊界、呼叫圖與交叉引用。換句話說，語意 claim 的準確度不是常數，它隨你裝了什麼而變。

另有兩個跨到原始碼領域的種類：behavior_equiv 與 prove_equiv。前者對應 reverify equiv 的測試比對，後者對應 Z3 的形式化證明。兩者的保證強度不同，README 沒有把等價性測試說成證明，這個區分是對的。

後端是選配，降級路徑要自己確認

Reverify 的核心是純 Python 的 RE 工具箱：PE、ELF、Mach-O 解析，x86、x64、ARM、ARM64 反組譯，AOB 樣式掃描，CPU 模擬，Protobuf 與 TLV 拆解，Frida hook 生成。README 強調開箱即用、不需要 Ghidra。

成熟引擎是選配。pip install "reverify[full]" 會把工具箱就地升級到 capstone（反組譯）、unicorn（真正的 CPU 模擬）、lief（PE/ELF/Mach-O）與 Z3（證明）；pip install "reverify[angr]" 再加上 angr，用於函式邊界、呼叫圖與交叉引用。

這裡有個必須講清楚的設計後果：沒安裝時會退回純 Python 核心。這聽起來像是優雅的容錯，實際上是行為分歧。同一份 claim 在裝了 unicorn 與沒裝 unicorn 的環境下，emulate_result 的結果可能不同；語意層的 function_at、calls、references、reachable_from_entry 在沒有 angr 時的判斷依據也不一樣。v0.9.1 的發布說明提到「soundness without the engines」，顯示作者確實在意無引擎情境下的可靠性，但這不等於兩種環境等價。

reverify backends 這個子命令就是為了這件事存在：它顯示目前哪些後端是活的。把它寫進 CI 的第一步，比在事後追查為什麼兩台機器結論不同便宜得多。

rollover：用檔案交接取代有損摘要

第二個功能跟二進位無關，處理的是上下文腐化。README 的說法是：不用有損的自動摘要，reverify rollover 把 session 交接給一個檔案，然後開一個新的，所以長任務不會漂移，也不需要 /clear。v0.11.0 的發布說明把範圍寫成跨 Claude Code、Codex、Gemini CLI 與 OpenCode 的無損上下文交接。

這個做法的取捨很明確。摘要式壓縮會丟掉細節，而且丟掉什麼由模型決定，不可控；檔案交接則把「什麼被保留」變成一個你看得到、可以檢查的檔案。代價是你多了一個要管理的檔案，而且交接的正確性取決於寫入的內容是否完整，README 沒有描述交接檔的格式或大小上限，這點在長 session 下值得自己實測。

把這兩個功能放在同一個工具裡，乍看像是兩件事硬湊。但對做逆向工程的 agent 來說，兩者其實是同一個需求的兩面：分析過程會產生大量被核對過的結論，這些結論必須活過上下文重置，否則每次 /clear 之後模型又開始重新猜 offset。

基準數字該怎麼讀

README 引用的數字是：在 71 個真實 Windows 系統檔上，AI 的教科書式答案有 97% 是錯的；reverify 全部抓到，並且從未接受錯誤的 claim（71 個裡 0 個）。同樣的閘門在每次 push 時於 Linux 與 macOS 的 CI 上執行，另有一次獨立的 aarch64 執行得到相同結果。相關材料指向 EXAMPLE.md、BENCHMARK.md，以及 python benchmarks/prologue_prior.py。

這個數字需要正確理解。它衡量的是「模型在沒有工具時錯得多離譜」，以及「閘門有沒有攔下來」，不是「reverify 的分析能力有多強」。97% 這個比例之所以高，是因為題目挑在幻覺最嚴重的地方：二進位逆向工程中的函式序言。v0.10.0 的發布說明提到 CI 閘門的基準、混淆矩陣、可重現語料與 receipts，這些是讓數字可被追溯的機制，方向正確。

但這裡有一個真實的限制：基準只證明閘門不會放行錯誤 claim，不證明閘門能回答你的問題。如果工具對某個 claim 回傳 INCONCLUSIVE，你不會得到答案，只會得到「無法判定」。把 no false accept 當成主要賣點是誠實的，但讀者不該把它誤讀成準確率。

什麼時候不該用它

最明顯的不適用情境是：你需要的是一個互動式、有 GUI 的反編譯器。Reverify 是 CLI 加 MCP server，它的產出是 claim 的判定與證據，不是給你逐行瀏覽、改名、加註解的工作區。想用滑鼠追 call graph 的人會覺得它綁手綁腳。

第二種情境是你只做原始碼、完全不碰二進位。這種情況下你只會用到 equiv 與 prove_equiv 那一小塊，卻要承擔整個 RE 工具箱的安裝與後端管理成本。reverify equiv <reference> <candidate> --lang python 或 C 的用途是把候選實作與參考實作餵同一組輸入、檢查結果一致，refutation 會附上輸入與兩邊輸出。這是個有用的測試骨架，但它不比既有的 property-based testing 框架更通用，只是換了個呼叫介面。

第三種情境是環境受限、裝不了 capstone、unicorn、lief、Z3 或 angr。純 Python 核心仍然可用，但語意層與模擬類 claim 的判斷力會下降，而你必須自己記住這件事。這不是缺陷，是選配架構的必然結果，只是它把複雜度轉嫁給了使用者。

還有一個要自己判斷的點：README 對授權的界線只說適用於授權的逆向工程，並指向 SECURITY.md。工具本身不會替你判斷某個樣本能不能分析，這個責任完全在使用者身上。

與 angr 的關係，以及維護成本

把 angr 當成替代品來比較是不準確的，因為 reverify 在裝了 reverify[angr] 之後會直接使用 angr。真正的差別在於方法論：angr 是符號執行與程式分析的框架，你自己寫腳本、自己解讀輸出，正確性由你的腳本負責；reverify 則是在分析框架外面再套一層裁決層，把模型的斷言轉成可判定的 claim，由工具回答 VERIFIED、REFUTED 或 INCONCLUSIVE。前者給你能力，後者給你否決權。

如果你的流程裡沒有人會對模型輸出提出懷疑，angr 加自己的腳本可能更直接；如果你的流程裡模型會直接寫出結論給人看，reverify 這一層才有意義。兩者不互斥。

維護成本方面，可從材料推得的有幾項。授權是 MIT，對商業使用與再散布相對寬鬆，但這是條款層面的描述，具體情境仍應自行確認，本文不構成法律意見。版本節奏偏快：v0.9.1、v0.10.0、v0.11.0 三個版本集中在 2026 年 9 月 4 日到 9 月 7 日之間，v0.9.1 還是修 ARM64 routing 的 patch（#5）。這種密度代表功能還在快速變動，鎖定版本並在升級時重跑你自己的 claim 集合，比跟著 main 走穩妥。

升級時真正要驗的是後端組合有沒有改變。capstone、unicorn、lief、Z3、angr 任一項的版本變動，都可能讓同一份 claim 的判定結果不同。把 reverify backends 的輸出與你的 claim 集合一起存進 CI 產物，是這個專案本身提供的、具體可行的做法。

編輯結論

Reverify 適合已經在用 Claude Code、Codex、Gemini CLI 或 OpenCode 做二進位分析、且願意把「模型說的」降級成「待核對的假設」的團隊；不適合只想拿一個現成反編譯器、或需要 GUI 互動式逆向的人。導入前先跑 reverify backends 確認 capstone、unicorn、lief、Z3 是否真的載入，因為沒裝就會退回純 Python 核心，disasm 與 emulate 類 claim 的行為會跟著變；再拿一份你手上的樣本跑 reverify auto --json，確認它對你的檔案格式給出的輸出符合預期。

官方來源

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