Researchers used AI and a behavioral specification language to identify a previously undocumented bug in the Apollo 11 guidance computer code, involving a resource lock leak in gyro control. The discovery was made by analyzing 130,000 lines of assembly through formal specification methods, despite the code's extensive historical scrutiny. This highlights how modern verification tools can uncover defects even in well-studied legacy systems.
Background
The Apollo Guidance Computer (AGC) code has been publicly available since 2003 and is one of the most studied codebases in history, though primarily through manual analysis and emulation rather than formal verification methods.
- Source
- Lobsters
- Published
- Apr 13, 2026 at 05:34 AM
- Score
- 7.0 / 10