形式化定理的工程翻譯
論文 §4.4 給出 6 條核心元理論定理。這裡不列證明，只把每條定理翻譯成「對真實 Agent Runtime 意味著什麼」。理解 Confluence 是理解整個論文價值的關鍵。
六條定理工程翻譯表
【論文原文結論 §4.4】
| 定理 | 章節號 | 工程翻譯 |
|---|---|---|
| Preservation（Thm 59） | §4.4.1 | 任何規則應用後 registry 仍然 well-formed：parent 指標落在 registry 內、不同 fiber 的 provision 不相交、committed view 只指向 installed fiber。工程意義：執行時永遠不會出現「懸空 fiber 參考」或「兩個插件同時聲稱自己提供 'database'」的狀態。 |
| Recovery Exactness（Thm 61） | §4.4.2 | 在 pairwise independence 假設下，對一個 fiber n 的 episode [b, u]，應用其 accumulator 等於「從未載入過 n」時的狀態（up to control fields）。工程意義：卸載一個插件後，環境狀態等價於它從未存在過——這對 HMR、插件熱替換至關重要。 |
| Ordering（Thm 63） | §4.4.3 | Provider 必須先於 Consumer 啟用、晚於 Consumer 卸載；Consumer 在整個 episode 中讀到的依賴解析（committed view）不變。工程意義：連線池關閉前所有 connection 已歸還；資料庫關閉前所有事務已提交；沒有「race condition 導致 consumer 讀到半關閉的 provider」。 |
| Resolution Coherence（Thm 64） | §4.4.3 | 一個 transition 的所有 iteration 都跑在同一份 committed view 下；若中途 target 變化，要麼完成轉入 Active，要麼經 L-Divert/L-Raise 進入 Unloading 並完全回滾。工程意義：非同步載入元件時不會「半舊半新」——不會一部分 effect 用舊依賴、另一部分用新依賴。 |
| Progress（Thm 66） | §4.4.4 | 在 ≺ acyclic、len(e_n) ≤ K、fiber 名有限的前提下，non-quiescent 狀態必有規則可施，且每個 fiber 的 step 數有界。工程意義：系統不會死鎖（guard 一定會釋放）；每次設定變更最終會達到穩定狀態。 |
| Confluence（Thm 73） | §4.4.5 | 在 pairwise independence、component total on provision、no failure 假設下，無論經過多少次載入/卸載/替換，只要最終設定相同，穩定狀態等價於按最終設定從零啟動一次。工程意義：動態歷史不留痕跡——一個 Agent 經過反覆替換自己元件後，等價於一次性啟動最終設定。這是「自演化 Agent」的理論基石。 |
Confluence：動態歷史不留痕跡
Confluence 是這套理論的高潮，值得單獨展開。
直觀表述：系統經過任意次數的動態載入、卸載和替換後，只要最終設定相同，其穩定狀態應等價於按照最終設定從零啟動一次得到的狀態。
對一個自演化 Agent 來說，這意味著：假設 Agent 在運行過程中先後替換了工具 A 三次、卸載並重裝了 Skill B 兩次、調整了子 Agent C 的隔離 realm，只要它最終的元件設定與「某次乾淨啟動」相同，那麼執行時的穩定狀態（哪些元件啟用、各自的 committed view、累積的環境狀態）就等價於那一次乾淨啟動。動態歷史不留下任何痕跡。
這是其他 DI/HMR 框架都沒有的保證：
- 傳統 DI 不支援執行時替換，無 Confluence 可言；
- HMR 需要開發者手寫狀態遷移函式，遷移是否正確沒有形式化保證；
- 容器編排「重啟即乾淨」是粗粒度丟棄全部狀態，不是同粒度的等價。
【論文原文結論 §4.4.5】注意 Confluence 的前提：
- pairwise independence：effect 彼此獨立或可交換（Def 19）；
- component total on provision：每個 component 實際安裝它宣告的所有 key（Def 69）；
- no failure：排除 failure 場景。
【論文原文結論 §4.4.5】Confluence 排除了 failure 場景（§4.3.4 的 L-Raise）——因為 failure 是真實分歧源：一個 schedule 可能 fail 另一個可能 succeed，但 Cor 62 保證 failed fiber 對 state 的貢獻為 0（失敗元件的副作用被完全回滾，不影響其他 fiber）。所以「失敗」不破壞狀態一致性，但確實讓兩條動態路徑產生分歧（一條有失敗、一條沒有）。
這套證明不能保證什麼
【論文原文結論 §6.1, §6.3】形式化證明只覆蓋透過 Context 管理的副作用。它不保證：
- 開發者寫的 inverse 一定正確（witness 條件
g(δ)=γ是義務不驗證）； - Context 之外的副作用（直接改全域變數、檔案、資料庫、外部系統）能被撤銷；
- 外部 emission（網路請求、訊息、郵件、支付）能自動回滾——這些一旦發出就跨出系統邊界；
- 不可信插件的安全性——Context 級權限控制不能替代行程/容器/WASM sandbox；
- failure 場景下的 Confluence（明確排除）；
- 依賴 key 的版本相容與結構相容（§6.6 open problem）。
詳細前提與局限見 局限與綜合評價。這套理論如何落到 DeepSeek Harness 上見 與 DeepSeek Harness 的關係。