研究人员使用AI工具和开源规范语言Allium，在阿波罗导航计算机(AGC)的陀螺控制代码中发现了一个存在57年的资源锁漏洞。该漏洞会在错误路径上泄露，导致制导平台无法重新校准。团队通过将13万行汇编代码提炼为1.25万行规范，最终定位到这个长期被忽视的缺陷。

标题：月球暗面的一个程序错误

主要内容：

1. 发现历史性错误

   • 阿波罗导航计算机（AGC）的代码库经过严格审查，但57年来一直未被发现一个资源锁泄漏问题。该问题存在于陀螺控制代码中，错误路径未释放锁，导致制导平台无法重新校准。

2. 研究方法

   • 使用开源行为规范语言Allium和AI工具Claude，将13万行AGC汇编代码提炼为1.25万行规范，直接定位到缺陷。

3. 错误细节

   • 共享资源锁LGYRO在正常路径中会被释放，但在紧急“锁定”（caging）操作时，错误路径BADEND未释放锁。缺少的两条指令（4字节）导致后续所有陀螺操作挂起。

4. 潜在风险场景

   • 1969年阿波罗11号任务中，如果宇航员迈克尔·柯林斯在月球背面操作时意外触发锁定开关，可能导致制导系统无法校准，影响返回地球的引擎点火方向。

5. 历史背景

   • AGC代码存储在手工编织的74KB核心绳存储器中。尽管经过严格测试和模拟，但此前未进行形式化验证或静态分析。

6. 现代启示

   • 现代编程语言（如Go、Rust）通过结构设计避免资源泄漏，但类似问题仍存在于数据库连接、分布式锁等场景中。

7. 结论

   • 这一57年前的错误未被发现，也未修复。文章呼吁关注现有系统中可能隐藏的类似问题。

（注：删减了部分历史细节和技术实现过程，保留了核心错误描述和关键背景信息。）

总结评论内容：

1. 对AI生成内容的质疑

• 认为AI写作缺乏灵魂："feels soulless and plastic"（评论1）
• 讽刺AI标注惯例："add 'using claude code'"（评论4）

2. 对文章质量的赞赏

• 高度评价写作水平："insightfully and powerfully written"（评论2）
• 为作者辩护："accused of 'being AI slop'"（评论2）

3. 对AI发现bug的讨论

• 质疑准确性："high false positive rate"（评论3）
• 指出局限性："bugs that AI won't find but humans would"（评论3）

4. 对代码复杂性的观察

• 以小见大："complexity hiding in even the smallest codebases"（评论5）
• 历史案例佐证："Software that ran on 4KB...still has undiscovered bugs"（评论5）