三千個人的冷門領域突然紅了：Byron Cook 在 SED 拆解 Formal Methods 怎麼變成 AI Agent 的防火牆

TL;DR

• Byron Cook 十多年前進 AWS 成立 Automated Reasoning Group，IAM Access Analyzer、VPC Reachability Analyzer、Bedrock Guardrails 全部是這個團隊的產出
• Formal methods（形式方法）過去三十年是學術界的小圈圈，全世界專做這行的只有兩三千人。Agentic AI 把這個冷門領域直接推上主流
• 真正的痛點不是 LLM 不夠聰明，是「人類來不及驗證」。當你背後有一千個 agent 在寫 code，你根本不可能逐行 review，工程師會 cognitive overload
• 解法是 neurosymbolic：LLM 負責翻譯自然語言到邏輯式、driving theorem prover，formal tool 負責給 yes / no 答案。原本五個人能做的事，現在生產力翻一千倍
• Lean theorem prover 因為 DeepSeek 拿它合成訓練資料而變成事實標準。AWS 也開源了 Strata，把 Python、Rust 翻譯到 Lean 的中介表示法

Software Engineering Daily 是工程師圈追蹤產業趨勢的老牌節目，這集在 2026 年 5 月 19 日上線，主持人是 Sean Falconer。來賓 Byron Cook 三個頭銜疊起來很猛：AWS 的 VP and Distinguished Scientist、倫敦大學學院（UCL）的電腦科學系教授、DARPA 的 program manager。他在十多年前進 Amazon 成立 Automated Reasoning Group，這個團隊的代表作包括 IAM Access Analyzer（IAM 政策分析器）、VPC Reachability Analyzer（虛擬網路可達性分析器）、Bedrock Guardrails（Bedrock 的 AI 護欄），都是 AWS 的核心安全產品。他更早之前還做了一件被當時學術界認為不可能的事：用一個叫 Terminator 的工具自動證明 Windows device driver 的 termination（程式終止性），正面挑戰了圖靈在 halting problem 上的判斷。

把「不可能」拆成「九成五可能」

先講一個概念。圖靈跟哥德爾的理論明確告訴你 halting problem（停機問題）是 undecidable 的，意思是你不可能寫出一個工具，可以拿任何程式進去都給出正確答案。這是個鐵律。

Byron 的反向操作很有意思。他說：那我就放寬條件。允許這個工具偶爾「我不知道」，只要「不知道」的比例夠低，使用者還是覺得這工具有用。他用一個很生活化的比喻：開車本來就是不安全的，但每天還是有幾億人開車，因為你只要平安到目的地，事後回頭看就是「安全到了」。

他在 Windows kernel team 做這件事的契機更妙。他每天跟一個 driver 開發者 carpool，這個同事一直用 eventually 這個字，「如果發生 X，eventually 應該會 Y」。Byron 突然意識到，eventually 就是 termination 問題。他挑 device driver 當第一個戰場有兩個原因：第一，2000 年代初期，作業系統八成五的 crash 來自 driver；第二，driver 不大，八萬行左右、大概六十個 loop，資料結構幾乎都是循環的雙向鏈表。換句話說，這是個 undecidable 問題的好版本，是可以收斂的版本。

這個思路套到後來幾乎所有形式方法的工程落地：不要硬解通解，找到一個你的領域知識可以幫你跳過 undecidability 的 niche。

Moonshot Ladder：別一次秀大藍圖

進 AWS 那段他講了一個很實在的建議。他之前在學術界都在搞 moonshot，但 Amazon 文化是「show me，看到才信」。所以他學到的是要找 moonshot ladder（登月梯）：你心裡有一個五年後的大藍圖，但對外不要講；每一季交付一個獨立來看就有價值的小東西，建立信任，然後一階一階爬。

他剛進 AWS 那兩三年同時抓四五個專案：IAM 政策的語意推理、virtual network 可達性、低階加密跟 virtualization、distributed protocol。結果四個全部成功，他自己變成 bottleneck，整整忙了兩三年才把溝通跟交接搞順。

這段對創業者跟資深工程師都很受用。我自己創業以來的體感很像：你越想一次解大問題，越容易卡住；先把藍圖切成可獨立交付的小塊，每一塊都能跑、能 demo、能讓人覺得「啊這個有意義」，後續才有長大的空間。

Agent 不怕坐牢，所以規則得提前寫死

整集最有衝擊力的轉折在這。

Byron 提出一個概念：人類社會原本有 sociotechnical mechanism（社會技術機制）幫忙過濾掉壞行為。警察是 sociotechnical 的，因為「我不想坐牢」會自動限制我做某些事；公司的法務、合規流程也是 sociotechnical，因為人會怕被罰。

但 agent 不怕坐牢。You can't send the AI to jail。

