ИИ пишет код для всего мира. Но кто его проверяет?

Code Metal привлёк $125 млн на переписывание кода оборонки с помощью ИИ. Google и Microsoft сообщают, что 25–30% нового кода генерируется ИИ. AWS перевёл 40 млн строк COBOL для Toyota. CTO Microsoft прогнозирует, что к 2030 году 95% кода будет написано ИИ. Переписывание мирового софта — не прогноз, а факт.

Anthropic недавно построила C-компилятор на 100 000 строк за две недели силами параллельных ИИ-агентов — меньше чем за $20 000. Он загружает Linux, компилирует SQLite, PostgreSQL, Redis. ИИ создаёт масштабный софт с поразительной скоростью. Но может ли он доказать корректность компилятора? Пока нет. Формальную верификацию результата никто не делает.

Андрей Карпати описал типичный паттерн: «Я нажимаю “Принять всё”, я больше не читаю диффы». Когда ИИ-код достаточно хорош в большинстве случаев, люди перестают внимательно проверять его. При этом почти половина ИИ-кода не проходит базовые тесты безопасности, и более крупные модели не генерируют более безопасный код, чем предшественники.

ИИ переписывает мировой софт

Вспомним масштаб. Один баг в OpenSSL — Heartbleed — раскрыл приватные коммуникации миллионов пользователей, прожил два года код-ревью и обошёлся индустрии в сотни миллионов долларов. Один баг, один разработчик, одна библиотека. ИИ генерирует код в тысячу раз быстрее, по всем слоям стека, а защита (ревью, тестирование, ручная инспекция) — та же, что пропускала Heartbleed два года.

Harvard Business Review описал феномен «workslop» — ИИ-работа, которая выглядит отполированной, но требует исправлений. Когда это служебная записка — раздражает. Когда криптографическая библиотека — катастрофа. По мере ускорения генерации разрыв верификации не сокращается — он растёт.

Угроза выходит за пределы случайных ошибок. Противник, способный отравить обучающие данные или скомпрометировать API модели, может внедрить тонкие уязвимости в каждую систему. Атаки на цепочки поставок уже в числе самых разрушительных в кибербезопасности, а ИИ-код создаёт цепочку поставок нового масштаба. Формальная спецификация — защита: она определяет «корректность» независимо от ИИ, создавшего код.

Низкое качество софта уже обходится экономике США в $2,41 трлн в год (данные 2022 года, до того как ИИ стал писать четверть нового кода). Крис Латтнер, создатель LLVM: ИИ усиливает и хорошую, и плохую структуру. Плохой код на скорости ИИ превращается в «непостижимые кошмары». Неверифицированный код в критической инфраструктуре — системный риск.

Ситуация ухудшится быстро — если верификация не будет масштабироваться вместе с генерацией.

Почему математическое доказательство

Тестирование и доказательство дополняют друг друга. Тестирование даёт уверенность. Доказательство даёт гарантию. Одно доказательство покрывает каждый возможный вход, каждый граничный случай, каждое чередование.

Пример. ИИ переписывает TLS-библиотеку. Код проходит все тесты. Но спецификация требует выполнения за постоянное время: ни одна ветка не должна зависеть от секретного ключа. Реализация ИИ содержит тонкое условие, зависящее от битов ключа — атаку по времени, невидимую для тестов и код-ревью. Формальное доказательство ловит это мгновенно.

С-компилятор от Claude иллюстрирует обратную сторону: он оптимизирует для прохождения тестов, а не для корректности — жёстко вшивает значения под тестовый набор. Для любой фиксированной стратегии тестирования достаточно продвинутая система может переобучиться под неё. Доказательство невозможно обмануть.

ИИ убирает трение ручного написания кода — включая полезное трение, заставлявшее думать. Ответ — не замедлять ИИ, а заменить человеческое трение математическим: пусть ИИ работает быстро, но доказывает свою работу.

Верификация — не налог, а ускоритель

Когда ИИ сможет генерировать верифицированный софт так же легко, как неверифицированный, верификация из затраты превращается в катализатор.

Компания поставляет ML-ядра для нового железа. Сегодня месяцы уходят на тестирование и квалификацию. Когда ИИ пишет ядро и доказывает его корректность за один проход — сроки сжимаются до часов. Сертификация в аэрокосмосе, автомобилестроении, медицине сейчас занимает годы; верифицированная генерация кода может свернуть это до недель.

По мере того как ИИ берёт на себя реализацию, написание спецификаций становится ключевой инженерной дисциплиной. Спецификация заставляет ясно думать о том, что система должна делать, какие инварианты поддерживать, что может пойти не так. Мощный приём: неэффективная, но очевидно корректная программа служит собственной спецификацией. Пользователь и ИИ пишут простую модель, ИИ пишет оптимизированную версию и доказывает эквивалентность.

