Команда Frontier Red Team компании Anthropic совместно с Theorem Labs применила модели Claude для проведения формальной верификации 123 библиотек с открытым исходным кодом. Работа заняла несколько недель, тогда как ранее подобные задачи требовали многолетних усилий специалистов.
Верификация проводится на уровне ассемблера, что позволяет анализировать низкоуровневые инструкции, исполняемые процессором. Такой подход дает математическое доказательство соответствия кода заданным свойствам безопасности, в отличие от традиционных методов тестирования, которые лишь выявляют ошибки.
Проект является частью стратегии Anthropic по развитию инструментов защиты открытого ПО, включая инициативу OSS Scanner. Ранее команда проанализировала 25 проектов с открытым кодом, охватив более 5 миллионов строк кода на языках C, C++, Java, PHP и Python.
В ходе предыдущего анализа было обнаружено 493 проблемы, включая критические уязвимости и 94 случая отключения механизмов безопасности. Исследователи стремятся перевести стандарты киберзащиты от простого тестирования к формальному доказательству корректности кода.
