Код бортового управляющего компьютера космического аппарата Аполлон (AGC) — одна из самых тщательно исследованных кодовых баз в истории. Её прочитали тысячи разработчиков. Учёные публиковали статьи о её надёжности. Эмуляторы выполняют её команда за командой. Мы обнаружили в ней баг, который, похоже, оставался незамеченным пятьдесят семь лет: блокировку ресурсов в коде гироскопического управления, приводящую к утечке на ошибочный путь и отключающую возможность изменения положения платформы наведения.Для преобразования 130 тысяч строк ассемблерного кода AGC в 12,5 тысячи строк спецификаций мы воспользовались Claude и Allium — нашим опенсорсным языком создания поведенческих спецификаций. Спецификации были выведены из самого кода, и этот процесс направил нас непосредственно к багу. Читать далее