Фаззинг или формальное доказательство: что именно они подтверждают в коде

Команда проверила библиотеку миллионами случайных входов и не увидела падения. Другая команда предъявила математическое доказательство, что программа не падает. Какой результат сильнее? Ответ зависит от границы проверки. Фаззинг способен обнаружить реальные ошибки и показать вход, на котором они воспроизводятся, но отсутствие найденного сбоя не означает отсутствие сбоя вообще. Доказательство охватывает все входы внутри формально заданной модели, но если модель не учитывает важное поведение системы, формально верный вывод не спасёт продукт. Эти методы не взаимозаменяемы.

На какой вопрос отвечает фаззинг

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

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

На какой вопрос отвечает доказательство

При формальной верификации свойство записывают как точное утверждение. Например: «для любого файла меньше заданного размера, при таких-то ответах операционной системы программа завершится без выхода за границы памяти». Затем строят цепочку рассуждений, которую проверяет небольшой доверенный компонент. Если доказательство прошло, утверждение выполнено в пределах указанных допущений. Это мощнее, чем «ошибку пока не нашли», но заметно уже рекламного «код полностью безопасен».

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

Где в этой истории ИИ

Исследователи Anthropic и Theorem показали путь, в котором Claude помогает писать большие формальные доказательства для скомпилированных программ, а отдельное ядро Rocq проверяет их. В описанном опыте речь шла о 239 входных точках из 123 открытых библиотек и ограничении размера входа. Эти числа впечатляют как инженерный масштаб, но не превращают все библиотеки в «безошибочные». Исследование относится к конкретным свойствам, архитектуре и условиям; авторы прямо описывают ограничения.

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

Как выбрать метод для обычного проекта

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

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

Полезный отчёт не должен скрывать отрицательные результаты. Запишите длительность фаззинга, покрытые версии, число найденных сбоев и условия остановки. Для доказательства — точный текст свойства, доверенные компоненты, все допущения и версии инструментов. Если проверить удалось только однопоточный путь, так и напишите. Это даст читателю больше, чем абстрактная отметка «проверено ИИ».

Вывод

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

Частые вопросы

Можно ли прекратить фаззинг после успешного доказательства? Только если доказанное свойство полностью совпадает с целью фаззинга и условиями реального запуска. Обычно остаются другие свойства и интеграционные ошибки.

Если ИИ написал доказательство, можно ли ему доверять? Доверять следует проверке конкретного доказательства и правильности исходной спецификации, а не авторству текста.

Обязательно ли это маленькому сайту? Нет. Начните с тестов, обновлений зависимостей и проверки границ ввода. Формальные методы оправданы там, где высока цена ошибки и область можно чётко ограничить.