Проверять можно не только тестами
Google DeepMind представила AlphaProof Code — систему формальной проверки программ. В демонстрации она исследовала криптографическое ядро Signal: вместо перебора отдельных примеров система строит математические доказательства того, что код соответствует заданным свойствам.
По данным разработчиков, работа заняла четыре недели и привела к созданию около шести миллионов строк доказательств на языке Lean. Люди формулировали и проверяли требования, а агенты помогали строить доказательства. Их корректность затем проверял отдельный механизм Lean.
Три этапа проверки: требования, скомпилированный код и доказательство. Схема Google DeepMind.
Почему требования важнее красивой цифры
Формальная проверка отвечает на конкретный вопрос: выполняется ли описанное свойство при указанных предпосылках. Если требование неполное, доказательство не охватит пропущенный риск. Проверка криптографического ядра также не равна аудиту всего приложения, операционной системы или устройства.
В эксперименте команда вернула две ранее исправленные ошибки в изолированную тестовую версию. Система смогла показать нарушение свойств. Это проверка метода на известном примере, а не сообщение о двух новых уязвимостях в актуальном Signal.
Официальная иллюстрация AlphaProof Code. Google DeepMind.
Что это меняет для разработчиков
Особенно интересна возможность проверять свойства скомпилированного кода, а не только удобную теоретическую модель алгоритма. DeepMind опубликовала технические материалы и артефакты проверки, чтобы результат можно было изучать.
Для пользователя главный вывод спокойный: продолжать обновлять приложения и защищать устройства. Для инженеров — следить, насколько такие инструменты снижают стоимость строгой проверки критичных компонентов и позволяют независимым командам повторить результат.
