" Стартап Math, созданный экс-сооснователем xAI, полностью формализовал доказательство безопасности протокола FRI — ключевого компонента STARK-систем доказательств с нулевым разглашением.
Работа выполнена на языке Lean 4 с помощью их автоформализационного агента Gauss.
FRI — это то, на чём держатся современные прозрачные ZK-системы. Без него не было бы ни StarkNet, ни множества других L2-решений.
Почему это важно?
Формальная верификация криптографических протоколов занимает месяцы ручной работы математиков. Gauss справился за дни. Это меняет экономику аудита — можно машинно гарантировать отсутствие ошибок в доказательствах безопасности, а не полагаться на peer review.
Для ZK-инфраструктуры это критично - одна ошибка в доказательстве и вся система скомпрометирована. Теперь есть инструмент, который делает такой аудит доступным.
