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-ядра для нового железа. Сегодня месяцы уходят на тестирование и квалификацию. Когда ИИ пишет ядро и доказывает его корректность за один проход — сроки сжимаются до часов. Сертификация в аэрокосмосе, автомобилестроении, медицине сейчас занимает годы; верифицированная генерация кода может свернуть это до недель.
По мере того как ИИ берёт на себя реализацию, написание спецификаций становится ключевой инженерной дисциплиной. Спецификация заставляет ясно думать о том, что система должна делать, какие инварианты поддерживать, что может пойти не так. Мощный приём: неэффективная, но очевидно корректная программа служит собственной спецификацией. Пользователь и ИИ пишут простую модель, ИИ пишет оптимизированную версию и доказывает эквивалентность.
Что нужно платформе верификации
Маленькое доверенное ядро — несколько тысяч строк кода, проверяющих каждый шаг каждого доказательства механически. Всё остальное (ИИ, автоматизация, человек) — за пределами доверенного периметра. Независимые реимплементации ядра на разных языках служат перекрёстной проверкой.
Платформа должна быть одновременно языком программирования и системой доказательства теорем — код и доказательства в одной системе, без разрыва трансляции. Нужен расширяемый фреймворк тактик, дающий ИИ структурную обратную связь: текущая цель, доступные гипотезы, что изменилось после каждого шага.
Альтернатива — «кнопочные» солверы, возвращающие бинарный «да/нет» без промежуточного состояния, — не дают ИИ ничего для обучения и управления поиском. Хуже того, доказательства, полагающиеся на эвристические солверы, часто ломаются при обновлении солвера.
Нужна максимально большая библиотека формализованных знаний. Верификация софта — это математика: те же рассуждения, что доказывают теорему в абстрактной алгебре, доказывают корректность криптобиблиотеки.
ИИ-сообщество уже сделало выбор. 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 несёт доказательства, что сбой во время записи не повредит базу, что конкурентные читатели никогда не увидят частичных транзакций. Тестирование даёт уверенность; математическое доказательство покрывает каждую точку сбоя и каждое чередование.
Каждый верифицированный компонент — постоянное общественное благо. Открытый исходный код с доказательствами, которые нельзя отозвать, деградировать или удержать решениями одной компании. Когда вы строите на этом стеке, вы наследуете доказательства.
Сегодня интеграция — место большинства багов: границы между компонентами, несовпадающие допущения. Верифицированные интерфейсы фундаментально отличаются: когда каждый компонент несёт доказательство по общей спецификации, композиция корректна по построению. Это преимущество масштабируется суперлинейно.
Мир, который это создаёт
Цель — верифицированный стек: открытый, свободный, математически гарантированно корректный. Роль инженера не исчезает, а сдвигается к спецификациям, проектированию систем на более высоком уровне абстракции. Работа становится более творческой: проектирование до генерации, мышление до написания кода.
Спецификации поднимают и не чисто технический вопрос: кто решает, что значит «корректно»? Спецификация для медицинского устройства, системы голосования или монитора безопасности ИИ кодирует ценности, а не только логику. Формальные и публичные спецификации не решают эти вопросы, но делают их явными и проверяемыми.
ИИ, генерирующий доказуемо корректный код, качественно отличается от ИИ, генерирующего правдоподобный код. Верификация превращает ИИ-генерацию кода из инструмента продуктивности в инфраструктуру доверия.
Автор: Cloud4Y
