研究者らは、統制実行を形式化するための新しい代数的意味論フレームワークを提案した。このフレームワークは、安全性、透明性、適切性という3つの中核公理によって統制の概念を公理化し、これらの公理がすべてのテンソル合成で統制特性を保存する対称モノイダル圏を誘導することを証明している。この成果は統制実行に強固な数学的基盤を提供する。
この研究はRocq証明アシスタントで機械化されており、32モジュール、約12,000行のコード、454の定理から構成され、未証明の前提は一切ない。フレームワークの基盤は相互作用木とパラメータ化された余帰納法であり、無限の振る舞いの推論を可能にする。代数的効果システムはさらにハンドラ代数を制約し、安全な断片内でのみ統制を保存するハンドラの構築を許可する。空能力集合を持つプログラムは、観測可能性ディレクティブのみを発することができる。
能力インデックス付き合成メカニズムにより、プログラムは機械検査された能力境界を持つことができ、二重保証定理が提供される。すなわち、すべての合成演算子の下で、within_caps（能力境界内）とgov_safe（統制安全）が同時に成立する。この研究の核心結果は共終境界定理である。形式モデル内では、4つの原始射構成子を介して表現可能なすべてのプログラムは解釈下で統制され、逆にすべての統制プログラムはそのようなプログラムの像として表現できる。
特筆すべき点として、統制内部でチューリング完全性は保存されるが、仲介なしのI/Oは統制断片から除外される。統制拒否は安全な余帰納的発散としてモデル化される。統制代数はパラメトリックであり、任意のシステムが3つの公理をインスタンス化すれば、収束、合成的閉包、目標保存を含むすべての派生特性を自動的に継承する。
実用性を検証するため、形式仕様からOCamlコードを抽出し、BEAMランタイムにネイティブ実装関数（NIF）として統合した。プロパティベーステストにより、70,000以上のランダム入力を用いて仕様とランタイムインタプリタの間で矛盾がないことが確認され、行動等価性が実証された。この研究は、安全で検証可能な統制実行システムを構築するための強固な理論的基盤と実用的な検証手段を提供する。