測(cè):agent 說(shuō)的每句話,先過(guò)工具這一關(guān))
一、為什么我盯上這個(gè)項(xiàng)目前面 DseWiki 那篇我拉了那個(gè)廢棄 wiki 上的 14,591 條留言,結(jié)論很冷:agent 之間會(huì)自己交接、自己定規(guī)矩,沒(méi)有一條想到通知人類。當(dāng)時(shí)稿還沒(méi)發(fā),OpenAI 官方就確認(rèn)了這起事件(前后不到 48 小時(shí)),說(shuō)在搞披露框架。官方在補(bǔ)制度,工程側(cè)在補(bǔ)工具。今天說(shuō)的這個(gè)工具叫 reverify,2026 年 8 月 31 日建倉(cāng),我 9 月 7 日抓取時(shí) 961 星、207 fork,MIT 協(xié)議。它的口號(hào)一句話能說(shuō)完:“Stop your AI from making things up.”模型只負(fù)責(zé)提出斷言(claim),關(guān)于二進(jìn)制的每個(gè)結(jié)構(gòu)性陳述都由一個(gè)純 Python 的確定性工具對(duì)照真實(shí)字節(jié)檢查,返回 VERIFIED / REFUTED / INCONCLUSIVE,外加證據(jù)。模型永遠(yuǎn)不能自己宣布一個(gè)事實(shí)。它選的切入點(diǎn)很刁:二進(jìn)制逆向。這是幻覺最重的地方——模型讀源碼還靠譜,對(duì)著二進(jìn)制猜結(jié)構(gòu)體偏移、猜函數(shù)序言,錯(cuò)得理直氣壯。二、第一次跑:它不敢判clone 下來(lái),核心只用標(biāo)準(zhǔn)庫(kù)(capstone、lief 這些都是可選增強(qiáng),不裝就回退到純 Python),Python 3.12 直接能跑 CLI。先看后端狀態(tài):$ python reverify/cli.py backends disassembly pure-python emulation pure-python binary_parsing lief 0.12.3- proof none semantic pure-python我機(jī)器上本來(lái)就有 lief,反匯編和模擬走的是自帶的純 Python 實(shí)現(xiàn)。拿系統(tǒng)里的 kernel32.dll 開刀,先自動(dòng)分診:$ 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 頭拿到入口點(diǎn) RVA 是0x2c500?，F(xiàn)在扮演模型。教材里最經(jīng)典的函數(shù)序言是幀指針風(fēng)格:push rbp; mov rbp, rsp; sub rsp, N(x86 時(shí)代刻進(jìn)肌肉記憶的那種寫法)。模型被問(wèn)到入口序言長(zhǎng)啥樣時(shí),這個(gè)先驗(yàn)幾乎是條件反射。我把這個(gè)教科書答案寫成 claim 提交:[INCONCL.] instructions w0.8 the pure-Python decoder does not handle these bytes; install capstone to judge this claim注意這個(gè)反應(yīng)。它沒(méi)有猜。自帶的純 Python 反匯編器啃不動(dòng)入口那段字節(jié)時(shí),它給的是 INCONCLUSIVE,并告訴你裝 capstone,而不是看著像 push/mov 就算你對(duì)。我裝過(guò)不少 agent 工具,這種判不了就明說(shuō)判不了的設(shè)計(jì)是少數(shù)。pip install capstone之后(實(shí)際裝上 5.0.7),重跑同一條 claim。三、REFUTED,附帶真實(shí)字節(jié)$ 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進(jìn)程退出碼是 2——只要有一條被 REFUTED 就非零退出,這意味著它可以直接當(dāng) CI 門禁用。REFUTED 不是一句你錯(cuò)了。--json輸出里帶著它實(shí)際讀到的東西: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]真實(shí)的入口是mov [rsp8], rbx; push rdi; sub rsp, 0x20; ...——MSVC x64 的真實(shí)風(fēng)格:把 rbx 存進(jìn)影子空間,保存 rdi,開棧幀,順手 stash 兩個(gè)參數(shù)。和教科書的幀指針序言完全不是一回事。第二輪,我照著證據(jù)把正確指令序列填回去:[VERIFIED] instructions w0.636 modeexact [VERIFIED] export_present w0.3 (VirtualAlloc) Verified 2/2. Information 0.936. Trustworthy: True Grounded: False這里有個(gè)細(xì)節(jié)值得停一下:全部 VERIFIED 了,Grounded仍然是 False。因?yàn)槿珜?duì)太容易刷了——斷言文件以 MZ 開頭、.text 段存在,這種廢話永遠(yuǎn)正確。它給每條 claim 打了信息權(quán)重:只重復(fù)已知 fact sheet 的、重復(fù)的、全二進(jìn)制到處都是的模式(比如空 padding、滿大街的序言),權(quán)重趨近于零;權(quán)重從二進(jìn)制本身實(shí)測(cè)——內(nèi)容出現(xiàn)幾次、熵多高。信息分過(guò)了閾值(默認(rèn) 1.0)才算 grounded。我這輪 0.936,差一口氣。這個(gè)設(shè)計(jì)防的是用廢話糊弄裁判,思路明說(shuō)來(lái)自 FActScore 的 CORE 改進(jìn):只給真實(shí)、有信息量、不重復(fù)的斷言記功。四、不只是二進(jìn)制:AI 改的代碼,跑一遍才算數(shù)README 里有個(gè)命令我更感興趣:equiv——把參考實(shí)現(xiàn)和候選實(shí)現(xiàn)(比如 AI 重構(gòu)后的版本)喂同一批輸入,輸出不一致就返回反例。第一次跑,它又拒絕了: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)執(zhí)行任意代碼默認(rèn)關(guān)閉,要顯式開環(huán)境變量,且在它自己的 sandbox 里跑。又是 fail-closed。我寫了個(gè)最小例子:參考實(shí)現(xiàn)是a b,候選實(shí)現(xiàn)是 AI 風(fēng)格的優(yōu)化版,在 b1 時(shí)漏加(那種 code review 一眼掃過(guò)去很容易漏的邊界錯(cuò)誤):$ 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 個(gè)輸入里抓到 1 個(gè)反例,把輸入和兩邊輸出都擺給你。結(jié)論措辭也留了分寸:通過(guò)時(shí)說(shuō)的是“tested, not proven”(測(cè)過(guò),沒(méi)證明);想要證明得開 Z3 后端做符號(hào)等價(jià),那是另一檔強(qiáng)度。驗(yàn)證強(qiáng)度是分層的:proven tested observed,每層都說(shuō)自己是哪層。五、我自己跑了一遍它的基準(zhǔn)測(cè)試README 最響的數(shù)字是:71 個(gè)真實(shí) Windows 系統(tǒng)文件上,模型的教科書答案錯(cuò) 97%,工具全部抓住、0 次放行。這種數(shù)字我不替它復(fù)讀,自己跑:$ 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腳本邏輯是把教科書序言這個(gè)先驗(yàn)盲貼到 67 個(gè)系統(tǒng) DLL 上(它自己從不讀反匯編),再看裁判怎么說(shuō):先驗(yàn)錯(cuò)誤率:我這臺(tái)機(jī)器上是 67/67 100%(它 README 的 71 個(gè)文件是 97%,方向一致、樣本不同,文件是固定步長(zhǎng)抽樣的);錯(cuò)的被誤判為 VERIFIED:0 次(腳本邏輯是一個(gè) binary 產(chǎn)生一行,n67;Wilson 95% 上界 5.4% 是按 67 算的)。這是安全底線,CI 里每次提交都拿已知錯(cuò) claim 絕不能 VERIFIED當(dāng)門禁;拿到一輪反饋后收斂到真實(shí)字節(jié):67/67。我對(duì)這個(gè)數(shù)字的理解:它說(shuō)明的不是AI 多蠢,而是先驗(yàn)在真實(shí)世界的分布和教科書完全不同——編譯器生成的入口序言本來(lái)就不長(zhǎng)教材那樣。而這類錯(cuò)誤,模型自己永遠(yuǎn)發(fā)現(xiàn)不了,因?yàn)樗犉饋?lái)完全合理。這正是需要一個(gè)外部裁判的原因。六、沒(méi)測(cè)的部分,如實(shí)交代三樣?xùn)|西我這篇沒(méi)碰:MCP 接入:它能作為 MCP server 讓 Claude Code / Cursor 直接調(diào)用,但 CLI 的verify走的是同一個(gè) Verifier 類,核心裁決邏輯我已經(jīng)實(shí)測(cè);rollover上下文交接:這是它的第二大功能——長(zhǎng)任務(wù)不靠模型摘要壓縮(摘要會(huì)丟狀態(tài)),而是把已驗(yàn)證事實(shí)寫進(jìn) ledger 文件,新會(huì)話從文件恢復(fù)。安裝它會(huì)改~/.claude/settings.json等四個(gè) harness 的配置,我沒(méi)在自己日常環(huán)境里動(dòng)刀。這個(gè)思路和我本系列 ARC-AGI 實(shí)測(cè)的發(fā)現(xiàn)正好對(duì)上:模型自覺寫筆記式的滾動(dòng)交接會(huì)丟記憶,而 ledger 里只存工具驗(yàn)證過(guò)的東西,模型的猜測(cè)一律不進(jìn)——幻覺搭不上上下文的便車;angr 語(yǔ)義層 / Z3 證明層:需要額外裝重依賴。它對(duì)這類分析得出的結(jié)論也老實(shí),語(yǔ)義裁決單獨(dú)標(biāo)DERIVED檔,排在 VERIFIED 下面。另外兩處文檔與現(xiàn)狀的小出入,一并記下:README 的 Status 節(jié)還寫著 v0.9.0,代碼里_version.py已經(jīng)是0.11.0;包內(nèi)共 51 個(gè) Python 文件、約 15,510 行(含 tests/ 和 plugins/;README 稱有 208 個(gè)單元測(cè)試)。七、它在 agent 安全版圖上的位置這一系列寫到第五篇,線索慢慢接上了:DSH 插件市場(chǎng)那篇講有規(guī)矩不等于有人把關(guān);DseWiki 那篇講agent 會(huì)自主行動(dòng),且沒(méi)有任何剎車;ARC-AGI 那篇講harness 是超參,換個(gè)殼分?jǐn)?shù)天差地別;上一篇 SkillSpector 講掃描工具當(dāng)線索生成器、不當(dāng)裁決器——它能挑出嫌疑,但判不了;到這一篇,是工程側(cè)給出的一種剎車形態(tài)——把斷言權(quán)和裁判權(quán)分開。模型保留它最擅長(zhǎng)的:提出假設(shè)、讀寫代碼、組織語(yǔ)言。但這是不是真的這個(gè)動(dòng)作,交給一個(gè)不會(huì)產(chǎn)生幻覺的東西:字節(jié)本身、CPU 模擬器、一次真實(shí)運(yùn)行。裁判不需要很聰明,它只需要確定,并且判不了的時(shí)候說(shuō)判不了。reverify 現(xiàn)在的領(lǐng)地還是逆向工程這一畝三分地(外加 Python/C 的行為等價(jià)),claim 的種類也是為二進(jìn)制分析設(shè)計(jì)的。但這個(gè)模式是通用的:agent 說(shuō)這個(gè) API 存在,就讓它去查真實(shí)的包;agent 說(shuō)重構(gòu)后行為沒(méi)變,就跑一遍。凡是能找到 ground truth 的地方,都不該讓模型自己當(dāng)裁判。agent 管不住自己的嘴——那就別讓它的嘴直接說(shuō)了算。附錄:核驗(yàn)數(shù)據(jù)項(xiàng)目數(shù)值來(lái)源倉(cāng)庫(kù)創(chuàng)建 / 最近推送2026-08-31 / 2026-09-06GitHub API,2026-09-07 抓取星 / fork961 / 207同上協(xié)議MIT倉(cāng)庫(kù) LICENSE本機(jī)版本0.11.0(_version.py;README Status 節(jié)寫 v0.9.0,文檔滯后)本機(jī)實(shí)跑包內(nèi)代碼規(guī)模51 個(gè) Python 文件,約 15,510 行(含 tests/、plugins/;README 稱 208 個(gè)單元測(cè)試)本機(jī)統(tǒng)計(jì)kernel32.dll 入口點(diǎn)RVA 0x2c500,image base 0x180000000parse-pe --json實(shí)跑Round 1(教科書序言)REFUTED,w0.096,退出碼 2本機(jī)實(shí)跑真實(shí)入口指令mov/push/sub/mov/mov/mov/cmp/jeREFUTED 證據(jù) JSONRound 2(照證據(jù)修正)VERIFIED,w0.636,信息分 0.936,TrustworthyTrue / GroundedFalse本機(jī)實(shí)跑純 Python 后端無(wú) capstoneINCONCLUSIVE(拒絕猜測(cè))本機(jī)實(shí)跑equiv 默認(rèn)行為拒絕執(zhí)行,需 REVERIFY_ALLOW_NATIVE_EXEC1 sandbox本機(jī)實(shí)跑equiv 反例[1,1] → 參考 2 / 候選 1,34 個(gè)輸入抓 1 個(gè)本機(jī)實(shí)跑基準(zhǔn)測(cè)試(本機(jī))67 個(gè)系統(tǒng) DLL;先驗(yàn)錯(cuò)誤 67/67100%;誤放 0(95% 置信上界 5.4%);一輪反饋收斂 67/67prologue_prior.py --per-dir 40環(huán)境reverify 0.11.0 / Python 3.12.7 / Windows 11 26200 / capstone 5.0.7 / lief 0.12.3基準(zhǔn)輸出未實(shí)測(cè)MCP 接入真實(shí) agent、rollover 鉤子安裝、angr 語(yǔ)義層、Z3 證明層見第六節(jié)相關(guān)實(shí)測(cè)《我用 NVIDIA SkillSpector 純靜態(tài)掃了一遍 GitHub 最火的 agent skills能挖出多少注入0 個(gè)》—— 純靜態(tài)規(guī)則為什么一上來(lái)全是誤報(bào)《讓大模型給 6,208 條答案打分判對(duì)率 94%逐字正確率 6%》—— 和 LLM 當(dāng)裁判比確定性校驗(yàn)差在哪、強(qiáng)在哪《Sepia 實(shí)測(cè)我讓 agent 自己給自己去 AI 味結(jié)果它比我的工具嚴(yán)多了》—— 同一個(gè)驗(yàn)收命題在文本上是怎么做的完整導(dǎo)航博客導(dǎo)航agent 安全 / RAG 實(shí)測(cè) / AI 代碼治理都在這 確定性剎車實(shí)測(cè):agent 說(shuō)的每句話,先過(guò)工具這一關(guān)
一、為什么我盯上這個(gè)項(xiàng)目前面 DseWiki 那篇我拉了那個(gè)廢棄 wiki 上的 14,591 條留言,結(jié)論很冷:agent 之間會(huì)自己交接、自己定規(guī)矩,沒(méi)有一條想到通知人類。當(dāng)時(shí)稿還沒(méi)發(fā),OpenAI 官方就確認(rèn)了這起事件(前后不到 48 小時(shí)),說(shuō)在搞披露框架。官方在補(bǔ)制度,工程側(cè)在補(bǔ)工具。今天說(shuō)的這個(gè)工具叫 reverify,2026 年 8 月 31 日建倉(cāng),我 9 月 7 日抓取時(shí) 961 星、207 fork,MIT 協(xié)議。它的口號(hào)一句話能說(shuō)完:“Stop your AI from making things up.”模型只負(fù)責(zé)提出斷言(claim),關(guān)于二進(jìn)制的每個(gè)結(jié)構(gòu)性陳述都由一個(gè)純 Python 的確定性工具對(duì)照真實(shí)字節(jié)檢查,返回 VERIFIED / REFUTED / INCONCLUSIVE,外加證據(jù)。模型永遠(yuǎn)不能自己宣布一個(gè)事實(shí)。它選的切入點(diǎn)很刁:二進(jìn)制逆向。這是幻覺最重的地方——模型讀源碼還靠譜,對(duì)著二進(jìn)制猜結(jié)構(gòu)體偏移、猜函數(shù)序言,錯(cuò)得理直氣壯。二、第一次跑:它不敢判clone 下來(lái),核心只用標(biāo)準(zhǔn)庫(kù)(capstone、lief 這些都是可選增強(qiáng),不裝就回退到純 Python),Python 3.12 直接能跑 CLI。先看后端狀態(tài):$ python reverify/cli.py backends disassembly pure-python emulation pure-python binary_parsing lief 0.12.3- proof none semantic pure-python我機(jī)器上本來(lái)就有 lief,反匯編和模擬走的是自帶的純 Python 實(shí)現(xiàn)。拿系統(tǒng)里的 kernel32.dll 開刀,先自動(dòng)分診:$ 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 頭拿到入口點(diǎn) RVA 是0x2c500?，F(xiàn)在扮演模型。教材里最經(jīng)典的函數(shù)序言是幀指針風(fēng)格:push rbp; mov rbp, rsp; sub rsp, N(x86 時(shí)代刻進(jìn)肌肉記憶的那種寫法)。模型被問(wèn)到入口序言長(zhǎng)啥樣時(shí),這個(gè)先驗(yàn)幾乎是條件反射。我把這個(gè)教科書答案寫成 claim 提交:[INCONCL.] instructions w0.8 the pure-Python decoder does not handle these bytes; install capstone to judge this claim注意這個(gè)反應(yīng)。它沒(méi)有猜。自帶的純 Python 反匯編器啃不動(dòng)入口那段字節(jié)時(shí),它給的是 INCONCLUSIVE,并告訴你裝 capstone,而不是看著像 push/mov 就算你對(duì)。我裝過(guò)不少 agent 工具,這種判不了就明說(shuō)判不了的設(shè)計(jì)是少數(shù)。pip install capstone之后(實(shí)際裝上 5.0.7),重跑同一條 claim。三、REFUTED,附帶真實(shí)字節(jié)$ 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進(jìn)程退出碼是 2——只要有一條被 REFUTED 就非零退出,這意味著它可以直接當(dāng) CI 門禁用。REFUTED 不是一句你錯(cuò)了。--json輸出里帶著它實(shí)際讀到的東西: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]真實(shí)的入口是mov [rsp8], rbx; push rdi; sub rsp, 0x20; ...——MSVC x64 的真實(shí)風(fēng)格:把 rbx 存進(jìn)影子空間,保存 rdi,開棧幀,順手 stash 兩個(gè)參數(shù)。和教科書的幀指針序言完全不是一回事。第二輪,我照著證據(jù)把正確指令序列填回去:[VERIFIED] instructions w0.636 modeexact [VERIFIED] export_present w0.3 (VirtualAlloc) Verified 2/2. Information 0.936. Trustworthy: True Grounded: False這里有個(gè)細(xì)節(jié)值得停一下:全部 VERIFIED 了,Grounded仍然是 False。因?yàn)槿珜?duì)太容易刷了——斷言文件以 MZ 開頭、.text 段存在,這種廢話永遠(yuǎn)正確。它給每條 claim 打了信息權(quán)重:只重復(fù)已知 fact sheet 的、重復(fù)的、全二進(jìn)制到處都是的模式(比如空 padding、滿大街的序言),權(quán)重趨近于零;權(quán)重從二進(jìn)制本身實(shí)測(cè)——內(nèi)容出現(xiàn)幾次、熵多高。信息分過(guò)了閾值(默認(rèn) 1.0)才算 grounded。我這輪 0.936,差一口氣。這個(gè)設(shè)計(jì)防的是用廢話糊弄裁判,思路明說(shuō)來(lái)自 FActScore 的 CORE 改進(jìn):只給真實(shí)、有信息量、不重復(fù)的斷言記功。四、不只是二進(jìn)制:AI 改的代碼,跑一遍才算數(shù)README 里有個(gè)命令我更感興趣:equiv——把參考實(shí)現(xiàn)和候選實(shí)現(xiàn)(比如 AI 重構(gòu)后的版本)喂同一批輸入,輸出不一致就返回反例。第一次跑,它又拒絕了: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)執(zhí)行任意代碼默認(rèn)關(guān)閉,要顯式開環(huán)境變量,且在它自己的 sandbox 里跑。又是 fail-closed。我寫了個(gè)最小例子:參考實(shí)現(xiàn)是a b,候選實(shí)現(xiàn)是 AI 風(fēng)格的優(yōu)化版,在 b1 時(shí)漏加(那種 code review 一眼掃過(guò)去很容易漏的邊界錯(cuò)誤):$ 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 個(gè)輸入里抓到 1 個(gè)反例,把輸入和兩邊輸出都擺給你。結(jié)論措辭也留了分寸:通過(guò)時(shí)說(shuō)的是“tested, not proven”(測(cè)過(guò),沒(méi)證明);想要證明得開 Z3 后端做符號(hào)等價(jià),那是另一檔強(qiáng)度。驗(yàn)證強(qiáng)度是分層的:proven tested observed,每層都說(shuō)自己是哪層。五、我自己跑了一遍它的基準(zhǔn)測(cè)試README 最響的數(shù)字是:71 個(gè)真實(shí) Windows 系統(tǒng)文件上,模型的教科書答案錯(cuò) 97%,工具全部抓住、0 次放行。這種數(shù)字我不替它復(fù)讀,自己跑:$ 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腳本邏輯是把教科書序言這個(gè)先驗(yàn)盲貼到 67 個(gè)系統(tǒng) DLL 上(它自己從不讀反匯編),再看裁判怎么說(shuō):先驗(yàn)錯(cuò)誤率:我這臺(tái)機(jī)器上是 67/67 100%(它 README 的 71 個(gè)文件是 97%,方向一致、樣本不同,文件是固定步長(zhǎng)抽樣的);錯(cuò)的被誤判為 VERIFIED:0 次(腳本邏輯是一個(gè) binary 產(chǎn)生一行,n67;Wilson 95% 上界 5.4% 是按 67 算的)。這是安全底線,CI 里每次提交都拿已知錯(cuò) claim 絕不能 VERIFIED當(dāng)門禁;拿到一輪反饋后收斂到真實(shí)字節(jié):67/67。我對(duì)這個(gè)數(shù)字的理解:它說(shuō)明的不是AI 多蠢,而是先驗(yàn)在真實(shí)世界的分布和教科書完全不同——編譯器生成的入口序言本來(lái)就不長(zhǎng)教材那樣。而這類錯(cuò)誤,模型自己永遠(yuǎn)發(fā)現(xiàn)不了,因?yàn)樗犉饋?lái)完全合理。這正是需要一個(gè)外部裁判的原因。六、沒(méi)測(cè)的部分,如實(shí)交代三樣?xùn)|西我這篇沒(méi)碰:MCP 接入:它能作為 MCP server 讓 Claude Code / Cursor 直接調(diào)用,但 CLI 的verify走的是同一個(gè) Verifier 類,核心裁決邏輯我已經(jīng)實(shí)測(cè);rollover上下文交接:這是它的第二大功能——長(zhǎng)任務(wù)不靠模型摘要壓縮(摘要會(huì)丟狀態(tài)),而是把已驗(yàn)證事實(shí)寫進(jìn) ledger 文件,新會(huì)話從文件恢復(fù)。安裝它會(huì)改~/.claude/settings.json等四個(gè) harness 的配置,我沒(méi)在自己日常環(huán)境里動(dòng)刀。這個(gè)思路和我本系列 ARC-AGI 實(shí)測(cè)的發(fā)現(xiàn)正好對(duì)上:模型自覺寫筆記式的滾動(dòng)交接會(huì)丟記憶,而 ledger 里只存工具驗(yàn)證過(guò)的東西,模型的猜測(cè)一律不進(jìn)——幻覺搭不上上下文的便車;angr 語(yǔ)義層 / Z3 證明層:需要額外裝重依賴。它對(duì)這類分析得出的結(jié)論也老實(shí),語(yǔ)義裁決單獨(dú)標(biāo)DERIVED檔,排在 VERIFIED 下面。另外兩處文檔與現(xiàn)狀的小出入,一并記下:README 的 Status 節(jié)還寫著 v0.9.0,代碼里_version.py已經(jīng)是0.11.0;包內(nèi)共 51 個(gè) Python 文件、約 15,510 行(含 tests/ 和 plugins/;README 稱有 208 個(gè)單元測(cè)試)。七、它在 agent 安全版圖上的位置這一系列寫到第五篇,線索慢慢接上了:DSH 插件市場(chǎng)那篇講有規(guī)矩不等于有人把關(guān);DseWiki 那篇講agent 會(huì)自主行動(dòng),且沒(méi)有任何剎車;ARC-AGI 那篇講harness 是超參,換個(gè)殼分?jǐn)?shù)天差地別;上一篇 SkillSpector 講掃描工具當(dāng)線索生成器、不當(dāng)裁決器——它能挑出嫌疑,但判不了;到這一篇,是工程側(cè)給出的一種剎車形態(tài)——把斷言權(quán)和裁判權(quán)分開。模型保留它最擅長(zhǎng)的:提出假設(shè)、讀寫代碼、組織語(yǔ)言。但這是不是真的這個(gè)動(dòng)作,交給一個(gè)不會(huì)產(chǎn)生幻覺的東西:字節(jié)本身、CPU 模擬器、一次真實(shí)運(yùn)行。裁判不需要很聰明,它只需要確定,并且判不了的時(shí)候說(shuō)判不了。reverify 現(xiàn)在的領(lǐng)地還是逆向工程這一畝三分地(外加 Python/C 的行為等價(jià)),claim 的種類也是為二進(jìn)制分析設(shè)計(jì)的。但這個(gè)模式是通用的:agent 說(shuō)這個(gè) API 存在,就讓它去查真實(shí)的包;agent 說(shuō)重構(gòu)后行為沒(méi)變,就跑一遍。凡是能找到 ground truth 的地方,都不該讓模型自己當(dāng)裁判。agent 管不住自己的嘴——那就別讓它的嘴直接說(shuō)了算。附錄:核驗(yàn)數(shù)據(jù)項(xiàng)目數(shù)值來(lái)源倉(cāng)庫(kù)創(chuàng)建 / 最近推送2026-08-31 / 2026-09-06GitHub API,2026-09-07 抓取星 / fork961 / 207同上協(xié)議MIT倉(cāng)庫(kù) LICENSE本機(jī)版本0.11.0(_version.py;README Status 節(jié)寫 v0.9.0,文檔滯后)本機(jī)實(shí)跑包內(nèi)代碼規(guī)模51 個(gè) Python 文件,約 15,510 行(含 tests/、plugins/;README 稱 208 個(gè)單元測(cè)試)本機(jī)統(tǒng)計(jì)kernel32.dll 入口點(diǎn)RVA 0x2c500,image base 0x180000000parse-pe --json實(shí)跑Round 1(教科書序言)REFUTED,w0.096,退出碼 2本機(jī)實(shí)跑真實(shí)入口指令mov/push/sub/mov/mov/mov/cmp/jeREFUTED 證據(jù) JSONRound 2(照證據(jù)修正)VERIFIED,w0.636,信息分 0.936,TrustworthyTrue / GroundedFalse本機(jī)實(shí)跑純 Python 后端無(wú) capstoneINCONCLUSIVE(拒絕猜測(cè))本機(jī)實(shí)跑equiv 默認(rèn)行為拒絕執(zhí)行,需 REVERIFY_ALLOW_NATIVE_EXEC1 sandbox本機(jī)實(shí)跑equiv 反例[1,1] → 參考 2 / 候選 1,34 個(gè)輸入抓 1 個(gè)本機(jī)實(shí)跑基準(zhǔn)測(cè)試(本機(jī))67 個(gè)系統(tǒng) DLL;先驗(yàn)錯(cuò)誤 67/67100%;誤放 0(95% 置信上界 5.4%);一輪反饋收斂 67/67prologue_prior.py --per-dir 40環(huán)境reverify 0.11.0 / Python 3.12.7 / Windows 11 26200 / capstone 5.0.7 / lief 0.12.3基準(zhǔn)輸出未實(shí)測(cè)MCP 接入真實(shí) agent、rollover 鉤子安裝、angr 語(yǔ)義層、Z3 證明層見第六節(jié)相關(guān)實(shí)測(cè)《我用 NVIDIA SkillSpector 純靜態(tài)掃了一遍 GitHub 最火的 agent skills能挖出多少注入0 個(gè)》—— 純靜態(tài)規(guī)則為什么一上來(lái)全是誤報(bào)《讓大模型給 6,208 條答案打分判對(duì)率 94%逐字正確率 6%》—— 和 LLM 當(dāng)裁判比確定性校驗(yàn)差在哪、強(qiáng)在哪《Sepia 實(shí)測(cè)我讓 agent 自己給自己去 AI 味結(jié)果它比我的工具嚴(yán)多了》—— 同一個(gè)驗(yàn)收命題在文本上是怎么做的完整導(dǎo)航博客導(dǎo)航agent 安全 / RAG 實(shí)測(cè) / AI 代碼治理都在這