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, мову програмування з відкритим кодом та асистента доказів. Агента ШІ може запропонувати доказ, запустити Lean, перевірити його відгук і переглянути спробу, в той час як ядро Lean перевіряє, чи слідує доказ його логічним правилам.

Неуспішна спроба не обов'язково вказує на дефект програмного забезпечення, згідно з NEAR. Вимога може бути неправильною, реалізація може її порушувати, або агент може не знайти дійсний доказ.

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

Інші команди блокчейну прагнули до верифікації з підтримкою ШІ

У травні Aptos Labs описали підтримку формальної верифікації з підтримкою ШІ, що стосується динамічної диспетчеризації в контрактах Move. Згідно з повідомленням про анонс, їхній заявлений робочий процес використовує специфікації, згенеровані ШІ, з Move Prover.

Співзасновник Ethereum Віталік Бутерін обговорював подібну комбінацію інструментів ШІ та машинно перевірених доказів. Як раніше повідомляло crypto.news, його коментарі в травні вказували на застосування в дорожній карті Ethereum, включаючи консенсус, квантово-стійку криптографію та системи нульових знань.

Бутерін застеріг, що доведення одного шару не встановлює, що вся система працює так, як задумано. Його обговорення охоплювало верифікацію від високорівневих специфікацій до реалізації нижчого рівня.

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

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