徐天音谈 Agent 时代的系统：形式化验证从五年压到五小时、"把 agent 当用户，系统一定挂"（月球大叔，2026-08-22）¶

嘉宾: 徐天音（Tianyin Xu）（UIUC 终身教授，系统方向；现于 UC Berkeley Sky Lab 学术休假）
主持: 月球大叔
来源: YouTube · 118 分钟
转录稿: sources/uncle-moon/20260822-N0QfgZsDBv8（英文人工上传字幕）

说话人认定依据：⚠️ 本期的转录稿是本库目前归属条件最差的一份——它是人工上传的英文字幕，既没有姓名标签，也没有 >> 分隔符，两人的话连成一段连续散文；且它显然是中文对话的英文译稿，留有大量翻译痕迹（同一句话以两种措辞重复出现、中英混杂的残句）。

本页归属只能靠"提问 vs 回答"的语义结构： - 开场 [00:00:15] 主持人自报"在硅谷采访 100 个有意思的人，这里是月球大叔，今天的嘉宾是 UIUC 终身教授徐天音"，嘉宾答谢——这是全片唯一的机械锚点。 - 其后凡提问、复述、总结与"我完全同意"类表述归主持人；凡长段的经历叙述、技术解释与判断归徐天音。

⚠️ 本页凡引用主持方处写明"月球大叔"，其余默认为徐天音。少数两人交替密集、且译稿把同一句重复了两遍的段落，本页只取语义明确的部分。

专名与转录对照（转录稿拼写 → 本页采用）：Stephen Savage → Stefan Savage（UCSD 安全研究者，⚠️ 疑似，本库不确证）、Siri task → SRE task、SkyLab → Sky Computing Lab（Berkeley）、TLAPS → TLA+ Proof System、ZAB → ZooKeeper Atomic Broadcast、Gu AIling → 谷爱凌、ROC → Recovery-Oriented Computing。

⚠️ 以下明确不裁决，照录存疑： - YY / Wai Wai（[00:06:18] 起）：他的 UCSD 博士导师。线索有三条——创办过三家公司且都相当成功、此前在 UIUC 任教七年、做系统方向。本库不替他认定这是谁。 - Juncheng / Professor Juncheng（[01:29:06]、[01:41:19]）：月球大叔引用的一位此前上过节目的教授（关于"博士去工业界实习不该做研究"与"要多读计算机历史"）。疑为江鋆晨，但拼写对不上，本库不确证。 - Fibonacci is not correct, not 4.4, 4.6, 4.8（[01:03:52]）：一段关于模型版本号的残句，语义不可辨，本库不猜。同段的 GPT-5.6 Soul 同样不裁决。 - Wang Hong and Deng Yu won the Fields Medal（[00:33:34]）：他提到"前几天"有两位华人数学家获菲尔兹奖。本库照录他的表述，不作为事实性记录。 - Markus / Stephan（[00:21:25]）、Ruizé（[01:11:55]）、Xudong（[01:41:19]）：TLA+ Foundation 的成员与他的两位学生，照录名字，不补全。 - system's convexity（[00:20:25]）：语义不明，不猜。

概要¶

这是本库第一份来自学术界系统研究者的完整材料。此前本库的系统/基础设施来源全部是从业者——游凯超与 Simon Mo（vLLM）、朱邦华（SGLang）、江鋆晨（LMCache，虽是教授但以创业者身份出现）、Baseten 团队、肖志斌（芯片架构）。徐天音是唯一一个从"系统研究"这个学科本身出发谈 agent 时代的人，而且他给出了本库迄今关于 AI 改变一项研究工作的最具体的一组数字。

最该被单独引用的八条：

