Lean 的 kernel 收下了一個 False、Anthropic 的密碼分析被卡在「誰能驗」這一關、讓模型檢查自己的十八組比較沒有一組是正的——這週一篇接一篇撞上同一件事：那個負責說「這是對的」的環節，往往是整條鏈上最沒被人回頭檢查過的一環。
第 32 週 —— 誰來檢查檢查的人
這週的主軸
七月二十八日到八月三日，實際出刊的是七月三十日到八月二日這四天，四篇 roundup、十二篇 deep story。主線不在哪個新東西發布，而在一個位置：鏈條最末端那個負責蓋章的環節。證明器的 kernel、密碼分析的驗證者、模型自己的反省步驟、on-call 的根因判斷、甚至一個平均數——這週有半數的篇幅在追同一個問題，那個說「這是對的」的東西，憑什麼？
最乾淨的一例是 一個 phantom 參數，讓 kernel 收下 False。Lean 的 kernel 是整套系統裡唯一被信任的那塊——所有 tactic、所有 elaborator 產出的東西，最後都要過它這一關。七月二十五日 Ramana Kumar 發表一份 AI 協助產出的 Collatz 猜想「反證」，三天後 Kiran Gopinathan 把它縮成一個 False 的最小證明。根因在 kernel 消去 nested occurrence 的時候：外層 inductive 型別的參數若是 phantom，也就是不出現在任何建構子欄位裡，它們在產生的輔助型別上會整組消失，於是躲過型別檢查。de Moura 的定調很克制——「This is an implementation bug, not a hole in Lean's meta-theory.」——修補在回報後一小時內以 PR #14577 推出。一小時修好的其實是最不重要的部分，重點是這個把關者本身也需要有人把關。
同一個位置，換到密碼學這頭。Matthew Green 拆 Anthropic 的密碼分析成果逐一評估了兩個結果：對後量子簽章 HAWK 的金鑰復原，以及對 7 回合 AES 的改良攻擊。他判前者才真有份量——把安全強度大約砍半、在弱化的挑戰實例上幾個小時就跑完——但同時強調它「並沒有發明全新的數學」，只是把既有工具用到徹底；後者只是 2013 年舊工作的常數倍改良，還停在紙上分析。他真正的重點不在誰對誰錯，而在瓶頸已經搬家了：模型很會生出「看起來像真的」卻誤導人的結果，於是產出便宜、驗證變貴。
AI 這一側把同一件事量得更難看。八月一日的 roundup 收了一篇把七種 inference-time 方法放回同樣 token 預算下重測的研究：三種開源模型、兩個數學 benchmark、每組 150 題，連 critique、reflection 與 debate 消耗的 token 都算進成本。三十六組配對比較裡沒有任何一種方法可靠地贏過單純重複取樣，十種可靠地更差，而全部十八組「讓模型檢查自己輸出」的比較都是負的。最刺眼的一筆是 Reflexion 在最小的模型上從未觸發過自己的重試——它每次都判定自己答對，安靜地退化成一條 chain of thought。隔天再補一刀：Northeastern 與 UC Berkeley 對開源 LRM 的研究量到，這些模型 30% 到 60% 的「思考步驟」對最終答案只有 minimal causal impact，NYU 的 William Merrill 說得更直白——「There's no guarantee the chain of thought has to be meaningful in any sense」。同一天的 ORCA-bench 則把場景換成 on-call：1,079 個帶 OpenTelemetry 的根因分析任務，五個 frontier agent 裡最好的在 Medium 難度只有 25.3%，Hard 剩 10.0%，最弱的那個在 40% 的事件報告裡編出一個站不住腳的根因。模型看得見自己的推理軌跡，那條軌跡卻不是它實際算過什麼的忠實紀錄。
把這條線推到底的，是兩篇根本不談 AI 可靠性的文章。七月三十日那篇壓評測察覺向量的論文，向量確實壓得下去（z 約 -7），但作者自己準備的對照組戳破了它：一個隨機的 placebo 方向一樣被壓得動、行為位移一樣大——真正做出判決的不是結果，是那個對照組。同一天的「別再用平均數看延遲」則示範得更赤裸：一次 rollout 後平均延遲上升 9%，看起來像退步，中位數其實改善了 46%，而 p99 幾乎變成三倍。同一份資料，換一個統計量就換一個結論。這週反覆在講的就是這件事：真正決定「對不對」的，往往不是被檢查的東西，而是那把用來檢查的尺。
沒被合稱的個別亮點
181 個節點，一把可重複使用的 auth key是這週最值得整個團隊傳閱的一篇。Tailscale 出面檢討 Hugging Face 那起入侵，開頭先把自己撇清得很明確——沒有任何 Tailscale 漏洞被找到或被利用——攻擊者拿的是 production secret store 裡 136 把金鑰之一，一把用來開 CI 節點、可重複使用的 auth key，接著花好幾天把總共 181 個節點加進對方的 tailnet，事後復原出 17,600 個動作、橫跨四天半。他們自己的結論寫得毫不客氣：「In a world of rogue AI agents, the big credential vault is the prize. It's not okay anymore.」
Kafka 的 payload，在 broker 上是密文是這週工程折衷寫得最誠實的一篇。LINE 把端到端加密推到 Kafka 這一層，用 DEK 與 KEK 兩層信封：AES-GCM 的對稱 DEK 加內容，secp521r1 曲線的 ECIES 只加那把短短的 DEK，理由用他們自己的話是「Encrypting large payloads with asymmetric keys alone is very expensive」。代價一併攤開——多個 consumer 共用一把 KEK 免得 header 隨 consumer 數膨脹、record-level 而非 batch-level 加密犧牲壓縮效率換到與標準擴充點相容——而實測在每秒 5,000 筆、數十 KB 訊息的尖峰下，每個 instance 的 CPU 增幅低於 1%。
Postgres 佇列的三個瓶頸是這週最能直接搬回自己專案的一篇。DBOS 把 Postgres-backed 的 workflow 佇列從每秒約 100 個推到三萬以上，靠的是三個 SQL 層的調整：FOR UPDATE SKIP LOCKED 讓 worker 不搶同一列、只有需要全域流量控制的佇列才用 REPEATABLE READ、以及只索引 ENQUEUED 狀態的部分索引。第二項是實務上最容易漏掉的一環，他們的說法是「在規模下，worker 花在重試交易的時間比處理 workflow 還多」。
把 break 拿掉，case-fold 才跑得動是這週最反直覺的一筆。GitHub 要對 180M 個 repo、480TB 原始碼做 Unicode case folding，而把吞吐從 3.1 GiB/s 推到 45 GiB/s 以上的關鍵是刪掉一個最佳化——那個遇到第一個非 ASCII byte 就 break 的提前退出，讓 LLVM 無法向量化整個迴圈。拿掉 break 先到 7.6 GiB/s，再把判斷、寫回、退出全改成無分支位元運算才吃滿記憶體頻寬。順手把 1,484 組 fold 從約 11.6 KB 壓到 1,776 bytes。
預設設定的代價：Active Storage 的 RCE則是這週最該立刻動手的一篇。CVE-2026-66066：Active Storage 在使用 vips 影像處理器的預設設定下，存在一條從任意檔案讀取通到遠端程式碼執行的鏈。受影響的是 Rails 7.0.0 到 7.2.3.1、8.0.0 到 8.0.5、8.1.0 到 8.1.3 的預設設定，修補版本是 7.2.3.2、8.0.5.1、8.1.3.1——但升級 gem 並不夠，「修補取決於 libvips 本身是 8.13 或更新的版本」，系統套件那一半漏掉就等於沒補。
本週動向
把這週（07/28–08/03）跟上週（07/21–07/27）放在一起量，第一個結論是幾乎沒動：總量兩週都是 52 則，五個 domain 沒有任何一個碰得到 10 pp 的敘事門檻。唯一稱得上位移的是 web，從 17.3% 掉到 11.5%（−5.8 pp）；infra 與 backend 各接走 +2.9 pp（19.2% → 22.1%、17.3% → 20.2%），ai 與 systems 幾乎原地不動（−1.0 pp、+0.9 pp）。web 的收縮在 deep story 那頭更明顯：這週十二篇 deep story 裡 web 是零，而上一次做 rollup 的那一週它還拿了三篇。
tag 這層的變化比 domain 誠實一點。rust 從上週的 1 次升到 3 次，是唯一一個構成 surge 的 tag，撐起它的是 rustc 的效能帳本、GitHub 的無分支 case-fold 與 gccrs 往編譯 kernel 又近一段這三條線；ai-agents 與 rails 各以 3 次新進榜，前者靠 ORCA-bench、Saul 那間假公司與 Copilot 蠕蟲撐著，後者則是 Active Storage 的 RCE 加上 Solid Queue 換 fiber。反方向最值得記的是 formal-verification 從 5 次退到 2 次——它退得最多，卻剛好貢獻了這週最尖銳的那篇 Lean kernel。tag 的次數量的是話題熱度，不是重量。
一週的形狀
四個出刊日、十二篇 deep story，archetype 這頭比上一次收斂：technical-deep-dive 5 篇領頭（KernelScript、Zig 增量編譯、Postgres 佇列、GitHub case-fold、LINE 的 Kafka E2EE），explainer 3 篇（Matthew Green 那篇、C++ 浮點轉整數的 UB、TPU 的 Roofline），narrative 2 篇（Tailscale 的 auth key、Lean 的 kernel），investigation 與 freeform 各 1 篇。五種 archetype 仍然全數到齊，但重心明顯壓在「把機制拆開講清楚」這一側，講故事的篇幅收窄了。
domain 上 systems 以 4 篇最厚（Zig、C++ UB、rustc、Lean），ai 與 infra 各 3 篇，backend 2 篇，web 掛零——這一格的空白就是前面那 −5.8 pp 在 deep story 層的樣子。web 這週不是沒東西：Servo 六月合進 558 個 commit、Chrome 開了 email 驗證的 origin trial、瀏覽器裡手寫 WebGPU kernel 解撲克，都在 roundup 裡。只是沒有一則長到值得單開一篇。這是這週形狀上唯一明顯缺的一角。
12 篇 deep story × 4 天（07/30、07/31、08/01、08/02）
下一週可能會展開的線索
最值得盯的是 Lean 那條線的後半。issue #14576 一小時就修好，但真正的問題是 kernel 這種「唯一被信任的那塊」該怎麼被獨立驗。外部的 nanoda 這類第三方 checker 是現成的答案之一，而這個 bug 恰好是 nested inductive 消去這種只有極少數人讀過的路徑。下週值得看的不是修補本身，是社群會不會開始要求「每個證明都要過兩套獨立 kernel」——這是把把關這件事本身冗餘化的唯一辦法。
另一條是 Rust 在編譯器這頭的三線並進。rust 是這週唯一的 surge（1 → 3），底下並行的是三條線：rustc 自己的效能帳本、GitHub 的無分支 case-fold，以及 gccrs 往編譯 Linux 又近一段。gccrs 那篇對現況說得很保守——「目前編譯器只能處理簡單的獨立程式，但這個情況可能在未來幾個月內迅速改變」——同時 GCC 才剛劃下 15 行的 LLM 貢獻紅線。一個正在衝刺、需要大量貢獻的子專案，撞上一條新的貢獻限制，接下來幾週會不會出現第一起「貢獻被這條規則擋下」的公開案例，是這條線最實際的觀察點。
這週的落點——把關這件事，本身沒有人把關。Lean 的 kernel 是整套系統的最後一道，它自己漏掉了一組 phantom 參數；Anthropic 的密碼分析生得出來，卡的是誰能驗；讓模型檢查自己，十八組比較全是負的；而一個 rollout 的好壞，取決於你看的是平均數還是中位數。四天、十二篇，反覆講的不是「AI 不可靠」這種空話，而是一件更具體的事：當產出變得便宜，唯一還貴的就是驗證，於是驗證那一環會是最先被省掉、也最不該被省掉的地方。