Google представила AlphaProof Code, систему ИИ-агентов, которая проверяет программный код с помощью математических доказательств. Первым крупным испытанием стал криптографический протокол Signal, защищающий переписку миллиардов пользователей. Обычно формальная верификация проверяет математическую модель протокола. Но ошибки могут появиться уже при реализации. AlphaProof Code пошёл дальше и проверил, что скомпилированный код действительно обеспечивает заявленные свойства безопасности. Агенты на базе Gemini Carbon за 4 недели сгенерировали более 6 млн строк доказательств на Lean. Каждое доказательство автоматически проверялось системой Lean, поэтому экспертам потребовалось дополнительно изучить только 1% кодовой базы. Для проверки метода исследователи специально вернули две ранее исправленные уязвимости. Система в обоих случаях смогла математически доказать, что изменённый код небезопасен. По данным Google, это первая формальная верификация реализации настолько широко используемого криптографического протокола на подобной глубине. https://deepmind.google/blog/introducing-alphaproof-code/