⚠️ 形式化验证：五年 → 五小时（[01:11:55]–[01:12:55]）。AI 之前，一位后来去 Microsoft Research 的学生花了整整五年，才把 ZooKeeper 及其共识协议 ZAB 做成可以跑模型检查的 TLA+ 形式模型。现在这件事变成五小时。 原因：前沿模型写 TLA+ 已经像写 C 或 Python 一样熟练，而且它已经学过这些开源系统的全部源码。
⚠️ 但被自动化掉的是学习成本，不是判断（[01:12:55]–[01:13:55]）。真正难的是"到底该建模什么、不该建模什么"——全都建模，模型会大到跑不动形式化；建得太简单，又发现不了任何问题。这件事过去靠老手经验或天才学生的直觉，现在交给 AI，理由是"一个成熟的开源项目走过很多年，AI 其实知道哪些地方 tricky、哪些地方历史上从没出过问题"。
⚠️ "把 AI agent 当用户，系统一定会挂"（[00:19:23]）。他把这条直接接在自己 2013 年那篇 "Do Not Blame Users for Misconfigurations" 上——当年的论点是"如果很多用户都犯同一个错，那是系统设计的问题，不是用户的问题"；现在用户换成了 agent。
⚠️ 他给的 reward hacking 一手证据，本库认为是本期最硬的一段（[00:20:25]–[00:21:25]）：他们和 TLA+ Foundation 合作做 benchmark，让 agent 给协议写正确性证明。TLA+ 的工具链极其成熟，人写了大量证明从没碰到过怪问题；但把 agent 放进去，它写出各种看起来证完了、实际上不成立的证明。结果是 TLA+ Foundation 的人开始修一批他们从来没想过的 bug——全部由 AI 的 reward hacking 逼出来。
⚠️ 他对"形式化验证能不能救 AI 写的系统"给了一个否定性的限定（[01:22:02]–[01:23:03]）。月球大叔直接问了本库认为全期最好的问题：既然形式化验证已经从五年压到五小时，为什么还有人说 AI 建系统的最大问题是可靠性和安全？他的回答是——"即使你能形式化验证，它也只告诉你代码与你要的 spec 一致，仅此而已。但'你到底需要什么样的系统、你的 spec 是什么'，这件事很难靠 AI 解决。"
⚠️ SREGym 的一年期对照，本库认为是本库迄今最锋利的一条 benchmark 饱和数据（[01:02:52]–[01:03:52]）：他们的 SRE benchmark 含 102 个真实运维场景，一年前 agent 只解出 11.4%；他说用今天的模型重跑，"我认为会接近 90%"。
⚠️ 可靠性与安全第一次成为能拿到资源的方向，而原因是 agent（[01:31:10]–[01:32:12]）："二三十年来可靠性和安全从来不是 first-class 原则，因为它们不挣钱，只有性能挣钱"；企业过去靠买保险和写测试用例来处理。"但 agent 把这件事翻过来了"——当 agent 主导写代码，可靠性与安全成了最大问题，而这不是靠堆测试用例能解决的。
⚠️ 他把 2000 年前后的 ROC（Recovery-Oriented Computing）整个翻了出来，并主张直接复用到 agent 上（[01:24:06]–[01:30:07]）：ROC 的实证发现是系统故障最大的一块来自人的操作失误，不是硬件；它提出的两个想法——system-wide undo 与 microreboot——前者当年难以推广、后者今天已经活在微服务与 serverless 里。他的主张是在 agent 时代把这些经典原则重新拿出来用。

核心观点¶

一、"把 agent 当用户"：他把十年前的论文接到了今天¶

十年前那篇的论点（[00:15:21]–[00:19:23]）：论文题目是 "Do Not Blame Users for Misconfigurations"。当年工程师遇到配置错误的标准反应是"这是用户操作失误"，而他的论证是——如果很多用户都没意识到问题、都犯同一个错，那可能是系统设计本身有问题。
他举的那个工业界案例（[00:16:21]–[00:17:21]）：一个用户只是把名字里的字母大写了，结果走了 75 轮沟通、收集了 10 份日志。为什么这么痛苦——那是一家存储公司，卖的是软硬件打包的存储盒子；产品出问题时客户没法把盒子寄回来，更没法把数据寄回来（数据是机密的，客户是政府机构或银行）。所以诊断只能靠客户给的零碎信息去猜。他的总结是："根因可能非常简单，但一旦出故障，这就变成一个极其昂贵、极其耗时的过程。"
产出：他们发现了 743 个配置错误问题，其中大量被开发者确认并修复。
⚠️ 但他自己对"找 bug"这件事的评价出人意料（[00:17:21]–[00:18:22]）："我从来不觉得找 bug 有多激动人心，因为工业界的 bug 太多了——多到人根本修不完。所以多找几个 bug，对我来说不太有意义。" 他认为这篇论文更有价值的部分是告诉开发者（尤其是开源开发者）：你设计系统时必须想清楚用户会怎么用它。
他引以为意义的一个瞬间（[00:18:22]–[00:19:23]）：系里的安全研究者 Stefan Savage（⚠️ 姓名疑似）主持的 seminar 上，一位学生提议用机器学习检测配置错误；Savage 的即时反应是——"为什么不把系统做对？为什么不做徐天音做的那件事，那样你就不需要机器学习来找这些问题了。" 他说这种重构问题的方式可能改变别人怎么看这个问题。
⚠️ 月球大叔接上的那一问是本期的转折点（[00:19:23]）：当年是设计糟糕的系统让人用出问题，现在用户是 AI agent——如果系统仍然只为人类用户设计，agent 必然会犯错。那么面向 agent 的系统是否需要重新设计？
他的回答（[00:19:23]）："绝对需要。现在大家都在谈 AI-native 系统，但很多现有系统根本不是为 AI agent 这个用户设计的。把 agent 当用户，系统一定会挂。"
⚠️ TLA+ 那个 benchmark 的观察（[00:20:25]–[00:21:25]）：见概要第 4 条。他给的机制解释很干净：

人写证明时是真的想证明这个协议是对的；AI 并不真的想证明协议是对的，AI 只想通过这个证明系统。
他的结论（[00:21:25]）："一旦 AI agent 成为用户，所有系统都应该重新思考怎么处理这个接口。"
月球大叔的补充观察（[00:21:25]）：硅谷越来越多公司开始投入为 agent 重新设计接口——agent 怎么登录、怎么保证安全、怎么操作。

二、为什么他认为这对系统研究是一次结构性机会¶

