DeepMind написал 3 млн строк кода на Lean для верификации Signal

Исследовательское подразделение DeepMind объявило о создании AlphaProof Code — системы на основе искусственного интеллекта, способной автоматически писать формальные доказательства корректности программного кода. В рамках эксперимента агенты AlphaProof Code сгенерировали три миллиона строк доказательств на языке Lean, чтобы проверить ядро шифрования популярного мессенджера Signal. Это первая в истории демонстрация того, что ИИ может верифицировать реальный криптографический код в таком объёме.

Lean — это язык и среда для формальной верификации, где каждое утверждение о работе программы должно быть строго доказано математически. Работа с ним обычно требует высокой квалификации в области математической логики и занимает много времени. AlphaProof Code автоматизировала этот процесс: агенты (автономные программы, выполняющие задачу без постоянного контроля человека) самостоятельно написали и проверили доказательства для всех ключевых компонентов шифрования Signal.

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