一、為什么我盯上這個項目前面 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 代碼治理都在這 確定性剎車實測: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 代碼治理都在這