We found an undocumented bug in the Apollo 11 guidance computer code

The Apollo Guidance Computer (AGC) is one of the most scrutinised codebases in history. Thousands of developers have read it. Academics have published papers on its reliability. Emulators run it instruction by instruction. We found a bug in it that had been missed for fifty-seven years: a resource lock in the gyro control code that leaks on an error path, silently disabling the guidance platform's ability to realign.

We used Claude and Allium, our open-source behavioural specification language, to distil 130,000 lines of AGC assembly into 12,500 lines of specs. The specs were derived from the code itself, and the process signposted us directly to the defect.

The source code has been publicly available since 2003, when Ron Burkey and a team of volunteers began painstakingly transcribing it by hand from printed listings at the MIT Instrumentation Laboratory. In 2016, former NASA intern Chris Garry’s GitHub repository went viral, topping the trending page. Thousands of developers scrolled through the assembly language of a machine with 2K of erasable RAM and a 1MHz clock.

The AGC’s programs were stored in 74KB of core rope: copper wire threaded by hand through tiny magnetic cores in a factory (a wire passing through a core was a 1; a wire bypassing it was a 0). The women who wove it were known internally as the “Little Old Ladies”, and the memory itself was called LOL memory. The program was physically woven into the hardware. Ken Shirriff has analysed it down to individual gates, and the Virtual AGC project runs the software in emulation, having confirmed the recovered source byte-for-byte against the original core rope dumps.

As far as we can determine, no formal verification, model checking or static analysis has been published against the flight code. The scrutiny has been deep, but it has been a particular kind of scrutiny: reading the code, emulating the code, verifying the transcription.

We took a different approach. We used Allium to distil a behavioural specification from the Inertial Measurement Unit (IMU) subsystem, the gyroscope-based platform that tells the spacecraft which way it is pointing. The specification models the lifecycle of every shared resource: when it is acquired, when it must be released, and on which paths.

It surfaced a flaw that reading and emulation had missed. The AGC manages the IMU through a shared resource lock called LGYRO. When the computer needs to torque the gyroscopes (to correct platform drift or perform a star alignment), it acquires LGYRO at the start and releases it when all three axes have been torqued. The lock prevents two routines from fighting over the gyro hardware at the same time.

‘Caging’ is an emergency measure: a physical clamp that locks the IMU’s gimbals in place to protect the gyroscopes from damage. When the IMU is caged while a torque is in progress, the code exits via a routine called BADEND, which does not clear the lock. Two instructions are missing: CAF ZERO and TS LGYRO. Four bytes. Once LGYRO is stuck, every subsequent attempt to torque the gyros finds the lock held, sleeps waiting for a wake signal that will never come, and hangs.

On 21 July 1969, while Neil Armstrong and Buzz Aldrin walked on the lunar surface, Michael Collins orbited alone in the Command Module Columbia. If this bug had manifested, Collins would have seen the program hang with no alarm. It would look like faulty hardware, not a stuck lock. A dead gyro system behind the Moon, with Armstrong and Aldrin on the surface waiting for a rendezvous burn that depends on a platform he can no longer align, is a nightmare scenario.

Margaret Hamilton and her team at the MIT Instrumentation Laboratory pioneered concepts we now take for granted: priority scheduling, asynchronous multitasking, and software-based error recovery. Their priority scheduling saved the Apollo 11 landing when the 1202 alarms fired. This newly discovered defect shows that even the most defensive code can have latent faults that remain hidden for decades.