阿波罗11号代码藏了57年的bug：2KB内存时代的幽灵锁

2KB内存，1MHz主频，74KB程序靠女工手穿铜线织进磁芯——这套1969年的计算机系统，被数千开发者读过、无数论文分析过、逐指令模拟过。一个资源锁泄漏的bug，硬是躲了57年。

发现它的是Anthropic的研究团队。他们用Claude和自研的行为规约语言Allium，把13万行AGC汇编蒸馏成1.25万行规格说明，代码自己"告诉"了他们缺陷在哪。这不是考古癖发作，而是给当下AI验证复杂系统打了个样。

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

AGC的源码2003年就公开了。Ron Burkey带着志愿者团队，从MIT仪器实验室的打印清单里手工抄录。2016年前NASA实习生Chris Garry把它放上GitHub，直接冲上趋势榜第一。那段时间，全球开发者都在刷这份汇编代码——有人逐行注释，有人做可视化，Ken Shirriff甚至分析到了门电路级别。

但所有 scrutiny 都集中在同一个维度：读代码、模拟执行、验证抄录是否准确。Virtual AGC项目把原始磁芯存储器的dump拿出来逐字节比对，确认恢复出的源码和1969年织进铜线的那版完全一致。

问题是：没人做过形式化验证。没有模型检验，没有静态分析，没有从代码里提取"这玩意儿该干什么"的规格说明。大家信的是"这么多人看过，肯定没问题"——一种分布式的人肉Code Review。

Anthropic团队换了个思路。他们没问"这行代码什么意思"，而是让Allium去推导"这些资源该遵守什么生命周期规则"。LGYRO锁的获取和释放路径，被建模成显式的状态机。规格是从代码本身蒸馏出来的，但视角完全不同——不是看代码"做了什么"，而是看它"承诺了什么"。

幽灵锁：紧急制动时埋下的雷

问题出在惯性测量单元（IMU）的控制逻辑。这个陀螺仪平台负责告诉飞船"我现在朝哪边"，是导航的核心。AGC用一个叫LGYRO的共享锁来管理它：要驱动陀螺仪时先拿锁，三个轴都处理完再释放，防止多个任务抢硬件。

正常路径很干净：进函数拿锁，出函数放锁。但还有第三条路——"Caging"（笼锁）。

这是物理层面的紧急保护：宇航员可以触发一个机械装置，把IMU的万向节直接锁死，防止陀螺仪在剧烈机动或故障时损坏。代码里检测到笼锁信号后，会立即跳转到错误处理路径。

跳转之前，没放LGYRO锁。

这个泄漏是静默的。没有报错，没有指示灯，飞船不会当场失控。但LGYRO一旦被占住，后续的陀螺仪对准操作——包括关键的恒星重新校准——都会被卡住。导航平台慢慢漂，宇航员慢慢懵。

57年里没人触发过？还是触发了但没被归因到这个bug？源码注释里没提，任务日志里也没明确记录。唯一确定的是：这个错误路径在代码里躺了半个多世纪，直到被AI从行为规格里"算"出来。

从铜线编织到AI蒸馏：验证方法的代差

AGC的存储叫"LOL memory"——Little Old Ladies memory。女工们坐在工厂里，把铜线手工穿过磁芯，穿过去是1，绕过去是0。程序不是"写"进去的，是"织"进去的。这种物理层面的不可修改性，让代码审查有了宗教般的仪式感：一旦上天，就是真理。

但仪式感不等于正确性。Anthropic的演示本质上是在说：人类读代码的极限，可以用AI+形式化方法突破。Allium把汇编的隐式契约变成显式规格，Claude负责理解和转换，最终定位到的是一个连NASA都没发现的边缘案例。

这事的讽刺之处在于：AGC当年是被"证明"过可靠的。它带着阿波罗11号着陆，带着阿波罗13号活着回来，任务成功率100%。但可靠性是统计概念，正确性是逻辑概念——前者可以靠测试和冗余堆出来，后者需要数学意义上的保证。

现在的复杂系统比AGC高出几个数量级。自动驾驶的代码量以亿行计，AI模型的行为空间几乎无限。传统的"读代码+测试用例"模式，在规模面前已经显形。Anthropic选AGC做demo，有点像是用考古来证明新工具的锋利：连这种被翻烂的历史遗迹都能挖出东西，现在的工业代码里还埋着什么？

团队把Allium开源了。规格语言和Claude的结合方式也写在论文里——不是替代人类审查，而是把"这代码想干什么"的推理负担，从人脑转移到可验证的形式化表示上。

那个泄漏的LGYRO锁，最后是怎么处理的？Anthropic的规格里标出来了，Virtual AGC的维护者已经收到报告。57年后，这段铜线编织的程序，终于有了一份机器生成的、可检验的行为契约。

如果AI能从被读烂的登月代码里找出新bug，你正在写的模块，上次被完整理解是什么时候？