研究人员提出了一种新的代数语义框架，用于形式化定义和验证受控执行。该框架通过三个核心公理——安全性、透明性和恰当性——来公理化控制的概念，并证明这些公理能够诱导出一个对称幺半范畴，其中所有张量组合都保持控制性质。这一成果为受控执行提供了坚实的数学基础。
这项工作在Rocq证明助手中进行了机械化实现，包含32个模块、约12000行代码和454个定理，且没有任何未证明的假设。框架的基础是交互树和参数化共归纳，这使得可以对无限行为进行推理。代数效应系统进一步限制了处理器代数，确保只有保持控制的处理器可以在安全片段中构造，而空能力集的程序仅能发出可观测性指令。
能力索引的组合机制允许程序携带机器检查的能力界限，提供了一個双重保证定理：在所有组合算子下，within_caps（能力边界内）和gov_safe（控制安全）同时成立。该工作的核心结果是共同边界定理：在形式模型中，每个通过四个原始态射构造子表达的程序在解释下都是受控的，反之，每个受控程序都可以表示为这样一个程序。
值得注意的是，受控内部保持了图灵完备性，但无中介I/O被排除在受控片段之外。控制拒绝被建模为安全的共归纳发散。该控制代数是参数化的，任何系统只要实例化三个公理，就能自动继承所有派生性质，包括收敛性、组合封闭性和目标保持性。
为了验证实用性，研究人员从形式规范中提取了OCaml代码，并将其作为本地实现函数（NIF）集成到BEAM运行时中。通过属性基测试，使用超过70000个随机输入，规范与运行时解释器之间未发现任何分歧，从而确认了行为等价性。这项研究为构建安全、可验证的受控执行系统提供了坚实的理论基础和实用的验证手段。