Antithesis：軟體 Bug 抓不到、重現不了？華爾街量化巨頭破例掏出 1.05 億美元買這台確定性電腦
FoundationDB 原班人馬歷經五年半隱形研發，打造確定性虛擬機與 AI 自主壓力測試平台；從 Jane Street 核心交易系統到以太坊 3,000 億美元資產遷移，重新定義軟體可靠性的邊界。
一分鐘速讀
市場痛點：74% 的量化機構曾在高波動期間遭遇基礎設施故障，分散式系統中的「Heisenbugs」幾乎無法重現。Knight Capital 曾因一個軟體部署疏失在 45 分鐘內虧損 4.4 億美元。
技術護城河：客製化確定性虛擬機 “The Determinator” 從 CPU 指令級消除硬體隨機性，搭配強化學習引擎在數萬個平行宇宙中自主探索系統狀態空間，並提供可倒轉的時光旅行除錯器。
資本驗證：2025 年 12 月完成 1.05 億美元 A 輪，由量化造市巨頭 Jane Street 破例領投，種子輪加總累計募資超過 1.5 億美元。
產業擴散：以太坊 The Merge 零事故遷移 3,000 億美元資產，MongoDB 深層 Bug 修復時間從數週壓縮至 3 天。Antithesis 正成為 AI 代理式開發時代的驗證基礎設施。
當演算法掌控 70% 交易量，最致命的風險藏在程式碼的時序縫隙裡
2012 年 8 月 1 日，美國造市商 Knight Capital 的交易系統在開盤後完全失控。一個名為 “SMARS” 的訂單路由系統因軟體部署疏失，意外啟動了一段已經廢棄的舊程式碼分支。在缺乏自動化斷路器的情況下，系統在 45 分鐘內向市場傾倒了數百萬筆錯誤訂單，累計交易 3.97 億股，直接造成 4.4 億美元虧損，Knight Capital 隨即被併購。
這起事件至今仍是量化交易史上最昂貴的軟體 Bug。但它暴露的問題遠比一家公司的存亡更深層：當全球股票市場超過 70% 的日交易量由演算法執行，外匯市場更高達 92% 的交易由自動化系統完成，整個金融體系的穩定性，實際上建立在分散式軟體架構的可靠性之上。
問題在於，這些架構的可靠性遠不如多數人想像。根據 Acuiti 與 Exegy 的聯合研究，在高波動市場中，74% 的量化交易公司曾遭遇市場數據基礎設施故障，包含延遲飆升、封包遺失或系統停機。僅有 3% 的受訪機構表示，其系統能在劇烈波動中穩定運作。
這些故障的根源，往往不是數學模型算錯了方向，而是底層分散式系統的「邏輯崩潰」。當極端波動來襲，訊息處理模組、風險控管引擎與訂單路由閘道器同時處於極高負載，多個執行緒搶著存取同一塊共享記憶體，微秒級的時序偏差就會引爆競爭條件。更麻煩的是，這類 Bug 在平穩市場中幾乎不會現身，只在最需要系統穩定的時刻才會爆發。工程師事後翻遍日誌，經常連崩潰的因果鏈都拼不出來。
這種「時有時無、無法重現」的 Bug，在軟體工程界有個精準的綽號：Heisenbugs，名字來自量子力學的海森堡測不準原理。你試圖觀察它，它就消失了；你以為修好了，它換個條件又冒出來。對於每日管理兆級交易量的量化機構而言，這不只是工程問題，而是資本安全的核心威脅。
五種測試方法，同一個結構性缺口
為了對付分散式系統中的隱藏缺陷，軟體工程界發展出了多種測試與驗證方法。但現代雲端架構、微服務與分散式資料庫的複雜度，已經讓系統的「狀態空間」（State Space）呈指數級膨脹。以下是五種主流方法的能力與盲區：
這五種方法各有所長，但它們共享同一個結構性缺口。能夠在程式碼層面精確執行的測試（單元測試、TLA+），缺乏真實世界網路的混沌與非確定性。能夠引入真實混沌的方法（混沌工程、Jepsen），卻因為無法精準控制硬體時鐘與作業系統排程，導致找到的 Bug 無法穩定重現。
換句話說，「確定性」與「真實混沌」在傳統工具中是互斥的。工程師只能二選一。
這個困境放在量化交易的語境下格外危險：當開發者無法穩定重現一個微秒級時序引發的Deadlock，他們只能靠猜測修復。若這種修復被部署到管理兆級資金的交易網路中，下一次極端波動就可能重演災難。
FoundationDB 原班人馬：五年半隱形研發，只為解一道題
Antithesis 的三位核心創辦人，CEO Will Wilson、CTO Dave Scherer 與 COO Nick Lavezzo，在創辦這家公司之前，已經親手解過一次「確定性」的難題。
他們是傳奇分散式資料庫 FoundationDB 的聯合創始人與核心架構師。FoundationDB 在 2015 年被蘋果公司收購之前，就以業界罕見的嚴格 ACID 事務保證與極高的系統穩定性聞名開源社群。一個規模不大的團隊能在短時間內打造出如此穩健的分散式資料庫，背後的秘密武器便是他們首創的確定性模擬測試（Deterministic Simulation Testing, DST）框架。這套框架讓工程師能夠在完全可控、可重現的環境中，對資料庫的分散式協定進行窮舉式的壓力測試。
但 FoundationDB 的 DST 框架有一個根本性的限制：它深度耦合在那套資料庫的底層架構中，無法被其他系統直接使用。Wilson 團隊意識到，如果能把「確定性模擬」這個概念從單一產品中抽離出來，重構為一個通用的基礎設施平台，它的價值將遠超一套資料庫。
2018 年，Antithesis 在維吉尼亞州成立。接下來的五年半，團隊幾乎完全處於隱形模式，專注於一件極其困難的底層工程：從零打造一台「確定性電腦」。直到 2024 年，產品才正式推向市場。
這段超長的研發週期本身就說明了技術難度。Wilson 後來回顧這段歷程時提到，團隊選擇在 Hypervisor 層級解決非確定性問題，而不是在應用層級做妥協，因為只有從最底層切入，才能讓任何語言、任何框架寫出的軟體都享受到確定性的保障。這個決策讓研發時間拉長了數年，但也築起了極高的技術門檻。
The Determinator：一台從 CPU 指令級消除隨機性的虛擬機
Antithesis 平台的底層核心，是一個名為 “The Determinator” 的客製化虛擬機管理程序（Hypervisor）。理解它的設計邏輯，需要先理解一個反直覺的事實：現代電腦本質上是「不確定」的。
傳統 Hypervisor（如 KVM、VMware）的設計目標是最大化硬體資源利用率，因此會讓虛擬機盡量直接與底層硬體互動。但高階 Intel 伺服器 CPU 內部充滿了非確定性機制：亂序執行、多層快取未命中、分支預測器的動態調整、非同步的硬體中斷。這些微觀行為會讓相同的程式碼在不同時間執行時，產生微小的時序差異。對一般應用來說，這些差異無關緊要；但對分散式系統的測試來說，它們是破壞重現性的元兇。
The Determinator 的設計哲學是「減法工程」：主動移除所有會將硬體非確定性暴露給虛擬機的標準功能，建立一個絕對封閉的「確定性泡泡」。它基於 FreeBSD 的 bhyve Hypervisor 進行深度分叉與改造，在三個層面實現確定性控制。
第一層：馴服時間。 The Determinator 向虛擬機完全隱藏物理時鐘。任何應用程式試圖獲取當前時間的呼叫，都會被攔截並回傳一個基於內部執行歷史計算出的「虛擬時間」。虛擬時鐘的推進，與 CPU 實際已退役指令（Instructions Retired）的數量掛鉤，透過 Intel 內建的效能監控計數器實現。即便計數器本身存在兆分之一的硬體誤差，團隊也開發了底層繞過機制來消除它。
第二層：隔離並發。 多核心架構下，多個執行緒在共享記憶體中的交錯順序是完全隨機的，這正是競爭條件的溫床。The Determinator 的做法很極端：強制每一個虛擬機實例只在單一物理 CPU 核心上運行。看似犧牲了平行效能，但平台透過雲端水平擴展來彌補，能同時啟動數千至數萬個隔離的單核虛擬機，各自探索不同的狀態分支。虛擬機內部的軟體仍「感覺」自己在多核環境中運行，因為 Antithesis 完全接管了行程排程器，可以精確控制每一次上下文切換的時機。
第三層：確定性 I/O。 任何與外部世界的互動（磁碟讀寫、網路封包、隨機數生成）都會打破確定性。The Determinator 利用 x86 架構的 VMCALL 指令作為客製化 API，將所有 I/O 操作轉化為嚴格的狀態轉換。主機可以將預先決定好的命令流或隨機數種子精準注入虛擬機，而這些輸入的瞬間，就構成了系統執行歷史中的「分支點」，讓外部演算法能將系統的運行軌跡描繪成一棵龐大的狀態決策樹。
三層控制疊加的結果：在 The Determinator 中運行的任何軟體，只要給定相同的初始條件與輸入序列，無論重複執行多少次，都會產生完全一致的行為，精確到每一條 CPU 指令。這是「完美重現」的物理基礎。
AI 引導的多重宇宙：讓強化學習替你找出「未知的未知」
有了一台確定性電腦，下一個問題是：如何有效率地在幾乎無窮盡的狀態空間中，找到那些深藏的致命 Bug？
Antithesis 的答案是放棄人工撰寫測試腳本，改用強化學習（Reinforcement Learning, RL）驅動的自主化測試。平台核心包含一個 AI 代理，它的任務不是生成程式碼，而是學習如何最高效地「破壞」你的系統。
RL 模型將受測系統視為一個探索環境。獎勵函數被設計為最大化程式碼覆蓋率的邊際增益，以及發現前所未見的稀有系統狀態。在測試過程中，AI 不僅會向應用程式的 API 發送隨機變異的輸入，還會同時對虛擬環境進行極致的混沌注入：隨機丟棄網路封包、模擬節點崩潰重啟、切斷網路分區、觸發極端的執行緒延遲。當某個故障組合引導系統進入了一段從未執行過的深層程式碼，AI 就會標記為高價值狀態，在此處建立檢查點並集中探索。
Antithesis 把這個過程概念化為「多重宇宙」（The Multiverse）。每一次測試不再是一條直線，而是分裂成數以萬計的平行分支。在宇宙 A 中，交易系統的網路在某個時刻斷線；在宇宙 B 中，網路正常但磁碟 I/O 被延遲 500 毫秒；在宇宙 C 中，資料庫主節點剛好在執行垃圾回收。AI 在這些宇宙間穿梭，不斷將系統推向邊界條件。
工程師不需要為每一種情境編寫獨立的測試案例。他們只需定義高階的系統不變性，也就是基於屬性的測試。例如：「系統絕不能發生未處理的異常」、「兩個微服務的狀態必須最終一致」、「保證金帳戶餘額不能為負數」。Antithesis 會在多重宇宙的每一個節點自動驗證這些屬性是否遭到違反。
當 AI 在某個平行宇宙中觸發了邏輯崩潰，確定性基礎設施的價值就完整展現出來。由於 The Determinator 記錄了所有初始種子與精確的指令序列，平台能提供完美的錯誤重現。開發者可以啟動「時光旅行除錯器」，將系統精確倒轉回崩潰前一秒鐘，單步執行程式碼、檢查每一塊記憶體狀態，甚至在虛擬機內部執行 tcpdump 檢視當時的網路封包。他們還能進行「破壞性分析」：在崩潰前夕人為修改某個變數，觀察系統是否仍會崩潰，藉此驗證對根因的假設。
這種能力從根本上消除了工程師最常說的那句話：「在我的電腦上明明會動。」
Jane Street 破例領投 1.05 億美元：當最挑剔的客戶變成最大的投資人
2025 年 12 月，Antithesis 宣佈完成 1.05 億美元 A 輪融資。這輪融資最引人矚目的，不只是金額，而是領投方的身份：Jane Street，全球頂尖的科技驅動型量化造市商。
Jane Street 每日處理全球兆級資產流動，擁有超過 3,000 名員工，向來以自研基礎設施著稱，極少涉足早期 B2B 企業軟體的風險投資。這家機構打破慣例領投其軟體供應商，背後是一段震撼性的技術驗證經歷。
Jane Street 內部有一個名為 “Aria” 的核心分散式系統。Aria 是一個超低延遲的共享訊息匯流排，提供嚴格的訊息排序與可靠性保證，是多個交易策略團隊構建高可用性微服務架構的根基。在引入 Antithesis 之前，Jane Street 已經為 Aria 建立了業界頂級的測試防線：純函數單元測試、模擬網路層的整合測試、Quickcheck 屬性測試、版本偏斜測試、AFL 模糊測試，加上預發布環境的持續混沌測試。即便如此，在面對真實世界的網路抖動與叢集重啟時，團隊仍無法保證萬無一失。
Jane Street 將 Aria 透過 Docker 映像檔載入 Antithesis 的確定性環境。在第一次執行中，平台就揪出了兩個團隊此前毫無察覺的深層 Bug，其中一個是近期才被引入、極可能在生產環境引發嚴重後果的漏洞。
後續的每晚自動壓力測試中，Antithesis 捕捉到了一個經典的競爭條件崩潰，完整的因果鏈如下：系統運行至 118.738 秒時，一個 standby replicator 服務在連上主伺服器後突然崩潰，拋出了損壞的二進制數據異常。工程師打開故障注入圖表，發現崩潰前 6 秒，Antithesis 的混沌引擎刻意殺死了一個 tip-retransmitter 服務。啟動時光旅行除錯器倒轉 1 秒，在虛擬網路上執行 tcpdump，發現 Replicator 客戶端向伺服器請求從位元組偏移量 313,425 開始傳輸日誌串流。但伺服器在重啟時，從磁碟載入的最新快照起始偏移量是 315,567。
客戶端請求的資料點，早於伺服器擁有的最舊資料點。伺服器本應回傳錯誤代碼，但由於近期一次跨區域傳輸功能的修改引入了未經周全考量的假設，伺服器沒有發出錯誤，而是把環形緩衝區中的空字元當作合法數據送出，觸發了客戶端的解析崩潰。
「服務意外中斷」、「快照落後」與「特定跨區請求時機」三個條件在微秒間隙內巧合觸發的競爭條件，傳統測試工具根本無從下手。Jane Street 工程師 Doug Patti 直言，若沒有 Antithesis 能夠定格時間並重現狀態，這個 Bug 如果發生在生產環境，團隊即使看到異常日誌也無法推導出完整的因果鏈。
與 Jane Street 共同參與此輪融資的，還有主導種子輪 4,700 萬美元的 Amplify Partners、知名創投 Spark Capital、Tamarack Global，以及 Stripe 共同創辦人 Patrick Collison。資金將用於擴張工程團隊、強化 AI 探索引擎與 Determinator，並擴大全球 GTM 運營，包含深度整合至 AWS Marketplace 等雲端通路。
跨領域戰果：以太坊 3,000 億美元遷移與 MongoDB 的除錯加速
Antithesis 的價值在「不允許失敗」的場景中最為顯著，而區塊鏈網路與分散式資料庫恰好是這類場景的代表。
2022 年 9 月，以太坊完成了歷史性的 The Merge 升級，將共識機制從工作量證明（PoW）全面轉換為持有量證明（PoS）。這是一次「在飛行中的飛機上更換引擎」的操作，承載超過 3,000 億美元資產與整個 DeFi 生態的信任。如果新舊程式碼在切換過程中因邏輯衝突導致區塊鏈分叉或節點大面積停機，市場衝擊將難以估量。
在合併前的一整年，以太坊基金會引入 Antithesis 作為終極防線。平台將 8 種不同語言編寫的以太坊客戶端（包含 Geth、Besu 等）以及新版 PoS 網路架構，完整載入確定性模擬環境。AI 代理持續對虛擬網路注入極端故障：網路延遲攻擊、拜占庭節點惡意行為、硬體失效。在此期間，Antithesis 協助發現並修復了 13 個致命的 Panic 與拒絕服務漏洞，以及 22 個區塊鏈營運與共識邏輯缺陷。
舉一個具體的例子：在代號 PR3813 的缺陷中，Antithesis 發現系統在早期證明者快取中，未能為即將到來的區塊正確產生證明。如果節點在驗證某區塊並設為 Head 之後的極短時間內被要求生成較早時槽的證明，就會導致「遺漏頂端投票」，進而引發共識斷層。這類由微妙時序交錯觸發的缺陷，在每日運行的 44,000 個傳統單元測試中完全隱形。
The Merge 最終在 2022 年 9 月順利完成，未發生重大事故，成功將以太坊網路的能源消耗降低 99.95%。時至今日，以太坊基金會仍持續依賴 Antithesis 測試後續更新。2023 年初以太坊主網短暫出現無法最終確認交易的異常時，開發團隊利用 Antithesis 在確定性環境中完美重現了該狀態，加速了修補流程。
另一個代表性案例是 MongoDB。這家全球廣泛使用的 NoSQL 資料庫，將 Antithesis 應用於 8 種不同的複雜叢集拓撲結構，涵蓋多重分片叢集、副本集，以及跨版本的升級與降級情境。統計數據很直接：每 2,500 小時的模擬測試逼出 1 個極度隱蔽的深層 Bug；相當於 100 天生產環境壓力的驗證，能濃縮至 100 小時完成。最顯著的改善在除錯效率：過去追查多節點時序交錯引起的 Bug，需要數名高級工程師耗費數週；在時光旅行除錯器輔助下，平均修復時間壓縮至 3 天以內。MongoDB 自 2021 年起將對 Antithesis 的投入規模增加了三倍。
馬克碎念
確定性的產品化，才是真正的突破
確定性模擬測試的概念並不新。FoundationDB 在十多年前就內部使用了這套方法，AWS 用 TLA+ 做形式化驗證也行之有年。但這些實踐有一個共同的瓶頸：它們要求使用者具備極高的系統底層知識，且通常深度綁定在特定的技術棧中。Antithesis 做的事情，是把「確定性」從一種只有頂尖團隊才能自建的能力，變成一個任何團隊只要提供 Docker 映像檔就能使用的雲端服務。
這跟雲端運算的歷史邏輯一致：最有價值的基礎設施創新，往往不是發明新概念，而是把原本只有少數公司能負擔的能力民主化。AWS 沒有發明伺服器虛擬化，但它讓任何新創公司都能用信用卡租到 Netflix 等級的基礎設施。Antithesis 走的是類似的路徑，只是它民主化的對象是「軟體可靠性的上限」。
AI 寫程式的時代，驗證比生成更值錢
隨著大型語言模型的編寫程式能力成熟，軟體開發正在快速邁向「代理式開發」與「Vibe Coding」的新階段。程式碼的產出速度將爆發性增長，人類開發者的角色會從「寫程式」轉向「審查與架構設計」。但 AI 生成的程式碼有一個根本弱點：它擅長產出語法正確的程式碼區塊，卻缺乏對分散式系統全域狀態與並發安全性的深刻理解。
Jane Street 的工程師點出了一個關鍵觀察：代理式編程工具面臨的最大瓶頸，在於「難以建立對 AI 所做修改的信心」。Antithesis 的 “AI Testing AI” 閉環架構，恰好填補了這個信任缺口。當 AI 代理產出新的微服務代碼，平台可以直接將其載入 Determinator 中，用強化學習引擎在多重宇宙中進行窮舉式驗證。只有通過極端混沌攻擊仍不崩潰的程式碼，才被允許進入生產環境。在 AI 生成程式碼越來越容易的趨勢下，能夠大規模驗證程式碼品質的基礎設施，其戰略價值可能會超越生成工具本身。
回看台灣
台灣的金融機構在分散式架構的複雜度上，與 Jane Street 或以太坊生態存在明顯的量級差距。多數銀行核心系統仍以主機架構為主，微服務化的程度有限，短期內不太會遇到需要在微秒級時序中抓競爭條件的場景。
但兩個趨勢值得留意。第一，隨著開放銀行政策推進與跨機構 API 串接增加，系統間的互動複雜度正在上升，整合測試的覆蓋率缺口會逐步擴大。第二，台灣的區塊鏈新創與 DeFi 開發者，面臨的智慧合約安全挑戰與全球同行完全相同，Antithesis 在以太坊生態中的實戰成果對這個族群有直接的參考價值。
比起直接採購 Antithesis（對多數台灣團隊而言，規模與預算未必匹配），更實際的啟示是理解確定性模擬測試的思維方式：在測試環境中追求可重現性、用屬性斷言取代逐案測試腳本、把「找 Bug」的過程從人力密集轉向自動化。這些原則不需要一台確定性虛擬機，也能在日常的軟體開發流程中落地。