The JUXT team, led by CTO Henry Garner, found a bug in Apollo 11's Guidance Computer code that escaped detection for 57 years. Using Claude AI and Allium, their open-source behavioral specification language, they distilled 130,000 lines of AGC assembly into 12,500 lines of behavioral specs. The process flagged a resource lock called LGYRO that fails to release when the Inertial Measurement Unit gets "caged" during a gyro torque operation. Four bytes of missing code would have fixed it.
During the mission, Michael Collins ran Program 52 every two hours to realign the guidance platform through star sightings. Each pass took him behind the Moon, out of radio contact. If he'd accidentally triggered the cage switch mid-torque, the lock would seize. Every subsequent alignment attempt would hang silently. No alarm, no error message. The DSKY would accept commands and do nothing. Collins wrote later that his "secret terror" was leaving Armstrong and Aldrin on the surface and returning to Earth alone. A stuck gyro system behind the Moon, with no aligned platform for the engine burn home, would have made that nightmare real.
The AGC codebase has been pored over since 2003, when Ron Burkey began transcribing it from original MIT Instrumentation Laboratory printouts. Chris Garry's 2016 GitHub repo made it go viral. Ken Shirriff analyzed it down to individual gates. The Virtual AGC project verified it byte-for-byte against core rope dumps. But as far as JUXT can determine, nobody published formal verification, model checking, or static analysis against the flight code until now. Reading and emulating are not the same as proving.
The methodology here matters more than the specific bug. Legacy systems everywhere carry similar hidden defects. Banking COBOL handling trillions, air traffic control, power grid SCADA, Pentagon weapons systems with 50 million lines of code. All critical, all old, all largely unverified. AI-assisted behavioral specification can surface bugs that human eyes miss, even in code thousands have read. The Apollo code was physically woven into copper wire by hand. These women, nicknamed "Little Old Ladies" internally, gave us "LOL memory." Their work was extraordinary. It was also, in at least one corner, imperfect.