https://softwareengineeringdaily.com/podcasts/software-verification-in-the-age-of-coding-agents/
Software Engineering Daily 這一集由 Sean Falconer 主持，來賓是 Antithesis 的 Carl Sfera。他在公司的 Red Team，也帶相當一部分 AI 策略。Antithesis 做軟體 verification。做法叫 deterministic simulation testing。平台把客戶的軟體放進完全受控的環境，執行時探索幾千條路徑。路徑事先沒有寫死，團隊預期會走到的情況只是其中一部分。一般 test 確認的是人已經想到的行為，殺傷力大的故障躲在開發時沒人去查的邊角。AI 寫出的程式愈來愈多沒有人仔細看過，這些盲點跟著變大。節目把測試說成做可靠系統少不了的一環，也是最難做好的事之一。
Red Team 向產品負責人回報
Carl 職務上在 Red Team。這支隊伍不是資安紅隊。名字來自一個假設：若請一群一輩子在建分散式系統、也在測分散式系統的人，給他們幾乎沒有上限的 Antithesis 使用權，讓他們先把這套技術用到很熟，再拿這支隊伍去幫客戶把技術用滿，會怎樣。
他給自己的目標是成為 Antithesis 的專家，然後幫客戶找出分散式系統裡很難的 bug。AI 策略那一塊，讓他同時面對客戶跟產品。公司另有完整的 FDE 團隊，每天在客戶那邊，幫他們寫 test harness、把 Antithesis 用起來。Red Team 是內部後援。進到一家客戶的狀況裡，先找出這家要成功還缺的那一步，再交回 FDE，讓 FDE 手上有足夠的資訊跟知識去做判斷。FDE 從這裡學到做法，再套到很多客戶，少數人的經驗就被放大。
Sean 提到這些經驗該流回產品，不能每次遇到都只修那一次。Carl 確認了。Red Team 向上報給產品負責人，不在業務組織裡。放在產品底下，是為了把東西做進產品，每一個客戶都用得到。
角色不好命名。它站在對客戶跟對產品中間，所以需要一個抽象、活動空間大的名字。Sean 在待過的公司看過不同版本，自己在 Google 也待過這類團隊的某些區塊。他說這類功能很有用，只是還沒有大家都同意的主流名稱。位置大概同時踩著產品工程跟 field engineering。
Red Team 裡每個人盯一塊產品。Carl 盯跟 AI 的關係。Antithesis 的 AI skills repos 是他寫的。另外有一支給 Agent 用的 CLI，讓 Agent 跟產品互動。隊友 Lawrence 盯 property-based testing 的函式庫，名字是 Hegel 跟 Bombadil。每人在自己感興趣的那一面，多放一點產品時間。
回歸 test 把已經存在的行為釘死
可靠性工具跟測試長期投資不足。一個壞 bug 對產品體驗的殺傷很大，最好的工程師卻通常不會被放去想測試策略。Sean 說，Antithesis 執行長 Will Wilson 也講過類似的話。測試被當成多數工程師討厭的雜務，肯專心做的人很少。
Carl 用 SingleStore 的十年說明他看到的原因。公司以前叫 MemSQL。他們做資料庫，測試上砸了非常大的工程力氣，文化是很極端的 shift left。寫程式的人同時寫 test，整件事自己負責。
他們發現，測試愈能從一種寫法展開成很多種情況，工程師愈願意用。內部的測試叢集叫 Sidux。Sidux 讓人寫會展開的 test。寫一條，把輸入空間參數化，就變成很多條。測試於是變成一個工程問題。工程師得先想要測什麼、有哪些測法，再寫一條會生出各種攻擊方式的 test，去驗證這一段程式。
工程師不愛 test，他覺得常常是因為 test 多半在做回歸。功能 X 做完，test 把功能 X 釘進可接受的結果裡。為未知的未知寫 test 很難。那也是他覺得比較有趣的 test。組織於是不想把最好的人放上去。寫出來的 test 停在回歸空間，把已經存在的行為編碼進去。未來空間裡那些還沒被想到的情況，很少有人寫。
未知的部分長成一棵樹
那種未來空間難測，先難在狀態。程式大致分成純的，跟有狀態的。純的程式，大家拿 unit test。若干輸入對上若干可接受的輸出，怎麼測很直接。比較有意思的軟體，再往上到高階一點的系統，尤其分散式系統，幾乎整包都高度有狀態。行為取決於到這一刻為止、整套軟體收過的輸入，也取決於以後所有可能的輸入。空間非常大。
要測的行為很多從故障長出來。想問的是 A 發生之後 B 發生，然後 C 發生，而 B 跟 C 是壞事。輸入錯了，或某個地方出錯。人通常寫 integration test，把一條特定的時間線編碼進去。人腦好處理這種東西。強迫軟體依序做 A、做 B、做 C，想得清楚。
要為一個還不知道存不存在的情況寫 integration test，做法就不明顯。勉強說得通的路，是在步驟 A 試所有可能的輸入，再對每一個 A，在步驟 B 試所有可能的輸入，然後繼續往下。長出來的是一棵樹。Sean 直接把它叫組合問題。
狀態機若是純的，沒有非確定的副作用，測起來直觀。現代軟體的情況不一樣。分散式系統的 state space 有一大片是非確定的。那些非確定性沒辦法用確定的方式模擬，問題就變硬。Carl 回憶 SingleStore，也就是進 Antithesis 之前。他們多半停在 integration test，測已知存在的事件序列，那些基本上是回歸。偶爾在路上注入故障，確認某個錯誤有被處理對。另一種是 stress test。不鎖一條時間線，改測極大量的隨機時間線，再看總體有沒有想要的性質。它們都收斂，或都恢復得回來。
未知的未知就是難測得多。多數人寧可守比較簡單的那格，確認最明顯的失敗路徑有被處理。他認為最好的測試，是能碰到未來那片可能性的測試。
壞天氣要連續下，mock 要比正式環境更糟
Netflix 把 chaos engineering 做出名。Carl 認為那就是在處理這種未知。Meta 講過類似的做法，Google 對 Google Cloud 也做不少 chaos engineering。Sean 補了一層。記得住的名字是 Netflix 取的。超大規模的公司大概早有類似功能，名字沒那麼響，後來別人從 Netflix 那邊學。
在 Carl 的描述裡，Netflix 做的是大規模 stress test，而且放在正式環境。系統若不斷處在壞天氣裡，可靠性會被逼著做快，比壞天氣很少出現時快得多。壞天氣指的是故障跟不正常條件一直發生。文化改成這些情況隨時都得應付。測試系統本身也可以變成一場不中斷的壞天氣 stress test，並要求系統在那種天氣裡隨時活得下來。
Sean 有過一個沒有名稱的版本。他第一份工程工作大約在 20 年前，人還在唸大學。開發伺服器又差又慢。東西在那裡能以還可以的速度跑起來，上正式環境就知道沒問題，因為正式環境容量大得多，機器也好得多。那個環境夠快，上線會更快，也扛得住一整排條件。
Antithesis 的客戶到了某個時點要把系統帶進平台，有時得 mock 一個外部服務。依賴 Stripe 是他常舉的例子。Stripe 放不進 Antithesis，得做一個像 Stripe 的東西。常有人問，mock 的擬真若跟 Stripe 不相等，測試算不算無效。他的框法是，mock 要比實際會發生的更糟。只要行為是正式環境的超集，而且多出來的都更糟，就可以拿來驗證軟體。做一個失敗情境更寬、比完美擬真更糟的 mock，有時比做一個完全擬真的 mock 容易。他用這個方式把這筆帳配平。
系統現在還會依賴另一種非確定。業務邏輯在多步流程裡問 LLM 下一步做什麼，再用機率看輸出多常符合預期的形狀。Carl 不覺得這改變了測試的觀念。它把要測的 state space 打開不少。從那一點能走的下一步可能爆開。極端的例子是讓 LLM Agent 在 Linux sandbox 裡跑，機器上它想做什麼就能做什麼。下游所有會對這個新輸入起反應的軟體，都得應付寬很多的輸入。所以更需要 DST 這種、把所有可能的下一步都拿去測的做法。
整套系統只接受平台注入的非確定性
Carl 跟客戶講 DST，先拆成兩樣材料。第一樣是確定性。受測的系統要能重播。做法不止一種。Antithesis 對 Linux 軟體提供自動的做法。軟體照原樣部署上來。可以把它想成一個部署目標，像一台 EC2。整套軟體都跑在同一台裡面，例如拆成幾個 Docker container，整個系統就是確定的。它只會遇到平台注入的非確定性，注入由平台控制。軟體自己仍看得到隨機、時間，以及可能不一樣的事件順序。平台注入的那一份，可以原樣重現。
另一條路是改寫軟體，把所有可能的非確定性都改成從外面注入。環境得被控制。讀時間、讀隨機這類來源時要可控，排程也要可控，事件順序照受控的方式發生。
隨機數不用客戶自己 mock。在 Antithesis 上這件事交給平台，系統的隨機性由他們控制。從系統讀隨機數，例如 Linux 的 /dev/urandom，拿到的都是平台完全控制的值。很多軟體會讀 /dev/random 跟時間，把位元混過，再拿去初始化一顆 PRNG，讓隨機數生得比較快。多數 runtime 都這樣做。跑在 Antithesis 上時，他們建議不要留著這顆 PRNG。軟體若要用隨機，改成每次直接讀系統的隨機來源。
原因是第二樣材料：模擬。他們要在每一個當下控制隨機。一顆已經排好後續數字的 PRNG 做不到這件事。每次做決定都得來問平台。DST 要能把模擬分叉。軟體可以看成一連串輸入造成的狀態改變。起點是根時刻，程式剛起來，狀態完全已知。接著輸入進來，歷史沿一條線往前走。因為確定，可以回到這條線上的任何一點再分出去。在那一刻改掉隨機，從那一刻長出另一條時間線，往後走它自己的歷史。
每次決策都讀平台的系統隨機，分叉就能切得很細。中間若夾一顆 PRNG，時間線就算分叉，新的分支仍會看到同一串隨機數，除非有辦法把 PRNG 重設。確定性指的是軟體每次看到同一串事件，而且可以重播。模擬指的是把那條時間線分成新的時間線，去試不同的事件順序。
他用三個節點的分散式系統舉例。先等到其中一個節點因故崩潰。多數這類系統，例如 Raft，應該承受得住一個節點死掉。崩潰之後分出一大束時間線，試不同的後續。那個節點若在新的領導者選舉走到一半時恢復，會不會出現壞事。能從任一點分叉，用不同順序試不同的事，等於對軟體的 state space 做廣度優先搜尋。
分支爆得快的地方，搜尋就往那裡擠
平台怎麼決定往哪分叉，Carl 說跟檢查上傳程式的位元組很接近。做法接到 fuzzing，也就是隔壁那塊研究。他用 JPEG encoder 說明。要驗證的是，encoder 吃得下任意數量的輸入位元組，隨便什麼雜訊，永遠編成合法的 JPEG，或乾淨地報錯，例如絕不崩潰。裡面一種策略叫 coverage-guided fuzzing。監看受測程式走了哪些分支。libjpeg 內部很多 if，各自走不同分支。記錄哪些分支被觸發。隨機雜訊送進去，慢慢做出對照。這份雜訊觸發這一串分支，換一份雜訊，另一串分支被走到。迴圈轉得很緊、轉很多次，對系統累積出知識。
Sean 把它說成黑箱。輸入進去，同樣的輸入得到同樣的輸出，再改輸入去改輸出。他聯想到去年一集談逆向晶片。Apple 不給晶片藍圖。靠輸入可以模擬硬體會生出什麼，看實際發生什麼，做出一個行為上模仿那顆晶片的模擬器。內部怎麼做不知道，知道的是輸入跟輸出。
Carl 說 DST 用的是同一類策略。軟體在 Antithesis 裡跑，完全確定。coverage 的分支是他們監看的輸入之一。系統上還有別的訊號，用來分辨現在看到的是新行為，還是已經見過的行為。他們會偵測自己是不是在繞圈。若在繞，就分叉，試著跳出那個圈，去找另一塊值得操的程式。
這樣跑會自己冒出一些性質。其中一項是，某種 thread 順序造成的 bug 很好找。thread 怎麼拿 lock、怎麼碰共享記憶體，都在這類裡。那一塊若很快出現不同的分支路徑，平台會派出一批自己跑的搜尋，全部從那段爭用很兇的程式開頭出發。最近對上的例子是 SQLite。
今年稍早，SQLite 有一個被回報、然後被修好的 bug。它在專案裡待了 10 年，大約從最初寫 write-ahead log 的程式就在。Carl 會追 SQLite。他把這個 bug 叫 WAL reset。形態是很難抓的並行問題。一條 thread 從共享記憶體讀出資料，然後睡著。另一條 thread 改了那份資料。第一條醒來，沒有在醒來之後做正確的重新驗證。窗口緊到他相信，大概只有一個 SQLite 大客戶真的撞上過。那個客戶是 Tailscale。釘死這個 bug 花了很長時間。Tailscale 今年稍早做了很多研究，把發現發表出來，bug 接著被修好。
他看到時認為，這個形狀正好是 Antithesis 該能很快找到的。他拿修補前、還帶著 bug 的那一版，放進平台，配一份很簡單的 workload。workload 迴圈做 insert 跟 WAL checkpoint。沒有專門瞄準這個 bug，但有操到相關程式。跑下去，15 分鐘後 fuzzer 找到它，並把範圍縮到必須發生的那一串操作順序。
這份 workload 確實用上了他事先知道 bug 在哪一帶。焦點放在那一塊程式。很快找到之後，他另寫一份通用的。所有 SQLite 操作以均等機率出現。有 select，有 insert。不只走 write-ahead log，也走預設那套以 journal 做交易的系統。等於把整個系統操過。這份仍然在大約 15 分鐘內找到同一個 bug。
平台會自己注意到哪些區域把行為空間炸開。一批新行為出現，fuzzing 的力氣就集中過去，直到新行為出現的速度慢下來，再換一塊。
日誌的順序是真的，時間也可以倒回去
用的人若只拿到「這個輸入產生了不該有的輸出」，還是不知道往哪看。平台給的第一樣是日誌。全部日誌合成一個視圖，而且跟操作順序嚴格對齊。傳統分散式系統裡，兩件事誰先誰後常常得猜。Antithesis 控制所有執行怎麼被排成序列，日誌裡的順序就是模擬裡的順序。解析度因此很高。
第二樣是 properties。系統放進來時，要一併給一大批 property。他測 SQLite 用的那條很簡單。請平台跑 pragma integrity check，也就是 SQLite 內建、用來問資料庫有沒有損壞的檢查。模擬跑起來之後，隨機挑時間點執行。一旦發現損壞，fuzzing 會往那個區域收。這是另一個「這裡有東西」的訊號。沿著發現問題的任何一種順序，都能回看系統，也等於告訴平台，什麼情況算是這套系統可能壞了。
後面兩樣，讓它跟單純的 observability 平台分開。multiverse debugging 允許在模擬的任何時刻 SSH 進系統。假設 integrity check 在大約 30 秒失敗。前 30 秒裡有東西把資料庫弄壞了，但不知道是哪一刻。可以 SSH 進那個叢集，跑 SQLite 的操作，把時間倒回，用二分搜尋找損壞真正發生的點。找到之後可以進 GDB。
causality analysis 把這件事改成平台自動做。找到 bug，想知道它在哪一刻被鎖進模擬，平台自己做二分搜尋。時間倒回，擾動環境，再往前滾，看 bug 在哪裡被定住。
編譯期擋得住的，跟模擬撞出來的，疊在一起
Sean 提到稍早 Joe Hellerstein 從 AWS 來談 Hydro。那個專案想在編譯期用 type system 抓住分散式 bug。某些類別的 bug 寫不出來，compiler 會擋。力氣放在事先證明。Sean 把它想成測試這件事上的 formal methods。Antithesis 則在執行期用模擬把系統撞開。
Carl 對 Hydro 不熟。他在意 proof 是落在實際程式上，還是落在一份形式化的抽象模型上。Sean 依記憶講的是編譯期檢查。人在寫程式，編譯時判斷這段會不會在分散式系統裡壞掉，從一開始就不讓它被寫出來。檢查烤在軟體裡，像型別檢查抓到 int 被塞進 string，或反過來。
Carl 把 Hydro 放在靜態 verification 這一類，而且是很進階的一種。同類的事早就在發生。寫 Rust 的人靠 type system 拿掉一批 bug。寫得很純、也很安全的 Rust，可以拿掉整類記憶體方面的 bug。他認為這件事該做。跟有 bug 的軟體之間，防線愈多愈好。
有些靜態做法會逼人用特定方式寫程式，嵌進 runtime，或嵌進程式怎麼被組織。那種寫法未必直覺，問題不一定表達得了，為了做出 proof，實作也可能得妥協。這類系統有時比較適合 greenfield，也就是從零開始、照那些性質把程式寫成特定形狀。Hydro 算不算這一類，他不懂，不能斷定，也許對方已經做得更好。自己從頭做 DST，他認為很有價值，也值得做，但對開發力氣抽稅很高。他想知道靜態檢查蓋得住哪些類別，哪些仍是未知。就算靜態那層在，上面再加一層像 Antithesis 的東西，他仍覺得這層值得加。
Formal methods 的取捨是另一套。人會為同一套系統做一份抽象模型，再證明它帶有某些正確性 invariant。那是模型上的 proof。Hydro 在 Sean 的描述裡，檢查的是正在寫的那份程式。
整疊測試裡，deterministic simulation testing 的位置比較靠近 integration test 跟 stress test。小塊、彼此獨立的程式仍用 unit test，那是最快的查法。能花得起錢的測試種類，他認為仍該盡量用，整體的程式品質會更好。AI 進來之後，測試愈多愈好。模型被約束得愈緊，交出好品質的機會愈高。
Antithesis 特別好用的地方，是拿去測未知的未知。一條這種 test 寫一次，幾乎可以測到軟體整個 state space。理論上，可能發生的事、壞的事件順序，都碰得到。integration 這一層因此適合它。同時測多個元件，一套分散式系統是例子，一個 CRUD 應用也是。有資料庫，有橫向擴出去的 web server，有 cache，有 client。這樣就夠出現怪情況。client 對一個節點送出寫入，寫入進了 cache，沒有馬上刷進資料庫，再到另一個節點讀，然後失敗。這些失敗的樣子跟事件順序，他覺得很難在 integration test 裡逐條寫完。用模擬去試，對他比較自然。
Sean 說，分散式系統常被講成只有規模很大才會碰到。現在的系統幾乎都是分散的。資料庫、client 跟 server 分開的做法存在很久，早於雲，也早於 Kubernetes。很簡單的三層架構一樣會出這些 bug。
Carl 把範圍再往程式裡面收。單一 process 裡，多條 thread 共享記憶體，或用訊息傳遞，這已經是一套分散式系統。要知道它正確，得把事件可能的順序想清楚。
給 Agent 一條會失敗的 test，它會貼著那一條寫
Carl 最近在教 AI，替任意軟體寫能在 Antithesis 跑的 workload。做這件事時，他也在學怎麼把 Antithesis 交到 AI 手上，讓它能問未來會發生什麼。
test driven development，也就是 TDD，走法是先寫一條 integration test。它會失敗，因為它依賴一個還沒寫的功能或改動。然後讓 AI 迭代，直到這條 test 過關。他覺得這對 AI 可能走錯。AI 會緊盯給它的目標。Sean 說，這就是對那條 test 過擬合。Carl 同意，結果就是擬合得很緊。
同一件事放到 Antithesis 上，他另給一個暫定名字，ADD，Antithesis driven development。這條路上幾乎沒有東西可以過擬合。平台的工作就是找 counterexample。程式改到行為符合測試之後，沒有一條很窄的案例可以死記。要守的是很一般的 property，例如資料庫永遠不損壞。對這種 property 做過擬合難得多。實作會被迫用最通用、也最正確的方式寫出來。
十五分鐘看明顯的回歸，隔夜十二小時模擬三個月
模擬要跑多久，決定它能不能進開發迴圈。unit test 很快。把編譯當成 test 也很快。做 AI coding 時，不能編譯，或沒過 unit test，回饋幾乎是立刻的。
Carl 把成本拆開看。若 workload 已經在，SQLite 那份就是。同一份已經把 state space 跟表面都測過的 workload，可以拿去驗新功能，繼續看 property 是否仍成立，資料庫有沒有損壞。跑愈久，信心愈高。平台是在對 state space 做廣度優先搜尋。15 分鐘有一些 coverage。1 小時更多。再往後大概會進入高原。跑到 12 小時，也許過了某個時數，增值就很少。他說像 8 小時那種。
接進開發流程時，跑的時間接近指數往上拉長。單一 PR 上，也許只跑 15 分鐘。這 15 分鐘的預設平行度是 48。系統裡還有快轉。程式若 sleep，時間會被快轉到那個點，不必用真實時間等待。因此常常看到至少 48 倍的加速。程式形狀不同，倍數可以高很多。workflow engine 或 job system，有可能到大約 1000 倍。15 分鐘裡，模擬時間很容易累積到好幾個小時。對「沒有弄壞明顯的東西」，這已經有相當高的信心。
還沒測過的範圍愈大，跑的時間也拉得愈長。從 PR 傳到主整合分支，他用一道波形容這層信心。PR 上的測試短，回饋快。昨天送出的程式，隔夜會在 12 小時的 stress test 上跑完，在 Antithesis 裡模擬大約 3 個月。到這一步，對沒有某種大的災難性 bug 會很有信心。3 小時前才合進去的 PR，可能只跑過 1 小時，信心少一截。
他們最近開始試另一件還沒做完的事：讓 Agent 對還沒跑完的輪次下指令、提問。Agent 可以在 Antithesis 啟動一輪，立刻訂閱它在意的某一個會失敗的 property。那個 property 若在開始後的前 5 分鐘就失敗，Agent 可以馬上收到通知，接著除錯，不必等整輪結束。
規格要準到能導出 property
Sean 把測試變緊這件事，連到程式生成變多。生成那段程式的人可能只看一點，或根本沒看，跟程式沒有以前那種連結，也未必懂它。他沒有把「AI 寫的每一行都比人差」當成前提。責任落到測試跟 verification。風險是程式大量送出，人沒看，或幾乎沒看。跟幾年前比，時間跟計算要花在哪，這筆帳不一樣了。
Carl 同意。寫程式花的時間下降，省下的力氣應該改配到 verification 跟規格。他看以後的工程工作，是把規格寫到非常準，用比現在更高的精度規定要什麼。Markdown 文件，他認為未必達得到那個精度。verification 要跟規格對得起來。他要的是一張網：所有可能的路徑是否都符合規格。規格導出程式該守的 property 跟 invariant，寫進 Antithesis 的 workload。模擬裡每條路徑都要落到合法的 property 結果，不能出現 counterexample。Agent 就會把力氣放在寫出能安全待在這張網裡的程式。
他最近另外在想影像 diffusion，也就是 AI 一次長出整張圖的那種過程。在某個可能的未來，生成程式的量大到，軟體工程可以離開一輪一輪的迭代：規格一改，整個程式庫重新長一次。它符合規格，也通過那張罩住 state space 的網，就把這份全新的程式庫當成新版本釋出。實務若往這個方向靠近，這個工作會變成什麼樣，他想看。verification 那一側，他認為 Antithesis 是一種解法。
軟體開發就算只看最近 6 個月，變動已經很大。Sean 不覺得現在停在穩態。接下來幾年還會大幅變，也沒有人確定會停在哪裡。過程裡會有高，也會有低。