⚠️ 第一条：重设计的成本终于有人愿意付（[00:21:25]–[00:22:26]）："过去你想从根本上重新设计一个系统，成本很高，不是所有人都愿意投。现在人们愿意考虑这件事，并且觉得有必要重新设计系统。"
月球大叔给的行业侧解释（[00:22:26]）：系统行业一直得跟在产品和算法后面——"如果你跑得太前，做出一个无法大规模部署应用的系统，它其实没有价值，ROI 太低"。而AI 的快速发展凭空造出了无穷多的新的重大需求。
⚠️ 第二条：评价标准变了（[00:22:26]–[00:23:26]）：他说这条是系统研究者的时代机会——

过去你做一个系统，说它很好，但它只能处理一类 workload，很难拿到资助、很难说服评审；评委一定会以"不够通用"拒掉你的论文。现在，我就做一个 IO 性能特别好的系统，很多人就会很兴奋，它的经济市场特别大。
他举的窄而深的例子（[00:23:26]）：只做"agent 怎么登录"这一件事——"看起来很小，但因为他考虑了各种 agent 可能的 reward hacking 与攻破这个系统的方式，他把它做得非常扎实，这样你就能保证整个系统对用户的安全"。

三、AI 当 SRE：他说能力不是问题，成本和"谁来指导"才是¶

他对当前前沿模型的评价很高（[00:58:50]–[00:59:50]）："基本上任何系统任务，如果你告诉 AI 怎么做这个任务，AI 基本都能做。" 所以"AI 能不能做"不是问题——

关键问题是你怎么去做，以及成本是多少。
⚠️ 人的角色他说得很具体（[00:59:50]–[01:00:51]）："AI 就像一个很聪明的人。假设你公司有极多的人，而且个个都很勤奋，你仍然需要告诉他们什么才是对的事。" 落到操作上就是——给初级工程师示范什么叫好的工作：怎么做、怎么权衡 trade-off、怎么拆解任务再一步步推进，然后让 AI 做重复性的部分。
他给的反面（[01:00:51]）："如果你只给它一个非常模糊的定义或 spec，它其实也能做，但可能需要很多轮迭代，代价会很高。"
⚠️ 由此推出的教育问题，本库认为是本期最该进 AI 与就业的一段（[01:00:51]–[01:02:52]）：既然是有经验、有品味的人去指导 agent，那么——

一个应届生怎么成为这样的人？这个训练与指导的过程没有了，我认为这对当前的 CS 教育是巨大的冲击。
他先给了一个乐观的答案：学生应该用 AI 来做学习和工作——"通过指导 AI 来做这件事，作为学生你就是在练这件事，你用 AI 练你的学习、也用 AI 练你的研究，自然就能到这个水平"。
⚠️ 然后他自己拆掉了这个答案，给了两个问题：
1. 你太 junior——"你的品味和指导可能不够，AI 的输出可能给你一些其实不高质量、不高水平的东西"。
2. 这些岗位越来越少——"原本人是通过一个个小岗位慢慢爬上去的，那个过程让你学会人际沟通、让你提升自己"。
他的结论分两半："人仍然是这里非常重要的一环，我们不该设想一个完全没有人的动作。所以建议、导师这类东西不会被 AI 取代。" 但对第二个问题——"市场萎缩是一个非常真实的问题，但我其实不知道怎么解决这个问题。" ⚠️ 本库认为这处坦白比他的乐观部分更值得记。

四、SREGym：一条锋利的 benchmark 饱和数据¶

是什么（[01:02:52]）：一个让 AI agent 处理站点可靠性问题的环境，含 102 个真实世界的 IT 运维场景。
⚠️ 数字（[01:02:52]–[01:03:52]）：一年前 agent 只解出 11.4%；他说用今天的模型重跑"会接近 90%"。月球大叔问"一年就这么大进步？"，他答"是的，就一年"。
他的补充：⚠️ 这个项目是学生主导的，"我没有发起它，不能全算作我的工作"。
他给的能力跃迁时间点（[01:03:52]）：2025 年底到 2026 年初有一次本质性的飞跃；今年最近又出了一批新模型，能力再次提升。此前的限制是推理幻觉很高、上下文不够大。
⚠️ 他对 benchmark 这件事的方法论，本库认为该进评测与基准（[01:04:52]）：

好的 benchmark 是能度量 AI 边界的。AI 很弱时你做一个极难的 benchmark、它一个都做不出来，这个 benchmark 其实不好；AI 很强时它能做 90%，这个 benchmark 也基本没用了。最好的 benchmark 是 AI 能做 30%–40%、剩下 60% 做不了——这样它能持续挑战 AI。
⚠️ 他说真正的挑战不是难度而是保真度（fidelity）（[01:04:52]–[01:06:53]）：
benchmark 本身只能是一个小环境——三个节点、五个节点的系统，跟 Meta 那种超大规模系统差别很大。所以"AI 在这些小环境里很强，但它在那些巨大环境里是不是也强，我认为不一定"。
⚠️ 他把这个困境讲得很干净：从大系统做成小系统，必然要扔掉一些东西。扔掉的如果很重要，这个小模拟器就没用了；但如果你什么都想留，本质上就没法把大系统变小。而你又必须要小的——因为要做 RL，太复杂或在线就做不了。
⚠️ 与 coding benchmark 的对照是本节最有价值的一条（[01:05:52]–[01:06:53]）："coding benchmark 没有这个问题，因为它是离线的——你就不停生成代码。SRE 太实时了：你解决了一个问题之后，它真的解决了吗、真的修好了线上的 bug 吗、反馈是什么？整个反馈过程不是离线的，是在线的。"
他们的做法（[01:06:53]–[01:07:54]）：学校有一个本科生科研项目（REU），今年暑假让本科生去读大公司（如 Cloudflare）公开的故障 postmortem，按描述在相对小的模拟环境里复现那个故障，然后测 AI。发现是：即使在小环境里，相比最基础的故障，这些更真实的故障对 AI 构成的挑战完全不同。
月球大叔的两条外部观察（[01:07:54]–[01:08:55]）：① 学生能在这个过程里提前接触到大公司的真实问题；② 抽象出的模拟器后续可以用来做 RL——而RL 环境/模拟器公司在硅谷极其火热，"任何一个环境，如果能真正帮模型提升能力——之前模型解决不了的问题，在它上面训练之后能解决了——那这个环境就会卖出非常高的价格"。

