阿波罗11号藏了57年的bug：2K内存里的锁泄漏

130,000行汇编代码，2K可擦写内存，1MHz主频——人类首次登月的计算机配置，放在今天连智能手环的零头都不到。但就是这么个"电子古董"，它的代码库被读了57年，跑了无数模拟器，甚至被逐门电路分析过，直到上周，一个资源锁泄漏的bug才被发现。

发现者用的不是人眼，是Claude。

被读了57年的代码，为什么还能藏bug

阿波罗制导计算机（AGC）的源代码2003年就公开了。MIT仪器实验室的打印清单被Ron Burkey团队手工转录，2016年前NASA实习生Chris Garry把它丢上GitHub，当天冲上趋势榜。几千个开发者 scrolling 过这些汇编，学术论文一摞一摞，模拟器跑了几十年。

但有个细节被所有人漏掉了：没有人对飞行代码做过形式化验证、模型检查或静态分析。

大家干的事很"程序员"——读代码、跑模拟、核对转录是否准确。Virtual AGC项目甚至把恢复后的源码和原始磁芯绳转储逐字节比对，确认一模一样。Ken Shirriff分析到了单个门电路。这种scrutiny很深，但也很单一：它验证的是"代码是不是对的"，不是"代码是不是会错"。

发现bug的团队走了另一条路。他们用Allium——一种开源行为规约语言——把惯性测量单元（IMU）子系统的130,000行汇编蒸馏成12,500行规约。规约不是人写的，是从代码里自动提取的。它追踪每个共享资源的生命周期：什么时候获取，什么时候必须释放，哪些路径会异常。

然后它直接指出了一个缺陷：LGYRO锁在错误路径上泄漏了。

一个锁泄漏，能让飞船"找不着北"

LGYRO是AGC管理IMU的共享资源锁。IMU是个陀螺仪平台，告诉飞船现在朝哪。当计算机需要给陀螺仪加力矩（修正漂移或做星对准）时，先获取LGYRO，三个轴都处理完再释放。锁的作用是防止两个程序同时抢硬件。

正常路径：获取→干活→释放。异常路径呢？

有个叫"Caging"的紧急操作——物理夹具把IMU的万向节锁死，保护陀螺仪不受损。宇航员可以手动触发，某些故障条件也会自动触发。一旦Caging启动，当前操作会被中断，平台进入保护状态。

问题就在这里：Caging路径没有释放LGYRO。

锁被拿走了，没还。后续任何需要陀螺仪的操作都会卡在"等锁"上。制导平台失去重新对准的能力，飞船不知道自己朝哪。

这个bug的狡猾之处在于：它只在错误路径触发。正常飞行你根本碰不到。模拟器跑正常任务，一切完美。只有真实的故障叠加，才会暴露它——而阿波罗任务恰好没走到那一步。

Claude怎么做到的：不是读代码，是建模型

传统调试是"我看着代码觉得没问题"。形式化方法是"我让机器证明它有问题"。

Allium的工作流程像给代码做CT：先把汇编翻译成中间表示，然后自动推导状态机——每个变量、每个锁、每个硬件寄存器，在什么时刻可能是什么值。规约语言描述的是"允许的行为"，任何偏离都是可疑的。

Claude在这里的角色是"规约工程师的副驾驶"。人类定义IMU子系统的资源契约（比如"LGYRO必须在函数退出前释放"），Claude帮忙把自然语言意图翻译成Allium的规约表达式，同时解释反例——当工具报出"路径X未释放锁"时，Claude把汇编上下文翻译成人类能读的故障场景。

130,000行汇编→12,500行规约，压缩比10:1。规约不是摘要，是行为等价的形式化描述。它丢掉的是实现细节（哪条指令、哪个寄存器），保留的是交互逻辑（谁先谁后、什么条件下会卡住）。

这种蒸馏让隐藏模式显形。人眼读汇编，看到的是"把A存到B，跳转C"；规约看到的是"获取资源R，进入状态S，异常时忘记释放"。

为什么是现在：老代码遇上新工具

AGC的代码有特殊性：它 frozen 在1969年，没有后续补丁，没有兼容包袱。这让它成为形式化方法的理想试验田——规格明确，边界清晰，历史价值高。

但工具链的成熟才是触发因素。五年前，把10万行汇编自动翻译成可验证的中间表示，工程量大到不现实。LLM降低了规约编写的门槛：不是让AI代替人思考，是让AI处理翻译的dirty work，人类专注在"要验证什么"。

这个案例的讽刺性在于：AGC是被认为"最可靠"的软件之一。它载人登月成功，零现场故障。但可靠性不等于正确性——它只是恰好没触发错误条件。

57年后，我们用2020年代的工具，发现了一个1960年代的bug。这个bug从未造成事故，也可能永远不会。但它在那里，被锁在铜线穿过的磁芯里，等着被找到。