Anthropic заявила, что вместе с Theorem использовала Claude для математического доказательства свойств безопасности более 100 реально используемых библиотек с открытым исходным кодом. Проверка касалась уровня ассемблера — низкоуровневых инструкций программы. Речь о конкретных свойствах кода, а не о гарантии полной защищённости этих библиотек.
Что именно заявила Anthropic
В центре проекта — программные библиотеки: готовые компоненты, которые разработчики используют в своих приложениях. По заявлению Anthropic, работа с Theorem охватила более 100 таких компонентов из реальных открытых проектов. Claude применяли для формального доказательства свойств их безопасности.
Формальное доказательство — это математическое обоснование того, что код удовлетворяет заданному условию. Его смысл отличается от обычного тестирования: проверить поведение на отдельных примерах и доказать определённое свойство — не одно и то же. При этом принципиально, какое именно условие доказывали и при каких предпосылках.
Почему важен уровень проверки
В заявлении отдельно указан уровень ассемблера. Если исходный код можно представить как описание действий для разработчика, то здесь речь идёт о низкоуровневых инструкциях, близких к тому, что выполняет процессор. Именно к этому уровню относится заявленный результат; переносить его на все стороны работы приложения нельзя.
Число «более 100» описывает охват библиотек. Оно не означает число найденных уязвимостей, исправленных ошибок или предотвращённых атак. В доступном сообщении такие результаты не перечислены. Не названы и конкретные библиотеки, доказанные свойства, версия Claude или распределение задач между моделью и участниками проекта.
Что это означает для читателя
Самая важная граница здесь — между доказанным свойством и безопасностью программы в целом. Из заявления нельзя заключить, что перечисленные компоненты защищены от любых атак или что приложения на их основе не нуждаются в других проверках. Для оценки конкретного результата нужны сами условия доказательства и описание охваченного кода.
Это также не сообщение о новой функции, которую уже можно включить в обычном чате Claude. Сведения о доступности такого процесса для сторонних пользователей в сообщении не приведены.
У Anthropic есть и отдельное направление работы с исследователями безопасности: ранее мы рассказывали, как компания расширила доступ к Claude для специалистов по безопасности и ослабила часть ограничений. Это другой сюжет: условия доступа к инструменту не следует путать с результатами совместного проекта с Theorem.