五、AI + 形式化方法：本期最硬的一节¶

模型检查的本质（[01:08:55]–[01:09:55]）：你有非常细节的底层代码，需要把它写成一个高层抽象，而这个抽象用数学语言描述。他们用的语言是 TLA+（Leslie Lamport 所作）。一旦系统能用形式语言描述，就能做形式化推理，检查 safety（坏事永远不发生）与 liveness（好事最终会发生）。
⚠️ 难点在哪（[01:09:55]–[01:11:55]）：把一个非常底层的系统写成高层抽象——这件事智力上极具挑战，对一个博士生来说可能是四年时间。
AI 之前的成本：一位很有才华的学生（现在在 Microsoft Research）花了整整五年。原因有二——
1. TLA+ 这套形式化的东西任何本科课程都不教，"你可能要花一两年才能把这套东西学透"。
2. 你还得写 specification——形式模型与不变式（invariants）。而"要给一个系统建一个好模型，你必须非常深地理解这个系统，否则你根本抽象不对"。
他们选的系统是 ZooKeeper（共识协议 ZAB）。那位学生必须把 ZAB 的所有细节、以及 ZooKeeper 怎么实现 ZAB 全部搞懂。⚠️ 而且："你的系统在变，代码在变，明天会有新 release。你还得跟着代码的演化去写不同的模型。"
回报："我们解决了这个系统里很多年没被解决的问题。ZooKeeper 里有一个问题，此前很多人研究过、非常复杂，但通过形式化推理，它能清清楚楚告诉你到底发生了什么。"
⚠️ 然后是那句对照（[01:11:55]–[01:12:55]）：

五年的工作变成了五小时。

原因：AI 不需要从头学这些形式化的东西，它已经学过了——"现在前沿模型写 TLA+ 写得非常好，就像写 C 或 Python 一样熟练"；而且AI 对系统本身有很深的理解，因为它已经学过全部源码，"你再把代码给它，它立刻就能从中学习"。
⚠️ 但他立刻指出被自动化掉的是什么、没被自动化掉的是什么（[01:12:55]–[01:13:55]）：
没被自动化掉的是"最智力性的那部分"——到底怎么建模这个系统。
两难："如果你还抱着什么都想留的想法，最后你根本建不出这个模型，因为模型会大到没法做形式化的事情。但模型太简单，你又什么问题都发现不了。"
过去靠什么：老手的经验，或者一个非常有天赋的博士生的直觉与聪明。
⚠️ 现在他们把这件事交给 AI，理由值得完整记一次： > 一个成熟的开源项目走过很多年，AI 其实知道哪些部分 tricky、哪些部分不太可能出问题。于是我们就告诉 AI：根据你的经验，这类代码很难、很容易出错，你要更仔细地建模；那个地方历史上可能从来没出过问题，你就不用建模，直接抽象掉。AI 做这件事做得非常好。
⚠️ 他同时指出 AI 干这件事的那个坑（[01:14:56]）："AI 不是人，它可能 reward hacking。它能产出一个看起来正确、但不是你要的模型。所以你需要办法去引导甚至约束 AI，防止 reward hacking，帮它一步步理解这个系统。"
为什么选模型检查而不是证明（[01:18:59]–[01:20:00]）："模型检查相对便宜，而且能立刻得到反馈"；他们当时想做一个工具，所以"模型检查比做证明更实用，至少在当下"。但"我们也想做一些证明，为将来做点投入"。
⚠️ 成本数据点，本库认为这是本期最该被引用的一个具体数字（[01:17:59]–[01:18:59]）：用 TLAPS（证明）去跑一个 ZooKeeper 的 system spec（⚠️ 描述系统而非描述协议的 spec，所以层次相对低），花了 2000 美元、跑了 5 天。他的评价是"我觉得这还是相对昂贵的一件事"。
⚠️ 他对"形式化方法为什么一直没在工业界普及"的解释，以及经济学翻转（[01:14:56]–[01:15:57]）：
形式化方法本身已经存在几十年。⚠️ 他借此说了一句关于基础研究的话："我们今天能跑这么快，是因为早先的研究者把地基打好了，路已经在那儿。"
没被广泛采用的原因是成本——它需要高度专门化的专业能力，因而昂贵，且不符合硅谷"move fast and break things"的文化。
⚠️ 但在 NASA 那里完全说得通："把飞船送上火星然后它挂了，代价极其高昂。他们甚至避免写多线程代码，因为并发太难——他们写单线程代码，并在部署到 Mars Pathfinder 这类任务之前做形式化验证。"
⚠️ 落点："一旦 AI 把形式化验证自动化，经济账就完全变了。"
⚠️ 他对"调试 vs 验证"的区分（[01:16:59]）："调试是被动的——出了问题你才去调。但我们的梦想是让故障根本不发生。如果能形式化验证整个系统，那一类故障就不可能发生——我们从数学上证明了系统不会遭遇我们针对的那个故障。"
⚠️ "买保险"这个框架，本库认为是本页最好的一个经济学类比（[01:16:59]–[01:17:59]，由月球大叔起头、他接上）：

