🚀️️️️️️ Google DeepMind математически доказала безопасность кода Signal с помощью ИИ. 6,5 млн строк доказательств за четыре недели. Исследователи представили AlphaProof Code - мультиагентную систему, которая проверила криптографическую реализацию Signal вплоть до машинного кода, исполняемого процессором. Что удалось сделать: - 40-80 ИИ-агентов на базе Gemini 4 Carbon работали над доказательствами. - Сгенерировано около 6,5 млн строк Lean-кода. - Проверены свойства конфиденциальности сообщений, аутентификации и прямой секретности (Forward Secrecy). - Работа заняла четыре недели вместо нескольких лет, которые потребовались бы экспертам с прежними инструментами. Почему это принципиально важно? Обычные тесты проверяют отдельные сценарии. Формальная верификация математически доказывает выполнение заданных свойств для всех случаев в рамках модели. При этом доверять самим ИИ-агентам не требуется: каждый шаг доказательства проверяет ядро Lean. Специалисты определяют требования безопасности и проверяют формальные спецификации. Исследователи также вернули в копию проекта две ранее исправленные уязвимости. В обоих случаях система смогла математически доказать нарушение безопасности. Проверялся скомпилированный код libsignal для AArch64, а не все приложения Signal целиком. Код, спецификации и доказательства открыты: https://github.com/google-deepmind/code-verification Исследование: https://google-deepmind.github.io/code-verification/ @data_analysis_ml