AI coding 整合正規方法

驗測 AI coding agent 產出程式的正確性

Transcript

1. AI coding 整合正規方法 驗測 AI coding agent 產出程式的正確性 企業架構科 鄭淳尹 Philipz 2026.09.30
2. AGENDA 1. 正規方法簡介 2. Quint簡單範例：銀行轉帳 3. Quint複雜範例：線上訂票 4. Redlock演算法驗證 5. 結語
3. 01 正規方法簡介
4. 正規方法 亦稱形式化方法（Formal Methods）是以嚴密 數理邏輯為基礎，對計算系統的行為規格、 體系架構與程式碼實作進行無歧義描述與數 學驗證的技術體系。 模型檢驗（Model Checking）則是正規方法轄 下最具工業突破性的全自動演算法分支，其 核心機制在於將被驗證系統抽象為有限狀態 轉移結構，並演算法化地判定該結構是否滿 足時序邏輯（Temporal Logic）所規範之行為 性質。當目標性質遭違背時，檢驗器能全自 動生成可重現的抗例路徑（Counterexample）， 為分散式交錯與並發缺陷提供確定性的除錯 軌跡。 4
5. 正規方法的應用案例 • 著名的Pentium bug 1994年，Intel的Pentium CPU竟然出現了嚴重 設計瑕疵，迫使Intel收回成品，造成嚴重損失。 而CMU的團隊證明他們的BDD技術有能力檢測 出該項設計瑕疵。 • 晶片設計與半導體 EDA(電子設計自動化) 模型檢驗 / 屬性驗證（Property Checking / Model Checking）：以 SystemVerilog Assertions (SVA) 或 PSL 為規格，利用 SAT/SMT 或 BDD 引擎窮舉證明 RTL 設計是否符合時序 行為性質，或尋找角落情境反例（Corner-case Bugs）。 5
6. MIT物理教授Max Tegmark也提到AI與正規方法的結合 6
7. 個人在模型檢驗相關的研究 研究所論文於2006年發表在國際期刊，主要使用UML的狀態圖轉成Model Checking狀態，用高階視角檢查有無規格設計問題 7
8. 正規語言與模型檢驗工具 TLA+/TLC Quint UPPAAL 由 LaTex作者 Leslie Lamport 發展 新一代 可執行規格語言 擅長時序邏輯驗證 已被用於分布式共識演 目的是減少傳統形式化工 圖形化狀態機介面，支 算法（Raft, Paxos）、 具在現代軟體工程管線的 援連續時間或物理時間 分佈式資料庫分散式交 採用門檻，支援 Claude 轉化為其正規語言， 像 易、非同步容錯協定。 Code/Codex 的Skill，讓 Redlock問題發生在 AWS並在S3服務上線前 LLM快速轉譯成Quint語言 「假設各節點與客戶端 抓出了一個會導致資料 ，且輕量化可以整合到CI 的物理時鐘單調且偏差 遺失的正確性漏洞。 測試步驟中。 有界」，只能用此模擬。 8
9. 02 Quint簡單範例 銀行轉帳
10. // 5. 轉帳動作 (Transfer Action) action transfer(from_acc: str, to_acc: str, amount: int): bool = { all { from_acc != to_acc, amount > 0, Quint轉帳規格 bank.qnt module Bank { // 1. 定義狀態變數 (State Variables) var balances: str -> int withdraw(from_acc, amount).then(deposit(to_acc, amount)), } } // 定義帳戶集合 pure val ACCOUNTS = Set("Alice", "Bob") // 2. 初始化動作 (Init Action) action init = { // 將 Alice 與 Bob 的初始餘額皆設為 100 balances' = ACCOUNTS.mapBy(_ => 100) } // 6. 步進轉移 (Step Action) action step = { nondet sender = ACCOUNTS.oneOf() nondet receiver = ACCOUNTS.exclude(Set(sender)).oneOf() nondet amount = 1.to(100).oneOf() // 任意挑選一個1到100之間的轉帳金 額 transfer(sender, receiver, amount) // 3. 存款行為 action deposit(account, amount) = { // 增加指定帳戶的存款餘額 balances' = balances.setBy(account, curr => curr + amount) } // 4. 提款行為 action withdraw(account, amount) = { // 扣除指定帳戶的存款餘額 balances' = balances.setBy(account, curr => curr - amount) } } // 7. 總金額守恆不變量 val total_money_conserved = { ACCOUNTS.fold(0, (sum, acc) => sum + balances.get(acc)) == 200 } // 8. 帳戶餘額不可為負數 val no_negatives = ACCOUNTS.forall(acc => balances.get(acc) >= 0) } 10
11. 檢查Quint轉帳規格 執行quint run bank.qnt -invariant=no_negatives時， 檢查帳戶餘額是否永遠大 於0元，命令列會回傳 [violation] Found an issue錯 誤，並印出完整的反例執 行軌跡（Trace） ，發現有 負數情況。 11
12. 正確的Quint轉帳規格 module Bank { // 1. 定義狀態變數 (State Variables) var balances: str -> int // 定義帳戶集合 pure val ACCOUNTS = Set("Alice", "Bob") // 2. 初始化動作 (Init Action) action init = { // 將 Alice 與 Bob 的初始餘額皆設為 100 balances' = ACCOUNTS.mapBy(_ => 100) } // 5. 轉帳動作 (Transfer Action) action transfer(from_acc: str, to_acc: str, amount: int): bool = { all { from_acc != to_acc, amount > 0, balances.get(from_acc) >= amount, // 前置條件（Guard）：餘額必須足夠！ withdraw(from_acc, amount).then(deposit(to_acc, amount)), } } // 6. 步進轉移 (Step Action) action step = { nondet sender = ACCOUNTS.oneOf() nondet receiver = ACCOUNTS.exclude(Set(sender)).oneOf() nondet amount = 1.to(100).oneOf() // 任意挑選一個1到100之間的轉帳金 額 transfer(sender, receiver, amount) // 3. 存款行為 action deposit(account, amount) = { // 增加指定帳戶的存款餘額 balances' = balances.setBy(account, curr => curr + amount) } // 4. 提款行為 action withdraw(account, amount) = { // 扣除指定帳戶的存款餘額 balances' = balances.setBy(account, curr => curr - amount) } } // 7. 總金額守恆不變量 val total_money_conserved = { ACCOUNTS.fold(0, (sum, acc) => sum + balances.get(acc)) == 200 } // 8. 帳戶餘額不可為負數 val no_negatives = ACCOUNTS.forall(acc => balances.get(acc) >= 0) } 12
13. Quint LLM Kit：AI Agent的規格寫作與驗證加速器 為了降低工程師與AI工具採 用Quint的學習門檻， Informal Systems開發了開源 套件Quint LLM Kit （https://github.com/quintco/quint-llm-kit），這是一套 專門為大型語言模型（LLM） 與AI Coding Agent設計的技能 工具包（Agent Skills）與容 器化開發環境，旨在讓AI能 夠無縫進行Quint規範的建模、 驗證與程式碼生成。 13
14. 03 Quint複雜範例 線上訂票
15. Restate分散式訂票系統 https://next-restate.everfine.com.tw/booking 15
16. 分析程式碼自動產生Quint規格 https://github.com/agent-playground/restate-cloudflare-workers-poc 16
17. 分析 checkoutBuggy.qnt 找出的錯誤設計 此時序圖展示修復前程式碼因缺少身分檢 查與認領守衛，如何導致雙重成交與奪票： 1. 致命驗證：票已賣給 Bob，Alice 呼 叫 confirm 依然回傳成功（雙重成交 RC2） 2. 致命驗證：第三方可直接釋放他人的有 效保留（RC1） 3. 致命驗證：未經預訂即可將 AVAILABLE 席位轉為 SOLD 17
18. 從錯誤反例修補程式 https://github.com/agent-playground/restate-cloudflare-workerspoc/blob/main/test/race_counterexample.test.ts 此時序圖展示修復後，在遭遇相同並發插 隊時，如何透過認領守衛（Caller Guard） 成功阻斷錯誤並啟動補償，並在 CI 加上錯 誤測試腳本，每一次程式碼異動都會檢查。 // test/race_counterexample.test.ts — 機械化重現 Quint 反例 （specs/checkoutBuggy.qnt S0-S11）的獨立測試套件。 // // 驗證目標： // 1. 重現 Quint 在 checkoutBuggy.qnt 所找到的 11 步交錯軌跡 （Trace） // 2. 斷言修復後的實作能成功阻斷反例，使 P1（不可雙重成交） 與 P2（已付款者持有票）在實作層恆真。 // 3. 支援獨立單獨執行，並納入 npm test / CI 自動化測試。 18
19. 04 Redlock演算法驗證
20. Redis分散式鎖演算法 Redlock 爭論 https://martin.kleppmann.com/2016/02/08/how-to-do-distributed-locking.html https://antirez.com/news/101 DDA作者 Martin Kleppmann 跟 Redis 作者 Antirez 對於 Redlock 安全問題有激烈討論 20
21. 先由AI agent進行程式碼分析產出Quint規格檔 使用 /grill-me + /quint-modeling 來跟 agent 討論逐一確認需求 21
22. Quint分析結果 https://github.com/agent-playground/node-redlock/blob/factory/quint-verified-v2/specs/README.md 22
23. UPPAAL分析結果 https://github.com/agent-playground/node-redlock/blob/factory/quint-verified-v2/specs/uppaal/README.md 23
24. UPPAAL執行畫面 – 軟體需要授權序號 https://uppaal.org/ 紅燈代表不滿足，表示有反例，需 要修正此錯誤。 Quint不支援連續時間或物理時間轉 化為其正規語言，UPPAAL可以模 擬物理時鐘，將客戶端的 Date.now() 往後調 5ms，就能讓 兩個客戶端因時間差同時進入異常 臨界區。 CLI模式 verifyta specs/uppaal/redlock_f9.xml specs/uppaal/redlock_f9.q # 全部查詢 verifyta -t1 specs/uppaal/redlock_f9.xml /tmp/one.q # 產生最短反例軌跡 24
25. UPPAAL反例軌跡模擬畫面 https://uppaal.org/ 25
26. 針對Redis官網推薦實作node-redlock發出 fix PR https://github.com/mike-marcacci/node-redlock/pull/369 分析表示，即便是知名套件仍有漏洞，在三大LLM模型都發佈誤駭新聞稿，基礎開源 套件或函式庫的安全漏洞是非常需要關切，如同黃仁勳點名 Cybersecurity 是下個機會 26
27. 05 結語
28. 採用正規方法的關鍵在自動形式化的正確率 28
29. 為何 AI coding 必須整合正規驗證 https://martin.kleppmann.com/2016/02/08/how-to-do-distributed-locking.html 為何20年前就出現的正規方法，直 到現在才有機會廣泛使用在一般業 01 務系統，關鍵在於自動形式化，如 果正規語言有提供skills，如Quint LLM Kits，就可透過LLM協助自動翻 譯成形式化規格或模型檢測描述， 在高層次建模或規格中，找出程式 邏輯設計錯誤，尤其是分散式演算 法這類複雜系統設計。藉此，AI coding agent產出的程式碼才能放心 地部署到正式環境。 驗證出 Redis分散式鎖演算法 – Redlock 確實存在缺陷 29
30. AI coding 輔助工具只會取代低階開發人員 TLA+/LaTex 作者 Leslie Lamport Programing ≠ Coding 01 30
31. 延伸閱讀： CTIMES- 軟／硬體的正規（formal）驗證 Autoformalization with Large Language Models 31