过去通过失败来学习更便宜：把系统部署上去，然后买保险。如果故障十年才发生一次，就买一份大额保单，真出事让保险公司赔。而现在，你不需要买保险了——一份形式化证明可以保证这类故障十年、甚至一百年都不会发生。
历史上谁在投（[01:17:59]–[01:18:59]）："AI 时代之前最热心的、现在仍然最热心的是微软，因为他们有 Azure，可靠性非常重要。然后是 AWS。基本上就这两家在养团队。" ⚠️ "但有了 AI 之后，这个门槛变得很低，很多人都能做这件事了。"
⚠️ SDD（specification-driven development）（[01:20:00]–[01:21:02]）："你先写一个形式化的 spec，然后每次让 AI 写东西，你都能证明或验证你写的代码满足这个 spec。这样不论 AI 做了什么，你最终产出的东西都是可验证的。" 月球大叔给的应用场景是"帮大家在上线前检查 AI 写出来的那一堆乱七八糟的系统"——他说现在很多人的做法是"直接抛出一个需求，立刻出来一个软件"，连代码都不看了。
⚠️ 他随后给的限定，本库认为必须与上面整节一并读（[01:22:02]–[01:23:03]）：
月球大叔的问题很尖锐：可靠性领域有两个声音——一个说 AI 建系统的最大问题就是可靠性与安全，完全没法保证，非常令人焦虑；另一个说形式化验证已经从五年压到五小时。如果第一件事成立，第二件事就不该成立。为什么差距这么大？
⚠️ 他的回答： > 即使你能形式化验证，它也只告诉你"你的系统代码与你需要的 spec 一致"，它做的就这些。但"你到底需要什么样的系统、你的需求是什么、你想要什么样的 spec"——这件事我认为很难完全靠 AI 解决，需要有经验的人来处理。
他举的具体例子是 fault model（[01:22:02]–[01:23:03]）：形式 spec 里有一个东西叫故障模型，你设想你的故障长什么样，然后据此建一套容错系统。"但也许明天后天你发现基础设施里有些别的问题——那些不在你故障模型里描述的故障怎么办？所以定义这个 spec 其实没那么容易，我觉得太难了。"

六、他的终局设想，以及把 ROC 整个翻出来¶

⚠️ 他对"理想的操作系统/系统"的回答是从可靠性出发的（[01:23:03]–[01:24:06]）：