這句話聽起來像哲學討論，實際是工程問題。當你的工程師一個人背後跑一千個 agent 在寫 code，所有責任在法律上會落在那個工程師身上，但工程師根本看不完輸出，cognitive overload 是必然的。前幾天我才寫過 OpenAI 工程師 Ryan Lopopolo 五個月沒寫一行 code，靠 agent 產出百萬行 production 程式碼的紀錄，那篇講的是怎麼用 harness engineering 讓 agent 自己 review agent。Byron 在這集講的是另一條互補的路：你得在 agent 動手之前，先把規則用數學寫死。

具體要寫什麼？availability（可用性）、confidentiality（機密性）、integrity（完整性）、durability（持久性）、sovereignty（資料主權）。這些原本你寫在 wiki 上的政策，現在得翻譯成 linear temporal logic（線性時序邏輯）或 CTL（計算樹邏輯）這種形式語言。然後在 agent 要執行任何指令之前，先靜態檢查這個動作會不會違反這些不變式。

這跟 Christian Catalini 提出的「verification is the new scarcity」論點幾乎是同一套。當 AI 把「生產智力」變便宜，稀缺性自動轉到「驗證」這一端。

Neurosymbolic：LLM 加 Lean 把生產力翻一千倍

Byron 在 AWS 內部觀察到的數字蠻誇張。

過去能 drive 一個 theorem prover（定理證明器）的工程師全世界大概只有幾百個。他十多年前進 AWS 招了四五個朋友進來，這幾個人就是「neuro」，讀過所有 proof、會手動 driving 工具。

現在用 LLM 配 theorem prover 之後，這幾個人手上同時跑幾千個 agentic 證明任務。Byron 的原話：「這不只是十倍、百倍，是一千倍的生產力提升。」

為什麼這套組合特別 work？因為 Lean 這類 theorem prover 是 yes / no 工具。你給它一個複雜命題，它回你「對」或「不對」。這種 binary feedback 對 LLM 來說太完美了，可以無限迭代、自動 verify、無人類介入。對比寫詩或翻譯，「這首詩好不好」沒有客觀答案，scaling 就卡住了。

這也解釋了為什麼這波 AI 浪潮裡，coding agent 跑得比其他應用快很多：compile pass 跟 unit test 就是天然的 verifier。形式方法給的是更強版本的同一件事。

Bedrock Guardrails 跟 Strata 開源

AWS 把這套東西包成產品叫 Automated Reasoning Checks，掛在 Bedrock Guardrails 底下。你把公司的休假政策、家庭醫療請假法（family medical leave act）、稅務規則翻譯成邏輯式，inference 時這個工具會把 LLM 的回答跟邏輯式對照，移除矛盾的部分，還能告訴你為什麼。

附帶的好處很有意思：客戶在用的時候，常常會反向發現自己原本的政策本身就互相矛盾。等於你用 LLM 當前端、formal tool 當後端，順便幫公司 debug 了治理規則。

入門路徑 Byron 給得很具體。AWS 開源了 Strata，這是一個 intermediate representation（中介表示法），可以把 Python、Java、Rust 翻譯成 Lean 看得懂的邏輯式。Lean 是這幾年突然紅起來的 theorem prover，因為 DeepSeek 等模型發現用 Lean 合成訓練資料能讓模型在 reasoning 上跳一個檔次，整個圈子的 lingua franca 就鎖定在 Lean 上了。

結語：兩種語言都會講的人現在 worth their weight in gold

這集對我最大的啟發是這個產業的鐘擺。

Byron 提到一件事：1940、50 年代電腦發明的時候，von Neumann、圖靈那群人本來就是邏輯學家，formal methods 跟程式設計是同一件事。後來 IT 商業化、AI winter 來來回回幾次，邏輯學派跟工程實作派分家。歐洲有些 formal reasoning 專家一輩子沒寫過程式，美國一堆寫程式的根本不知道程式可以被「證明」。

現在 agentic AI 把兩邊強制拉回來。原本三千人的冷門領域，突然變成每個寫 agent 的人都得學一點的基本功。

寫到這邊我自己的感想是，這幾年最會賺的人應該是「會兩種語言的人」。會邏輯也會工程、會技術也懂治理、會 build agent 也懂 spec out 規則。Byron 講過一句話我很喜歡：這種 bilingual 的人現在 worth their weight in gold。

如果你跟我一樣每天在追 AI、agent、產業變動的最新動向，wilsonhuang.xyz 上還有更多這類深度整理，歡迎訂閱一起追。

Sources:

• Prof. Dr. Byron Cook, FREng - UCL Computer Science
• Byron Cook | DARPA
• AWS Security Profile: Byron Cook, Director of the AWS Automated Reasoning Group
• A chat with Byron Cook on automated reasoning and trust in AI systems