El cofundador de Ethereum, Vitalik Buterin, propuso un nuevo lenguaje de programación. Compilaría directamente en Lean o HOL, otro asistente de prueba formal.
La idea apunta a una brecha específica en cómo las personas leen la salida de la IA. La inteligencia artificial produce cada vez más grandes bloques de pruebas automatizadas, a menudo más rápido de lo que cualquier equipo humano podría escribirlas a mano. Pocos lectores pueden confirmar rápidamente lo que esas pruebas realmente establecen.
Un lenguaje construido solo para lectores de pruebas de IA
Lean es un asistente de prueba, un software que los matemáticos e ingenieros utilizan para escribir pruebas que una computadora puede verificar línea por línea. Los investigadores de Ethereum ya lo utilizan para verificar código criptográfico y lógica de consenso. Los asistentes de prueba han existido durante casi 60 años, sin embargo, el campo ha permanecido como una búsqueda de nicho.
En su publicación, Buterin argumentó que los pasos internos de una prueba solo tienen un requisito. Ese requisito es la corrección matemática, nada más. Los lectores nunca inspeccionan esa maquinaria directamente. Las definiciones y los teoremas funcionan de manera diferente, ya que los humanos leen esas partes para aprender lo que un software realmente garantiza.
Buterin exploró una división relacionada en una publicación de blog de mayo. Allí, una prueba matemática muestra que el código eficiente de bajo nivel coincide con una especificación separada y legible, por lo que una sola auditoría cubre ambas versiones a la vez.
Su cronograma también coincide con el propio esfuerzo de reconstrucción de Ethereum, que lleva un apodo separado, la hoja de ruta Lean Ethereum. Mientras tanto, los investigadores están construyendo un ZK-EVM formalmente verificado, una versión de la máquina virtual de Ethereum (EVM) que se puede probar con conocimiento cero, utilizando métodos comparables.
La IA escribe las pruebas, los humanos verifican las afirmaciones
Los modelos de lenguaje grandes ya pueden escribir pruebas Lean utilizables. Buterin ha nombrado a Claude y Deepseek 4 Pro como herramientas capaces, junto con Leanstral, un modelo más pequeño ajustado específicamente para Lean. Un proyecto de ejemplo es evm-asm, una implementación de EVM verificada contra una referencia legible. Esa capacidad refleja las habilidades de razonamiento que los desarrolladores mostraron en un reciente desafío de IA de Buterin. Los evaluadores resolvieron ese desafío en pocas horas.
Sin embargo, las apuestas van más allá de la conveniencia. Los investigadores de seguridad han rastreado un aumento en los intentos de explotación asistidos por IA este año. El código formalmente verificado ofrece una defensa contra esa tendencia. Un lenguaje de especificación más amigable permitiría a los desarrolladores auditar afirmaciones sin tener que sumergirse en la prueba circundante.
Más allá de los círculos de investigación de Ethereum
Buterin sigue probando estas ideas en público, ya que recientemente demostró una valla publicitaria anónima construida con pruebas de conocimiento cero. La demostración mostró cómo las afirmaciones verificables pueden pasar de los repositorios de investigación a productos en funcionamiento. Los investigadores también han comenzado a verificar formalmente los clientes de consenso en Lean para detectar errores temprano.
Aún así, la dirección refleja un patrón familiar: separar el código rápido de las afirmaciones legibles, y luego probar que ambos coinciden.
Aún no existe un prototipo del nuevo lenguaje, y Buterin dejó abierta la sintaxis exacta. Los desarrolladores pueden converger en un estándar compartido, o conformarse con varios dialectos incompatibles. Esa elección podría determinar qué tan rápido el código verificado por IA llega a los sistemas de producción.
Fuente: BeInCrypto
