Vitalik Buterin quiere un nuevo lenguaje que se compile a Lean o HOL.
El lenguaje se dirigiría únicamente a definiciones y teoremas, no a los pasos de la demostración.
Buterin dice que los reclamos legibles ayudan a los humanos a verificar los blobs de prueba generados por IA.

El cofundador de Ethereum, Vitalik Buterin, propuso un nuevo lenguaje de programación. Este lenguaje compilaría directamente en Lean o HOL, que son asistentes de pruebas formales.

La idea apunta a una necesidad específica en la forma en que las personas leen los resultados generados por la inteligencia artificial. La inteligencia artificial crea cada vez más bloques grandes de pruebas automatizadas, muchas veces más rápido que cualquier grupo de humanos podría hacerlo a mano. Pocos lectores pueden confirmar rápidamente lo que realmente prueban esas demostraciones.

Un lenguaje creado solo para lectores de pruebas de IA

Lean es un asistente de pruebas, un software que matemáticos e ingenieros usan para escribir demostraciones que una computadora puede revisar línea por línea.

Los investigadores de Ethereum ya lo usan para verificar código criptográfico y la lógica de consenso. Los asistentes de pruebas existen desde hace casi 60 años, pero esta área sigue siendo una actividad de nicho.

A new type of "high-level programming language" that seems really worth trying to make, is a language that gets compiled to Lean (or HOL, or…) that is specifically about making it as friendly as possible for a human to read definitions and theorems.Not the proofs – as all…
— vitalik.eth (@VitalikButerin) July 21, 2026

En su publicación, Buterin explicó que los pasos internos de una prueba solo tienen un requisito: que sean matemáticamente correctos, nada más. Los lectores nunca revisan directamente ese mecanismo interno. Las definiciones y los teoremas sí funcionan diferente, porque los humanos leen esas partes para entender qué garantiza realmente un software.

Buterin exploró una separación relacionada en una entrada de blog en mayo. Allí, una prueba matemática muestra que un código eficiente de bajo nivel corresponde con una especificación separada y legible, por lo que una sola auditoría cubre ambas versiones a la vez.

El momento de Buterin también coincide con el propio esfuerzo de reconstrucción de Ethereum, que tiene un apodo propio: la Lean Ethereum roadmap.

Al mismo tiempo, los investigadores están creando una ZK-EVM verificada formalmente, una versión de la máquina virtual de Ethereum (EVM) capaz de demostrar conocimiento cero, usando métodos comparables.

La IA escribe las pruebas, los humanos revisan las afirmaciones

Los modelos de lenguaje de gran tamaño ya pueden escribir pruebas válidas en Lean. Buterin mencionó Claude y Deepseek 4 Pro como herramientas adecuadas, junto con Leanstral, que es un modelo más pequeño optimizado para Lean.

Un proyecto como ejemplo es evm-asm, una implementación de la EVM verificada respecto a una referencia legible. Esta capacidad se asemeja a las habilidades de razonamiento que los desarrolladores mostraron en un reciente reto con IA de Buterin. Los testers resolvieron ese reto en pocas horas.

Sin embargo, las implicaciones van más allá de la comodidad. Los investigadores de seguridad han notado un aumento en los intentos de exploit asistidos por IA este año.

El código verificado formalmente es una defensa ante esa tendencia. Un lenguaje de especificación más amigable permitiría a los desarrolladores auditar las afirmaciones sin tener que leer toda la prueba técnica.

Más allá de los círculos de investigación de Ethereum

Buterin sigue probando estas ideas en público; recientemente hizo una demostración de una cartelera anónima basada en pruebas de conocimiento cero.

La demostración mostró cómo las afirmaciones verificables pueden pasar de los repositorios de investigación a productos funcionales. Además, los investigadores han empezado a verificar formalmente los clientes de consenso en Lean para detectar errores temprano.

Aun así, la dirección repite un patrón conocido: separar el código rápido de las afirmaciones legibles, y luego probar que ambos coinciden.

Todavía no existe ningún prototipo del nuevo lenguaje y Buterin dejó abierta la sintaxis exacta. Los desarrolladores podrían llegar a un estándar común, o bien quedarse con varios dialectos incompatibles. Esa decisión podría determinar qué tan rápido el código verificado por IA llegue a sistemas en producción.

Leer el artículo en BeInCrypto