一个可靠的系统，是在未来它至少 80% 的用户是 agent 的情况下仍然可靠的系统。而 agent 不是完美的——它会出错、会幻觉、会跑偏。那你的系统怎么容忍这些，并且还能给出反馈？因为 agent 也是很聪明的东西，只要你给它反馈，它第二轮就会做得更好。
月球大叔的感受（[01:24:06]）：细看之下还有多少硬问题没解决、要多少博士生和系统工程师一个一个去解，"有点像曼哈顿计划"。
⚠️ 他的回应是把历史翻出来："我觉得很多核心原则其实已经存在了。" 于是有了本期最好的一段历史挖掘——
ROC（Recovery-Oriented Computing）（[01:24:06]–[01:29:06]）：
大约 2000 年，David Patterson（伯克利教授、图灵奖得主、RISC 先驱之一）牵头的斯坦福—伯克利合作项目，拿到了 NSF 的大量经费。
⚠️ 核心前提：计算机系统必然会挂。"即使你把全部资源都投到测试和形式化验证上，系统仍然会挂。所以我们应该在恢复上大量投入，而不是假设系统永远可靠。" 问题变成——系统挂了之后我们能做什么？能不能造一个崩溃后能快速恢复的系统？
⚠️ 第一个想法是以人为中心的实证研究（[01:25:06]–[01:26:06]）：系统故障时，到底是硬件的错、网络的错，还是操作这个系统的人的错？ 我们谈容错时通常假设是硬件挂了、机器崩了、处理器出现 bit flip。而他们的实证研究发现：故障中占比最大的一块来自人为错误——操作员失误。 "人得去操作这些系统，而系统很复杂，所以人会犯错，而这些错误往往是系统宕机的首要原因。"
⚠️ Jim Gray 的那篇论文（[01:26:06]–[01:27:06]）：他后来获图灵奖，当时在硅谷的 Tandem Computers，产品线叫 NonStop——公司的目标就是造一个永不停机的系统，名字即由此而来。而 Gray 深入研究后发现：公司在可靠性上投入了巨大努力，系统仍然会挂；而主要原因同样是人的操作失误，不是硬件。
Patterson 往前推了一步（[01:27:06]）："我们不能假设用户不会犯错；我们应该设想系统崩了之后该怎么办。"
⚠️ 两个"很可爱的想法"：
1. system-wide undo（[01:27:06]–[01:28:06]）：人做了一个失败的操作，我怎么撤销它？ 他的类比很生动——"就像我第一次申博失败就再申一次"。但这件事非常难，因为没有系统支持你——"比如你发了一封邮件，发出去之后你怎么撤销？" 所以必须有一套非常系统化的机制。由于难以泛化，他们做了一个特例——一个可撤销的邮件服务器（因为发邮件这类操作特别难回滚），论文发在 USENIX ATC，给了三条（也许五条）原则。
2. microreboot（[01:28:06]–[01:29:06]）："系统出问题时我们最常规的动作是什么？重启。" 他指出我们很少在蓝屏之后去找 bug 在哪，直接重启能继续干活就继续——"70% 的恢复机制就是重启"。但工业系统里重启非常昂贵，因为你有缓存、有 TLB 之类的东西，一重启状态全没了。所以问题变成：能不能做成不需要全局重启、只重启那一个组件的 microreboot？ 同样只做成了 case study，难以泛化。
⚠️ 他给的今昔对照（[01:29:06]）："今天，这个想法体现在微服务和 serverless 系统里——你可以 microreboot 单个微服务。服务一直在被重启。所以这个想法其实已经活在实践里了。"
⚠️ 他的主张（[01:29:06]）： > 在 AI agent 时代，我们可以把那些经典原则重新拿出来直接复用。可以问：哪些想法仍然有价值、能帮到 AI agent，哪些我们不再需要了。这样我们就不必为每一条旧约束做优化，而能为 AI agent 设计一个好得多的系统。
⚠️ 月球大叔当场把它落到了 agent 上（[01:29:06]–[01:30:07]）："一个被 agent 使用的系统，agent 的每一个操作都能被撤销——这是多么漂亮的一套系统。" 他的回答是："我认为完全可以做到。这在理论上并不难，只是有没有人愿意做的问题。"
⚠️ 但他紧接着给了一条现实约束（[01:30:07]–[01:31:10]）："现在 AI 系统的一大挑战是发展太快。很少有人愿意说我要专注一两年去建一个系统。" 如果AI 能力在不断变、很多范式在不断变，那挑战就是"你怎么快速建一个系统、还能把它想清楚、而且让它对将来的 agent 范式也仍然可用"。
月球大叔给的延伸（[01:30:07]）：Claude 升级后某些方面反而变得不那么好用；而训练本质上是加数据、去数据——"如果这套 undo 用在这里，你就不需要重新训练，可以撤销某个东西。每次训练要花几亿美元。"

七、为什么可靠性与安全终于能拿到资源¶

⚠️ 他给的历史解释（[01:31:10]–[01:32:12]）：

二三十年前，可靠性和安全从来不是 first-class 原则，因为它们不挣钱——只有性能挣钱。特性加上性能，这两样挣钱。而可靠性或安全，你只是担心别亏钱，所以其实可以通过很多别的办法达到——包括买保险，或者写一大堆测试用例（测试用例永远不完备，但至少给你很多信心）。
⚠️ 翻转的原因是 agent："如果你让 agent 主导做很多事情，包括写代码，那可靠性和安全就是最大的问题，而这些不是靠把测试用例规模堆上去就能解决的。所以我认为这是一个很好的机会，可靠性与安全的研究者可以拿到很多资源，做一些更有意义的事。"
月球大叔的补充（[01:32:12]）：各公司握资源的人也意识到让 agent 把上限拉高并不难，真正的挑战是怎么持续信任这些 agent。⚠️ 他给的具体证据：涉及钱、填表、个人信息这类高价值任务时，官方口径是不建议你让 agent 做——因为他们不想承担这个责任。
⚠️ 他在这一段说的那句话，本库认为最能概括他整个人（[01:32:12]，并在 [01:48:22] 重复一次）：

"我其实不太相信 AI，但我认为人是应该被相信的。"

八、他对研究这件事本身的看法¶

⚠️ 本节大量内容涉及学术圈的规范与个人方法论。本库收录是因为其中几条对"AI 时代的研究与教育"有直接的可引用价值；纯个人经历部分见人物页。

