随着AI代理系统越来越多地执行而非仅提供建议，确保其行为的正确性变得至关重要。特别是在AI代理查询受监管的数据、调用具有影响力的工具并修改持久状态时，单凭终端输出的合理性无法保证正确性。关键问题在于：每一步是否在合同下获得授权？记录的历史是否具有防篡改性？轨迹能否被确定性地重构？我们将这一过程形式化为运行时执行证明（PoE）。
一个执行被定义为三元组 $x = (C, T, R)$：合同 $C$、执行因果事件流（ECES） $T$ 和重放上下文 $R$。我们通过良构性谓词和五个可验证的不变性来构成PoE的有效性谓词。这五个语义保证描述了授权、路径合规、拒绝时的无效效果、历史完整性和重放性。我们在明确的密码学和部署假设下证明了声学性：任何生成违反语义保证的PoE有效执行的PPT攻击者都会导致签名伪造、哈希碰撞或量化的部署失败事件。
主要执行模型（PEM）将规划、执行、效果和记录分离到不同的权威平面；一个引理将轨迹完整性简化为效应器专属凭证的认证。只有当PoE = 1时，执行证明证书（EAC）才会被发放。在一个单节点的TypeScript原型中，PoE在最小流上增加约2.7毫秒的延迟，并在并发批处理工作负载上增加4.4%的开销；一个标准的八事件轨迹压缩到约1.1 KB；注入的网关绕过和轨迹篡改攻击被拒绝。PoE并不替代共识、TEE或zkVM，而是将授权、效果、历史和重放绑定成一个单一的可运行时检查的对象，使得治理执行在合同下成为可证明的。