LLMs are making formal software verification feasible at a much larger scale
Формальная верификация ПО исторически требовала огромных усилий экспертов: на написание кода ядра seL4 ушло два человеко-года, а на его формальное доказательство — двадцать. Из-за этого метод применяли лишь в критичных системах вроде авионики Airbus. Теперь большие языковые модели меняют расклад: с помощью Claude удалось автономно доказать свойства безопасности на уровне ассемблера (архитектура RISC-V) более чем в 100 реальных открытых библиотеках — по заявлению авторов, это первая крупномасштабная попытка применить ИИ для формальной верификации production-кода на уровне ассемблера.
В частности, доказано, что программы всегда завершаются нормально и не падают при любом вводе объёмом до 64 МБ на многих точках входа фаззинга Google OSS-Fuzz, включая сбои, выявляемые санитайзером ASan. Попутно Claude нашёл баги, годами ускользавшие от обнаружения, несмотря на триллионы прогонов тестов. Авторы честно оговаривают границы: ASan ловит не все ошибки памяти, охвачены не все точки входа, а библиотеку могут неправильно использовать из вызывающего кода — для этого пришлось бы специфицировать требования к каждому публичному вызову.
Вывод: верификация пройдёт путь от «прикрученной сбоку» к встроенной, как статические типы и тестовые фреймворки, и вскоре станет такой же обыденной, как фаззинг.