研究人員提出了一種新的代數語義框架，用於形式化定義和驗證受控執行。該框架透過三個核心公理——安全性、透明性和恰當性——來公理化控制的概念，並證明這些公理能夠誘匯出一個對稱么半範疇，其中所有張量組合都保持控制性質。這一成果為受控執行提供了堅實的數學基礎。
這項工作在Rocq證明助手中進行了機械化實現，包含32個模組、約12000行程式碼和454個定理，且沒有任何未證明的假設。框架的基礎是互動樹和引數化共歸納，這使得可以對無限行為進行推理。代數效應系統進一步限制了處理器代數，確保只有保持控制的處理器可以在安全片段中構造，而空能力集的程式僅能發出可觀測性指令。
能力索引的組合機制允許程式攜帶機器檢查的能力界限，提供了一個雙重保證定理：在所有組合運算元下，within_caps（能力邊界內）和gov_safe（控制安全）同時成立。該工作的核心結果是共同邊界定理：在形式模型中，每個透過四個原始態射構造子表達的程式在解釋下都是受控的，反之，每個受控程式都可以表示為這樣一個程式。
值得注意的是，受控內部保持了圖靈完備性，但無中介I/O被排除在受控片段之外。控制拒絕被建模為安全的共歸納發散。該控制代數是引數化的，任何系統只要例項化三個公理，就能自動繼承所有派生性質，包括收斂性、組合封閉性和目標保持性。
為了驗證實用性，研究人員從形式規範中提取了OCaml程式碼，並將其作為本地實現函式（NIF）整合到BEAM執行時中。透過屬性基測試，使用超過70000個隨機輸入，規範與執行時直譯器之間未發現任何分歧，從而確認了行為等價性。這項研究為構建安全、可驗證的受控執行系統提供了堅實的理論基礎和實用的驗證手段。