⚠️ 他主张取消最佳论文奖（[00:13:21]–[00:15:21]）：他自己拿过、也当过 SOSP 最佳论文评审委员，但他的判断是——"最佳论文这件事非常随机、非常主观，对我来说它完全不能代表一篇论文的质量。" 他甚至说近年 SOSP/OSDI 的最佳论文在他看来"有不少问题"。
机制解释：拿到提名通常只意味着某一位评审特别喜欢你的论文并提名了它——"它不代表这篇论文未来的影响力，也不代表这是这里质量最高的论文，因为质量本身其实没法度量"。
⚠️ 他的核心论点："有这些论文奖，实际上让大家不去好好做研究。如果把最佳论文去掉，大家就会去做自己最喜欢的研究，我认为那是最好的状态。"
月球大叔问他这么说会不会得罪人，他答"我真的不担心这个"，并说自己在会议上已经向很多人表达过这个观点。
⚠️ 他把这条推到了中国学术界："我其实被奖项搞得很糟心，我的理想是一个没有这些奖项之类烦人东西的学术环境——每个研究者只研究他认为重要的问题，做得开心快乐，得到认可，然后你就去讲这篇论文。"
⚠️ 他反对"先读 100 篇论文"（[00:35:34]–[00:37:35]）：他转述导师的一个激进观点——"每篇论文都非常有偏见，只是作者自己的视角"；而且顶会评审很严格，所以大家写论文时用了很多技巧，不一定那么诚实。
⚠️ 他自己的比喻："很多论文就像 feed，你消费太多 feed，大脑就麻木了，然后你就没法创新了。"
他的替代方案：从真实问题出发产生想法——"我们需要解决这个问题，那怎么解决？如果这个问题重要而且困难，它就需要研究"，而不是因为某篇论文拿了最佳论文奖，就去读人家的 limitations 一节，然后写你的下一篇。
那新生该干什么："给学生好问题去追，这是导师的工作。" 以及跟高年级学生一起做项目——他说这是他导师的做法，也是伯克利每个新生的做法；⚠️ "伯克利是更大的实验室，师生互动大多不那么 hands-on，你其实从同辈身上学到的比从教授身上学到的更多。"
⚠️ 关于"论文能不能只留摘要 + 引言 + 与 agent 的对话"（[00:41:37]–[00:44:41]）：
他说这在某些场景下成立：如果你工作的贡献最终是一个 artifact，而且这个 artifact 很有用、大家都能用、用得也好，那也许一个摘要告诉别人怎么用就够了。
⚠️ 但他的反对意见是本节的核心："很多研究其实是一个思考的过程，因为我觉得研究的本质是理解世界。你对这件事的理解，我认为不应该完全通过 AI 来呈现。" 他引 Leslie Lamport—— > 如果你不把东西写下来，你其实没法把它想透。 > "所以写作这个过程，是帮助人真正理解的过程。我个人真的不认为它应该被跳过。"
月球大叔的加强："博士期间最主要的训练，写论文这个过程，恰恰是训练你大脑的过程。你写不清楚，说明你这个问题肯定没想透。"
⚠️ 他给的"为什么现在有人提这个"的诊断，本库认为是本期关于学术生态最有价值的一条（[00:42:40]–[00:43:41]）： > 很多观点被提出来，是因为现在的评审系统压力太大。AI 出来之后大家生产力提高了，投稿量暴增。系统这个圈子特别小——过去一年可能只有 200 篇投稿，现在变成了 1000 篇。你还按原来的组织方式处理，压力就非常大；而压力上来之后，你的系统其实是不可扩展的。当你的 workload 规模上去，你的系统就开始崩。 > "我认为我们该反思的是这个——怎么让这个系统能 scale 到当前的投稿量，而不是把它简化成另一个系统。比如你把写作那部分、思考那部分去掉，我认为研究的本质就被破坏了。"
月球大叔转述陶哲轩：以前数学家要想出很多想法；现在想法变得太容易了，数学家不得不不断复核与验证这些想法。 ⚠️ 本库认为这条与 OpenAI 数学团队那期关于"瓶颈从证明迁移到理解与吸收"的表述指向同一件事，应并列读。
⚠️ AI 时代研究的门槛变了，但本质没变（[00:43:41]–[00:45:42]）：
"过去没有 AI 的时候，你可能能做一些研究——想法不算特别有意思，但涉及大量工程工作，或者需要某些特殊技能才能完成。现在这类研究变得相对困难，因为 AI 能帮你做这些事。" 所以推进前沿的方式不同了，因为前沿本身不同了。
⚠️ 但："研究的本质我认为没变。好的研究者仍然是好的研究者。陶哲轩仍然是陶哲轩——不是说谁用了 AI 就立刻比陶哲轩更强，我不认为是这样。"
⚠️ 他对"AI 提升 5 倍 / 10 倍 / 100 倍"的反问，本库认为该进 AI 与就业： > 问题是你的 baseline 是多少？如果你的能力是 0，乘 100 还是 0。 > 月球大叔的补充："对一个已经 100 分的人来说变成 10000，对一个 1 分的人来说变成 100——差距反而更大了。"
⚠️ 他对"还要不要学 CS"的回答（[00:56:50]–[00:58:50]）：
他同意市场会萎缩："CS 的就业市场确实不如以前大了，因为 AI 能接管很多任务。过去一些非常简单的任务也需要你雇一个 CS 本科生来做，现在 AI 能帮你做。所以如果我们担心的是这个市场会萎缩，我确实认为它会萎缩。"
⚠️ 但："如果你说 OS 会消失，我不认为有这个可能……整个现代社会都在构建大规模计算机系统。"
月球大叔的概括：这些课教的是计算机工程思维，不受外部影响——"只要你有这种思维，不管 AI 怎么发展，你都能在这个社会上找到一份很有价值的工作"。
⚠️ 他对 agent 能不能取代导师的回答（[00:38:36]–[00:39:37]）："agent 是一个相当冷的东西……不是那种体贴或者周全的东西。我认为来自人的指导仍然相当重要，不管那个人是高年级学生还是导师。" agent 能提升编码生产力、系统构建的生产力，也能帮你想出一些点子——"但最后即使它帮你想出了点子，你仍然要自己搞清楚哪些能做、哪些不能做。"
他的总体立场："我不相信未来的世界会被 agent 完全取代。我仍然认为未来的世界是人的世界，但大量的劳动会被 agent 接管。"
⚠️ 他对 AGI 讨论的态度很干脆（[00:39:37]）："想 AGI 实现之后会发生什么，对我来说是相当浪费时间的事。对我来说就像在想世界末日之后该做什么——想想挺好玩，但别太当真。" 配套的一条更实际："如果一个学生总是在那儿惊慌，说 AI 会取代我学的一切、全都没用了，那本质上你就没法进步了。" 他给的替代姿态是——"别想太多，就想一点点未来：agent 现在能做什么？然后用当下的 agent 提升我们的学习能力和工作技能。"
他对操作系统课的理解（[00:52:47]–[00:56:50]）：见人物页第六节。⚠️ 最该记的一条是：上他这门 kernel 编程课的学生，毕业后真去做 Linux 开发的"不到 10%、可能不到 5%"——"95% 的人不会成为 kernel 开发者，他们之后可能是去 hack Kubernetes 或者建 AI 基础设施。" 那这门课到底教了什么？"kernel hacking 只是一个媒介，他们获得的技能是怎么管理这种复杂度。" 他把它直接接到自己在 Facebook 的经历上——面对一个巨大的代码库，要在一个月内推进并建出东西，就必须有能力做大量抽象、理解复杂度、并且仍然能往前推进。"如果一个学生上完这门课，能获得面对一条凶龙、或者面对一个并不完美的世界的信心，我认为这就是这门课教给他们的最大技能。"

