用机器可验的证明约束Agent执行
AI Engineer · youtube · 2026-07-14
这是一场关于 AI agent 执行安全的演讲，核心观点是：**让 agent 先给出可机器验证的安全证明，再允许它执行动作**。 要点包括： - 现实里已经出现多种 agent 失控案例，例如聊天机器人误同意低价卖车、编码 agent 误删生产数据库、技能安装 keylogger 等； - 这些不是边缘事故，而是“允许无机械保证的行动”必然带来的失败模式； - 由于执行是不可逆的，错误动作的代价远高于拒绝一次安全动作，因此系统设计上应把信任边界前移； - Automind 是一个 agent harness：执行前必须提交计划与用 Universalis 写出的、可机器检查的安全/正确性证明； - 由一个小而可审计的 checker 决定是否允许执行，系统只信任 checker，而不是 agent 的口头承诺或自然语言 proof。 视频还介绍了 Erik Meijer 的背景，以及 Universalis 的定位：把形式化验证与 LLM 结合，目标是让 agent 系统更透明、可控，适用于真实世界的知识工作。