Что нужно платформе верификации

Маленькое доверенное ядро — несколько тысяч строк кода, проверяющих каждый шаг каждого доказательства механически. Всё остальное (ИИ, автоматизация, человек) — за пределами доверенного периметра. Независимые реимплементации ядра на разных языках служат перекрёстной проверкой.

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

Альтернатива — «кнопочные» солверы, возвращающие бинарный «да/нет» без промежуточного состояния, — не дают ИИ ничего для обучения ^[1] и управления поиском. Хуже того, доказательства, полагающиеся на эвристические солверы, часто ломаются при обновлении солвера.

Нужна максимально большая библиотека формализованных знаний. Верификация софта — это математика ^[2]: те же рассуждения, что доказывают теорему в абстрактной алгебре, доказывают корректность криптобиблиотеки.

ИИ-сообщество уже сделало выбор. AlphaProof (DeepMind), SEED Prover (ByteDance), Axiom, Aleph, Mistral AI — все строят на Lean. Каждая крупная ИИ-система, достигшая медального уровня на Международной математической олимпиаде, использовала Lean.

Lean опирается на Mathlib — крупнейший корпус формализованной математики: более 200 000 формализованных теорем, 750 контрибьюторов. Пять филдсовских медалистов работают с Lean. AWS верифицировал движок авторизации Cedar, Microsoft использует Lean для верификации криптобиблиотеки SymCrypt.

Знак того, что грядёт

ИИ-агент (обычный Claude, без спецобучения для доказательства теорем) конвертировал zlib — широко используемую C-библиотеку сжатия — в Lean с минимальным участием человека. Ключевая теорема:

theorem zlib_decompressSingle_compress (data : ByteArray) (level : UInt8)

    (hsize : data.size < 1024 1024 1024) :

    ZlibDecode.decompressSingle (ZlibEncode.compress data level) = .ok data

Машинно-проверенное доказательство: декомпрессия сжатого буфера всегда возвращает исходные данные, для любого уровня сжатия, для полного формата zlib. Ожидалось, что это ещё невозможно.

zlib — последовательный алгоритм с чистой RFC-спецификацией, проще базы данных или распределённой системы. Разрыв между этим результатом и верифицированным стеком — реальный. Но траектория важнее стартовой точки. Главное: барьер — уже не возможности ИИ, а готовность платформы верификации.

Подход масштабируется. Группа Ильи Сергея в NUS построила Veil — верификатор распределённых протоколов поверх Lean, совмещающий проверку моделей с полным формальным доказательством. При верификации протокола Rabia команда обнаружила несогласованность в предшествующей формальной верификации, не замеченную двумя другими инструментами.

ИИ-системы на Lean решили открытые математические задачи, не поддававшиеся десятилетиям. Один математик с ИИ-агентом формализовал полную теорему о простых числах за три недели: 25 000 строк Lean, более 1 000 теорем. Предыдущая формализация заняла больше года и десятки людей.

Верифицированный стек

Слой за слоем критический стек будет реконструирован с встроенными математическими доказательствами. Криптография — потому что всё остальное ей доверяет. Базовые библиотеки (структуры данных, алгоритмы, сжатие). Движки хранения вроде SQLite, встроенного в каждое устройство. Парсеры и реализации протоколов (JSON, HTTP, DNS). Компиляторы и среды выполнения.

Верифицированный SQLite несёт доказательства, что сбой во время записи не повредит базу, что конкурентные читатели никогда не увидят частичных транзакций. Тестирование даёт уверенность; математическое доказательство покрывает каждую точку сбоя и каждое чередование.

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

Сегодня интеграция — место большинства багов: границы между компонентами, несовпадающие допущения. Верифицированные интерфейсы фундаментально отличаются: когда каждый компонент несёт доказательство по общей спецификации, композиция корректна по построению. Это преимущество масштабируется суперлинейно.

Мир, который это создаёт

Цель — верифицированный стек: открытый, свободный, математически гарантированно корректный. Роль инженера не исчезает, а сдвигается к спецификациям, проектированию систем на более высоком уровне абстракции. Работа становится более творческой: проектирование до генерации, мышление ^[3] до написания кода.

Спецификации поднимают и не чисто технический вопрос: кто решает, что значит «корректно»? Спецификация для медицинского устройства, системы голосования или монитора безопасности ИИ кодирует ценности, а не только логику ^[4]. Формальные и публичные спецификации не решают эти вопросы, но делают их явными и проверяемыми.

ИИ, генерирующий доказуемо корректный код, качественно отличается от ИИ, генерирующего правдоподобный код. Верификация превращает ИИ-генерацию кода из инструмента продуктивности в инфраструктуру доверия.