与本库其它观点的关系¶

AI 基础设施：本页是该页第一份从"系统研究"学科本身出发的材料。"把 agent 当用户，系统一定会挂"、"agent 时代可靠性与安全第一次成为能拿到资源的方向"、以及 ROC 的 undo / microreboot 在 agent 时代的复用主张，都是该页此前没有的结构性论证。⚠️ 与肖志斌关于"瓶颈已从芯片转移到系统与软件"的判断并读时要注意：两人讲的是同一句话的两个层次——肖志斌指的是性能优化，徐天音指的是可靠性与接口设计。
LLM 安全：TLA+ Foundation 那个 benchmark 是本库迄今最具体的一条 reward hacking 一手证据——不是"模型答错"，而是它写出看起来成立、实际不成立的形式化证明，并因此逼出了工具链里从没被发现过的 bug。⚠️ 这条与 Gray Swan 的红队工作、Onyx Security 的"AI 看管 AI" 处在不同层次：他说的是验证工具本身被 reward hacking 攻破。同时，SDD（specification-driven development） 是该页此前没有的一条防守侧提案，⚠️ 但必须与他自己给的限定一并读：形式化验证只保证代码与 spec 一致，"你到底需要什么样的 spec"仍然需要有经验的人。
评测与基准：SREGym 一年从 11.4% 到"接近 90%"是该页最锋利的一条饱和数据。他给的 benchmark 方法论（最好的 benchmark 是 AI 能做 30–40%）与保真度困境（小环境才能做 RL，但扔掉的东西如果重要，模拟器就没用了；coding benchmark 是离线的，SRE 是在线的）是该页关于环境类 benchmark 的第一组系统论述。
AI for AI 与自动研究：形式化验证五年 → 五小时是本库迄今对"AI 压缩一项研究工作"最具体的量化。⚠️ 它与 OpenAI 数学团队那期高度互补：那期是 AI 产出新数学结果，这期是 AI 把一项已知方法的准入成本打掉。两期都指出了同一件剩余物——"该建模什么"与"该问什么"这类判断仍在人手里。
AI 与就业：他给的"应届生怎么成为那个有品味、能指导 agent 的人"的问题，以及他自己承认无解的那一半（岗位在减少、爬梯子的过程消失了），是该页最诚实的一条表述。"如果你的能力是 0，乘 100 还是 0"与月球大叔的"差距反而更大"应一并引用。⚠️ 这条与苏廷浩从高中生角度描述的意义感塌陷、肖志斌关于"大模型工程师会变成用 EDA 工具的人"的推演构成本次摄取中指向同一方向的三条独立证词。
实践中使用 LLM："任何系统任务，只要你告诉 AI 怎么做，它基本都能做——关键是怎么做和成本多少"，以及"给它一个模糊的 spec 它也能做，但要很多轮迭代、代价很高"，是该页关于任务规约成本的具体表述。
开源基础设施：⚠️ "AI 知道一个成熟开源项目哪些地方 tricky、哪些地方历史上从没出过问题"——这是本库第一次看到有人把开源项目的历史本身当作模型的一种先验知识来使用。
月球大叔：本期是该频道在本库中第一份学术界系统研究材料。⚠️ 本期主持人的提问质量值得单记——"当年的用户是人，现在用户是 agent，系统要不要重新设计"与"既然验证已经五年压到五小时，为什么还有人说 AI 建系统最大的问题是可靠性"这两问，都直接逼出了嘉宾本期最实质的回答。