约束验证：独立于对齐的 AI 安全保证

智能体框架是 AI 智能体与世界互动的软件层。现有安全方法通过干预模型实现，依赖于不可验证的学习行为属性。我们引入约束验证技术，将安全保证定位于智能体框架本身。基于混乱预言机语义，AI 被建模为在整个类型动作空间中不受约束的预言机，而经过约束的验证层必须对每一种可能的 AI 输出强制执行边界策略。对于以边界事件、动作参数和状态为表达式范围的可边界可 enforce 属性，我们通过前向仿真细化证明普遍保证，并在 Dafny 中实现其机械化。我们通过验证一个极简智能体 LLM 框架 PocketFlow 来实例化该范式，并使用智能体合成管道在信息屏障下生成规范、操作模型和细化证明，以避免自矛盾规范。迄今为止，这是对智能体框架进行的首个演绎形式验证，其保证对建模的类型动作边界而言具有不变性。