Неизвестный баг в apollo 11: как формальные методы нашли 55-летний дефект

08.04.2026 · 5 мин

Уже читал про баг в Apollo 11? Я тоже думал, что всё давно изучено. Тысячи людей смотрели этот код, эмуляторы запускали его по инструкции, академики пишут статьи о надёжности. Но оказалось — кое-что пропустили.

В Juxt нашли неизвестный дефект в коде управления гироскопами. Баг сидел там 55 лет.

Компьютер размером с холодильник

Давай сначала про контекст. Apollo Guidance Computer (AGC) — это бортовой компьютер лунного модуля. 2 килобайта оперативной памяти (да, не мегабайт — килобайт), тактовая частота 1 мегагерц. Программа хранилась в 74 килобайтах тросовой памяти — медная проволока, продетая через магнитные сердечники вручную на фабрике. Провод через сердечник — это единица, мимо — ноль. Работали над этим «маленькие пожилые дамы» (так их звали внутри MIT), и память так и называли — LOL memory.

Исходный код опубликовали только в 2003 году. Рон Бёрки с командой волонтёров перепечатывали его вручную из распечаток, которые хранятся в музее MIT. В 2016 году бывший стажёр NASA Крис Гарри выложил это на GitHub — и код завирусился. Тысячи разработчиков листали ассемблер машины, которая отправила людей на Луну.

Казалось бы — изучено вдоль и поперёк.

Как искали баг

Ребята из Juxt пошли другим путём. Они взяли Claude и Allium (свой open-source язык поведенческих спецификаций) и перевели 130 000 строк ассемблера AGC в 12 500 строк спецификаций. Не просто прочитали код — формализовали его.

Фокус был на подсистеме IMU — Inertial Measurement Unit, инерциальной системе навигации. Это та часть, которая говорит кораблю, куда он направлен, используя гироскопы.

Самое интересное — спецификация моделировала жизненный цикл каждого общего ресурса: когда он захватывается, когда освобождается, и по каким путям кода это происходит. И именно этот анализ выявил дефект.

Сам баг

Проблема — утечка блокировки ресурса (resource lock) на ошибочном пути выполнения.

Представь: компьютер управляет гироскопами, которые ориентируют корабль в пространстве. Чтобы несколько частей системы не пытались крутить гироскоп одновременно, используется блокировка — ресурс захватывается перед использованием и освобождается после. Нормальный путь работает корректно.

Но есть ситуация, когда происходит ошибка — и на этом пути блокировка не освобождается. Она «утекает». Если ошибка случается повторно, система в итоге остаётся без свободных ресурсов.

НОРМАЛЬНЫЙ ПУТЬ                    ПУТЬ С ОШИБКОЙ
───────────────                    ──────────────
Захватить ресурс ──▶ Использовать ──▶ Освободить
                      ▲
                      │
                 (ошибка)
                      │
                      ▼
              Захватить ресурс ──▶ ??? (утечка!)
Сравнение путей выполнения: на ошибочном пути ресурс не освобождается

Красота в том, что спецификация показала это напрямую. Не надо было гадать или искать иголку в стоге сена — формальный анализ сам указал на проблемное место.

Почему это не всплыло раньше

Удивительно, но до сих пор не было публичной формальной верификации, model checking или статического анализа кода полёта AGC. Всё, что делали — читали код, запускали эмуляторы, проверяли транскрипцию. Глубоко, да. Но определённым способом.

Команда Juxt применила другой подход — формальные методы. И баг нашёлся.

Насколько он был критичен в реальном полёте? История умалчивает. Возможно, этот путь просто никогда не срабатывал. Возможно, астронавты справлялись вручную. Но факт остаётся фактом: 55 лет никто не замечал.

Что это значит для нас

Несколько мыслей.

Первое: даже самый изученный код может содержать неизвестные дефекты. Тысячи глаз смотрели на AGC, но искали по-разному — не тем инструментом.

Второе: формальные методы — это не академическая экзотика. Они реально находят баги, которые не видны при ручном ревью. Когда 130 000 строк ассемблера превращаются в 12 500 строк спецификации — начинает работать магия.

Третье: исторический код — это не музейный экспонат. AGC до сих пор изучают, и он до сих пор способен удивлять. Это как раскопки — всегда есть шанс найти что-то новое.

Меня зацепила сама история «маленьких пожилых дам», которые вручную плели память для корабля. Они не знали, что их работа — часть одной из величайших историй в истории человечества. И они точно не знали, что через 55 лет какой-то язык спецификаций найдёт баг в том, что они создали.

Интересно, какие ещё скелеты прячутся в том коде?

Ссылки

Дмитрий Полухин — продуктовый дизайнер. Пишу про разработку, AI и дизайн интерфейсов. Обо мне, контакты и профили.

Что почитать дальше