NEAR Protocol объявил о переводе технологии автоматизированного доказательства теорем из исследовательской плоскости в производственную. Команда планирует применять ИИ-формальную верификацию к самому протоколу NEAR и ключевым смарт-контрактам, а также предоставить инструменты разработчикам экосистемы.
Согласно сообщению от 16 октября, исследовательская часть сосредоточена на снижении затрат на доказательство того, что программное обеспечение следует заданным правилам. В бенчмарке PutnamBench, основанном на студенческой олимпиаде имени Патнэма, ИИ-агент NEAR решил 672 задачи при стоимости модельного запуска $111,85, то есть в среднем около $0,17 за задачу. В публичном репозитории уточняется, что результат включает 670 исходных задач и две исправленные версии с некорректной формализацией. Повторное воспроизведение того же объема вычислений по более поздним внепиковым тарифам DeepSeek обошлось бы в $331, а методология учитывает и неудачные попытки; самый длительный прогон занял более трех суток.
В NEAR подчеркивают, что математические бенчмарки отражают лишь способность, необходимую для верификации ПО, но не тождественны проверке развернутого кода. Для промышленного применения требуется представить программу математически, определить свойства, которым она должна удовлетворять, и построить доказательства, покрывающие именно ту реализацию, которую используют пользователи. Формальная верификация рассматривается как дополнение к тестированию, код-ревью и практикам операционной безопасности. Гарантии ограничены выбранными спецификациями и допущениями: например, доказательство сохранения балансов при переводах не означает, что только авторизованные счета могут инициировать транзакции.
Сооснователь NEAR Илья Полосухин связал исследования с рисками кода, генерируемого ИИ, и инструментов, которые помогают злоумышленникам находить уязвимости. «Будущее ИИ и созданного им кода впечатляет, но лишь после того, как мы получим проверяемые математические гарантии его поведения», — приводятся его слова в анонсе.
Помимо PutnamBench, команда заняла первое место по общему числу решений в лидерборде Lean Eval v1. В репозитории отмечается, что самый длительный запуск длился более трех дней, а проверка учитывает незавершенные доказательства и изменения доказываемых утверждений. Отдельно NEAR выделяет, что расходы $111,85 не включают полную стоимость разработки системы и не являются оценкой цены верификации производственного контракта.
Инициатива дополняет более ранние шаги NEAR в области безопасности. В мае Near One предложил поддержку подписей FIPS-204 на базе стандарта ML-DSA, одобренного Национальным институтом стандартов и технологий США, с целевым запуском в тестнете к концу второго квартала 2026 года. В экосистеме уже есть примеры формальной верификации: в конце марта Certora оценивала кредитный протокол Templar на NEAR, включая ручной анализ Rust-контрактов и формальную спецификацию рыночного контракта. Похожие подходы обсуждают и другие блокчейн-команды: Aptos Labs в мае описывала поддержку ИИ-верификации в Move-контрактах, а сооснователь Ethereum Виталик Бутерин говорил о сочетании ИИ-инструментов и машинно-проверяемых доказательств для консенсуса, квантово-устойчивой криптографии и zero-knowledge систем.
В NEAR рассчитывают, что снижение стоимости специализированного труда и вычислительных ресурсов сделает формальную верификацию доступной большему числу разработчиков, ускорит развитие экосистемы и укрепит безопасность протокола и базовых смарт-контрактов.
