22 октября Anthropic опубликовала исследование формальной верификации с участием Claude и команды Theorem. Авторы сообщили о проверке 239 точек входа в 123 библиотеках из OSS-Fuzz. На Mentoring.digital объясняем главное различие: найденное моделью доказательство проверяет отдельная система, а область вывода задаётся условиями задачи.
Как разделили работу модели и проверяющего инструмента
Claude участвовал в построении доказательств, которые проверялись системой Rocq. В отличие от обычного ответа модели, здесь недостаточно убедительно описать, почему программа должна работать. Предложенное доказательство должно пройти формальную проверку относительно заданных правил.
В эксперименте тестовые точки входа компилировали для RISC-V. Проверяемое свойство касалось отсутствия аварийного завершения при входных данных размером менее 64 МБ в принятой модели выполнения. Это существенно уже утверждения «весь проект не содержит ошибок».
Какие границы нельзя опускать
Авторы работают с однопоточным статически собранным кодом, фиксированной моделью памяти и описанной семантикой RISC-V и Linux. Корректность этой модели, формулировка утверждения и проверяющее ядро остаются частью доверенной основы.
Такое доказательство не подтверждает автоматически правильность бизнес-логики, защиту всех развёрнутых конфигураций или отсутствие проблем многопоточности. Если свойство не включено в формулировку, нельзя считать его доказанным только потому, что проверка завершилась успешно.
Что из этого полезно разработчику
Практический вывод редакции: оценивать AI-инструмент нужно вместе с независимым способом проверки результата. Для обычной задачи это может быть воспроизводимый тест и проверка изменений человеком; для формального утверждения требуется подходящий проверяющий инструмент.
При обсуждении подобного исследования полезно задать три вопроса: что именно доказано, для какого кода и при каких допущениях. Разобрать применение моделей в разработке можно с наставником по машинному обучению. Исследование показывает конкретный эксперимент, а не готовую гарантию качества любого кода, написанного Claude.
