Erik Meijer 的 “In Code They Act, In Proof We Trust” 是当天最硬核的一场。他把 agent 安全从 prompt、policy 和 “模型应该学会对齐” 拉回 proof。
原视频：https://www.youtube.com/watch?v=htM02KMNZnk
能回答和能行动不是一回事
Erik 从 2022 年 11 月 ChatGPT 的出现讲起。那一天之后，人第一次可以自然地对电脑说话，让它总结邮件、回答问题、写文本。这个看似简单的函数，可以理解成 question in、answer out。
问题是，LLM 并不会天然区分代码、数据、指令、意图。只要它能读文本，就可能把不该当指令的东西当成指令。这就是 prompt injection 这类问题的根源。
当 agent 只是回答问题，错误还能被人拦住。可一旦 agent 能行动，风险就变了。它可能发消息、改数据库、调用 API、触发付款、删除资源。执行是不可撤销的，不能只靠模型 “看起来会安全地做”。
proof-carrying code 的旧思想重新有用
Erik 讨论 Lean、Dafny、proof-carrying code、taint analysis 等方法。核心思路是：agent 不只提交要执行的动作，还要提交机器能检查的证据。
如果一个 agent 要执行某个 plan，它应该证明这个 plan 不会把不可信输入带到危险操作里。proof 的价值在于，它不要求你相信模型。你只需要检查证明是否成立。
他也指出了困难。某些 proof 如果落到 IO 这种黑盒类型里，意义会变弱。Lean 这样的系统有强约束，但工程实践里要把这些理论接到真实 agent harness 上，并不简单。
软件工厂越自动化，proof 越重要
这场和 Derek Nee 的 proof ledger、Karpathy 的 verification、Kyle 的 control loop 是一条线。agent 越能行动，证据就越重要。没有 proof 的 agent，只是更快的权限风险。
很多团队现在把安全寄托在 prompt 上：告诉 agent 不要做坏事，告诉它遵守规则。这个层面有用，但不够。模型会误解，会被注入，会为了完成目标绕过限制。
Erik 给的方向更工程化：把不可让渡的安全条件做成机器可检查的东西。能静态检查就静态检查，能 taint analysis 就 taint analysis，能把 proof 放到执行前就不要等事故后复盘。
我的理解是，software factory 里的 “factory” 如果没有 proof，只是把危险动作规模化。真正能放心自动化的前提，是系统能在行动前拒绝不安全计划。
prompt injection 不是小漏洞
Erik 从 LLM 的基本形态讲起：question in、answer out。这个函数看似简单，但它把自然语言、代码、数据和指令混在同一个通道里。prompt injection 之所以麻烦，是因为模型很难天然分清“这段文本是在描述指令”还是“这段文本就是指令”。
当模型只回答问题时，这个风险已经存在；当它变成 agent 能行动时，风险就放大了。它可能把网页里的恶意内容当成用户命令，可能把不可信数据带到危险 API，可能为了完成任务越过安全边界。
所以这不是靠提醒模型“请安全”就能解决的问题。安全条件必须从自然语言愿望变成机器可检查规则。
proof 的价值是缩小信任边界
Erik 讲 proof-carrying code、taint analysis、Lean、Dafny，本质都是一件事：不要相信执行者本身，要相信可检查的证明和小而可信的 checker。
如果 agent 要执行一个计划，它不仅要说“我认为这安全”，还要给出“为什么安全”的形式化证据。系统只需要检查证明，而不是完全信任模型的判断。
这会把信任边界前移。危险动作不是执行后再审计，而是在执行前被拦住。对于删除数据、付款、发邮件、改生产配置这类不可逆动作，这个差别非常大。
proof 不是所有场景的答案，但会成为高风险动作的门槛
我不认为所有 AI 操作都要形式化证明。让 agent 改一段文案、生成一份摘要，不需要上 Lean。但高风险动作不同：生产数据库、权限系统、资金流、用户隐私、供应链脚本，这些地方必须有更强 gate。
Erik 这场的长期意义，是把软件工厂的安全标准从“相信 agent 会遵守规则”提升到“让系统拒绝无法证明安全的计划”。自动化越强，这条线越重要。
来源与说明
本文基于 AI Engineer World’s Fair 2026 Day 1 主舞台视频转录、官方日程信息，以及本地 AI engineering 知识库整理。文章不是逐字稿，而是按单场分享的主线、上下文和工程启发重写。
评论前必须登录！
立即登录 注册