NEAR se centra en la seguridad del protocolo tras una ejecución de generación de pruebas de IA de 112 dólares

NEAR Protocol ha delineado planes para aplicar verificación formal asistida por IA a su protocolo y contratos inteligentes centrales después de informar sobre 672 problemas matemáticos resueltos a un costo de modelo de tiempo de presentación de 111,85 dólares.

Resumen

• NEAR planea aplicar verificación formal asistida por IA a su protocolo y contratos inteligentes centrales.
• NEAR AI informó haber resuelto 672 problemas de PutnamBench a un costo de modelo de tiempo de presentación de 111,85 dólares.
• La verificación de producción requiere modelos de software precisos, requisitos definidos y pruebas que cubran la implementación desplegada.
• La verificación formal complementa las pruebas y revisiones de código, con garantías limitadas a propiedades y suposiciones especificadas.

NEAR Protocol dijo en un anuncio del 16 de octubre que su investigación busca reducir el trabajo especializado y los costos computacionales involucrados en demostrar que el software sigue reglas definidas.

La verificación formal prueba que el software sigue reglas definidas.

Nuestro objetivo es hacerlo asequible para más desarrolladores. El progreso de NEAR AI en la generación automática de pruebas nos acerca.

Próximo: aplicarlo al protocolo NEAR y a los contratos inteligentes centrales. https://t.co/MqFxz4B166
--- NEAR Protocol (@NEARProtocol) 19 de octubre de 2026

La aplicación planificada cubre el protocolo de la red y los contratos centrales, junto con herramientas para desarrolladores del ecosistema. NEAR describió la verificación de producción como un objetivo, mientras que su trabajo de referencia completado se refiere a la generación automática de pruebas matemáticas.

NEAR planea llevar la generación de pruebas al software de producción

Según el anuncio de NEAR, aplicar la investigación al software en funcionamiento implica tres etapas. Los desarrolladores deben representar un programa matemáticamente, definir las propiedades que debe satisfacer y construir pruebas que demuestren que esas propiedades se mantienen.

Los recientes resultados de referencia de NEAR AI demuestran avances en la tercera etapa. El anuncio dice que el trabajo de producción aún requiere modelos precisos del comportamiento del software y una conexión clara entre las pruebas y la implementación en la que los usuarios confían.

En su explicación, NEAR distingue una prueba que cubre una regla contable particular de una garantía de que toda la aplicación es segura. Un contrato podría preservar saldos durante las transferencias mientras requiere una prueba separada de que solo las cuentas autorizadas pueden iniciarlas.

El cofundador de NEAR, Illia Polosukhin, ha vinculado la investigación a los riesgos del software generado por IA y las herramientas que ayudan a los atacantes a identificar debilidades.

"El futuro de la IA y el código generado por IA es emocionante, pero solo una vez que logremos garantías verificables y matemáticas de su comportamiento."

El anuncio reproduce la declaración del escrito de Polosukhin sobre la seguridad del software. NEAR dice que la verificación formal debe complementar las pruebas, la revisión de código y las prácticas de seguridad operativa.

El resultado de 111,85 dólares mide pruebas matemáticas

El anuncio de NEAR informa que su agente de IA resolvió 672 problemas Lean de PutnamBench, un referente basado en la competencia de matemáticas de pregrado de Putnam. El costo medio informado fue de aproximadamente 0,17 dólares por problema a los precios del modelo utilizados para la presentación.

El repositorio público del proyecto describe el resultado como 670 problemas de upstream más versiones corregidas de dos problemas con formalizaciones defectuosas. NEAR dice que el gasto informado excluye el costo total de desarrollar el sistema y no estima el precio de verificar un contrato de producción.

En el repositorio, el equipo informa que reproducir el mismo uso a precios fuera de pico de DeepSeek listados más tarde costaría 331 dólares. Su metodología incluye intentos fallidos, aunque los autores identifican un experimento paralelo separado utilizando Kimi que excluyeron de la contabilidad de costos.

El repositorio describe verificaciones contra pruebas incompletas y cambios en la declaración matemática que se está probando. Informa que la ejecución más larga duró más de tres días.

Junto a PutnamBench, NEAR afirma que su equipo alcanzó el primer lugar por total de soluciones en la tabla de clasificación de formalización Lean Eval v1. El anuncio especifica que esta medida de clasificación la distingue de las primeras soluciones y soluciones únicas.

Según NEAR, los puntos de referencia matemáticos ejercen una capacidad necesaria para la verificación de software porque los desarrolladores traducen los requisitos del software en declaraciones matemáticas. La empresa separa esos resultados del trabajo de prueba de propiedades del código desplegado.

Las pruebas formales dependen de las reglas que eligen los desarrolladores

En el ejemplo de transferencia de NEAR, una prueba convencional verifica una transacción seleccionada, como mover cinco tokens entre dos cuentas. Una prueba puede establecer que cada transferencia exitosa cubierta por el modelo matemático preserva el saldo combinado de las cuentas.

El anuncio explica que los desarrolladores primero eligen un requisito, expresan el comportamiento relevante del software matemáticamente y envían una prueba propuesta a un verificador. La garantía resultante depende de las definiciones y suposiciones utilizadas.

El enfoque de NEAR utiliza Lean, un lenguaje de programación de código abierto y asistente de prueba. Un agente de IA puede proponer una prueba, ejecutar Lean, inspeccionar su retroalimentación y revisar el intento, mientras que el núcleo de Lean verifica si la prueba sigue sus reglas lógicas.

Un intento fallido no necesariamente identifica un defecto en el software, según NEAR. El requisito puede ser incorrecto, la implementación puede violarlo o el agente puede no encontrar una prueba válida.

La verificación formal ya tiene aplicaciones documentadas dentro del ecosistema de NEAR. La evaluación de Certora del 30 de marzo sobre Templar, un protocolo de préstamos desplegado en NEAR, describe la revisión manual de sus contratos en Rust y la especificación y verificación formal de su contrato de mercado. La página de evaluación de Certora identifica las propiedades probadas y los problemas descubiertos como temas del informe completo.

Otros equipos de blockchain han perseguido la verificación asistida por IA

En mayo, Aptos Labs describió el apoyo a la verificación formal asistida por IA que involucra el despacho dinámico en contratos Move. Su flujo de trabajo declarado utiliza especificaciones generadas por IA con Move Prover, según la cobertura del anuncio.

El cofundador de Ethereum, Vitalik Buterin, ha discutido una combinación similar de herramientas de IA y pruebas verificadas por máquina. Como informó anteriormente crypto.news, sus comentarios de mayo identificaron aplicaciones a lo largo de la hoja de ruta de Ethereum, incluyendo consenso, criptografía resistente a cuántica y sistemas de conocimiento cero.

Buterin advirtió que probar una capa no establece que todo el sistema se comporte como se pretende. Su discusión abarcó la verificación desde especificaciones de alto nivel hasta la implementación de bajo nivel.

La investigación de seguridad separada de NEAR ha abordado la firma resistente a cuántica. La propuesta de Near One de mayo seleccionó el soporte de firma FIPS-204, utilizando el estándar ML-DSA aprobado por el Instituto Nacional de Estándares y Tecnología de EE. UU.

La propuesta de mayo describió un objetivo de testnet para finales del segundo trimestre de 2026. Near One dijo que el software de billetera, las billeteras de hardware, los puntos finales y las API requerirían cambios coordinados para apoyar los nuevos esquemas de firma.