NEAR нацеливается на безопасность протокола после запуска генерации доказательств на $112 с использованием ИИ

NEAR Protocol изложил планы по применению формальной верификации с помощью ИИ к своему протоколу и основным смарт-контрактам после сообщения о решении 672 математических задач при стоимости модели на момент подачи в $111.85.

Резюме

• NEAR планирует применить формальную верификацию с помощью ИИ к своему протоколу и основным смарт-контрактам.
• NEAR AI сообщил о решении 672 задач PutnamBench при стоимости модели на момент подачи в $111.85.
• Производственная верификация требует точных моделей программного обеспечения, определенных требований и доказательств, охватывающих развернутую реализацию.
• Формальная верификация дополняет тестирование и ревью кода, с гарантией, ограниченной определенными свойствами и предположениями.

NEAR Protocol заявил в объявлении от 16 октября, что его исследования направлены на снижение специализированной работы и вычислительных затрат, связанных с доказательством того, что программное обеспечение соответствует установленным правилам.

Формальная верификация доказывает, что программное обеспечение соответствует установленным правилам.

Наша цель — сделать это доступным для большего числа разработчиков. Прогресс NEAR AI в автоматической генерации доказательств приближает нас к этому.

Далее: применение этого к протоколу NEAR и основным смарт-контрактам. https://t.co/MqFxz4B166
--- NEAR Protocol (@NEARProtocol) 19 октября 2026 года

Запланированное применение охватывает протокол сети и основные контракты, а также инструменты для разработчиков экосистемы. NEAR описал производственную верификацию как цель, в то время как его завершенная работа по бенчмаркам касается автоматической генерации математических доказательств.

NEAR планирует перенести генерацию доказательств в производственное программное обеспечение

Согласно объявлению NEAR, применение исследований к работающему программному обеспечению включает три этапа. Разработчики должны представить программу математически, определить свойства, которые она должна удовлетворять, и построить доказательства, показывающие, что эти свойства выполняются.

Недавние результаты бенчмарка NEAR AI демонстрируют прогресс на третьем этапе. В объявлении говорится, что производственная работа все еще требует точных моделей поведения программного обеспечения и четкой связи между доказательствами и реализацией, на которую полагаются пользователи.

В своем объяснении NEAR различает доказательство, охватывающее конкретное правило учета, от гарантии того, что все приложение безопасно. Контракт может сохранять балансы во время переводов, требуя при этом отдельного доказательства, что только авторизованные аккаунты могут их инициировать.

Соучредитель NEAR Илья Полосухин связал исследования с рисками от программного обеспечения, сгенерированного ИИ, и инструментами, которые помогают злоумышленникам выявлять уязвимости.

"Будущее ИИ и кода, сгенерированного ИИ, захватывающе — но только после того, как мы достигнем проверяемых и математических гарантий его поведения."

Объявление воспроизводит заявление из написанного Полосухиным о безопасности программного обеспечения. NEAR утверждает, что формальная верификация должна дополнять тестирование, ревью кода и практики операционной безопасности.

Результат в $111.85 измеряет математические доказательства

Объявление NEAR сообщает, что его ИИ-агент решил 672 задачи Lean из PutnamBench, бенчмарка, основанного на математическом конкурсе для студентов Putnam. Сообщаемая средняя стоимость составила примерно $0.17 за задачу по ценам модели, использованным для подачи.

Общественный репозиторий проекта описывает результат как 670 исходных задач плюс исправленные версии двух задач с дефектными формализациями. NEAR утверждает, что сообщенные расходы не включают полную стоимость разработки системы и не оценивают цену верификации производственного контракта.

В репозитории команда сообщает, что повторное использование того же использования по более поздним ценам DeepSeek в нерабочее время обойдется в $331. Его методология включает неудачные попытки, хотя авторы выделяют отдельный параллельный эксперимент с использованием Kimi, который они исключили из учета затрат.

Репозиторий описывает проверки против незавершенных доказательств и изменения в математическом утверждении, которое необходимо доказать. Сообщается, что самая длительная сессия длилась более трех дней.

Вместе с PutnamBench команда NEAR заявляет, что заняла первое место по общему количеству решений на таблице лидеров Lean Eval v1. В объявлении уточняется, что это измерение рейтинга отличается от первых решений и уникальных решений.

Согласно NEAR, математические эталоны проверяют способность, необходимую для верификации программного обеспечения, поскольку разработчики переводят требования к программному обеспечению в математические утверждения. Компания отделяет эти результаты от работы по доказательству свойств развернутого кода.

Формальные доказательства зависят от правил, которые выбирают разработчики

В примере передачи NEAR обычный тест проверяет выбранную транзакцию, такую как перемещение пяти токенов между двумя счетами. Доказательство может установить, что каждая успешная передача, охваченная математической моделью, сохраняет совокупный баланс счетов.

В объявлении объясняется, что разработчики сначала выбирают требование, выражают соответствующее поведение программного обеспечения математически и представляют предложенное доказательство проверяющему. Полученная гарантия зависит от используемых определений и предположений.

Подход NEAR использует Lean, язык программирования с открытым исходным кодом и помощник по доказательствам. AI-агент может предложить доказательство, запустить Lean, проверить его обратную связь и пересмотреть попытку, в то время как ядро Lean проверяет, соответствует ли доказательство его логическим правилам.

Неудачная попытка не обязательно указывает на недостаток программного обеспечения, согласно NEAR. Требование может быть неверным, реализация может его нарушать, или агент может не найти действительное доказательство.

Формальная верификация уже имеет задокументированные приложения в экосистеме NEAR. Оценка Certora от 30 марта Templar, протокола кредитования, развернутого на NEAR, описывает ручной обзор его контрактов на Rust и формальную спецификацию и верификацию его рыночного контракта. Страница оценки Certora определяет доказанные свойства и обнаруженные проблемы как предметы полного отчета.

Другие команды блокчейна стремились к верификации с помощью AI

В мае Aptos Labs описала поддержку верификации с помощью AI, связанной с динамической диспетчеризацией в контрактах Move. Согласно освещению объявления, их рабочий процесс использует спецификации, сгенерированные AI, с Move Prover.

Сооснователь Ethereum Виталик Бутерин обсуждал аналогичное сочетание инструментов AI и проверок, выполненных машиной. Как ранее сообщалось в crypto.news, его комментарии в мае определили приложения по всей дорожной карте Ethereum, включая консенсус, криптографию, устойчивую к квантовым атакам, и системы с нулевым разглашением.

Бутерин предостерег, что доказательство одного уровня не устанавливает, что вся система ведет себя так, как задумано. Его обсуждение охватывало верификацию от высокоуровневых спецификаций до реализации на более низком уровне.

Отдельные исследования безопасности NEAR касались подписания, устойчивого к квантовым атакам. Предложение Near One в мае выбрало поддержку подписей FIPS-204, используя стандарт ML-DSA, одобренный Национальным институтом стандартов и технологий США.

Предложение мая описывало целевой тестнет на конец второго квартала 2026 года. Near One заявила, что программное обеспечение для кошельков, аппаратные кошельки, конечные точки и API потребуют согласованных изменений для поддержки новых схем подписания.