62 noticias
El método de verificación formal TLA+ es una herramienta potente para garantizar la corrección de sistemas concurrentes complejos, pero su capacidad de verificación está limitada por la naturaleza de las propiedades que puede expresar. A diferencia de la creencia popular de que resuelve todos los pr
Un equipo de investigación ha desarrollado un modelo de lenguaje de gran escala (LLM) de 27.000 millones de parámetros diseñado para predecir la dificultad de las pruebas matemáticas. El objetivo principal no es solo generar teoremas, sino identificar aquellos que son intrínsecamente interesantes y
El reciente viralizado de un tweet de Boris Cherny que utilizó TLA+ para modelar el Claude Agent SDK ha generado un interés masivo en el uso de modelos formales en la programación asistida por IA. TLA+ (Temporal Logic of Actions) es un lenguaje de especificación que describe el comportamiento tempor
Un equipo de diez agentes de IA, coordinados mediante un tablero de mensajes, ha desarrollado un nuevo algoritmo determinista llamado C-HD para calcular distancias de caminos más cortos en grafos dirigidos con pesos reales no negativos. Este avance, respaldado por una verificación formal completa en
Un laboratorio de investigación en desarrollo, fundado por Shayaan Siddique e Ibrahim Mian, se especializa en la verificación formal de matemáticas y la resolución de problemas científicos abiertos mediante inteligencia artificial. A diferencia de las herramientas actuales que pueden generar pruebas
Bend 2 se presenta como un lenguaje de programación para la era de la IA, donde los humanos definen las leyes y la IA genera las implementaciones y pruebas. Sin embargo, el proyecto presenta un problema fundamental: ignora el campo de la verificación formal, que ya existe y permite probar la correcc
Bend es un lenguaje de programación diseñado para eliminar la ambigüedad en la interacción con agentes de inteligencia artificial, garantizando que el código generado cumpla estrictamente con las especificaciones definidas por el usuario. A diferencia de los lenguajes tradicionales, Bend utiliza un
El 8 de septiembre de 2026, OpenAI anunció haber generado una solución a uno de los Problemas del Milenio, el problema de la existencia y suavidad de Navier-Stokes. Este anuncio provocó un intenso debate sobre la atribución del crédito y la naturaleza de la inteligencia artificial en las matemáticas
Investigadores presentan C*, una extensión del lenguaje C que incorpora de forma nativa capacidades de verificación formal, con el objetivo de acercar las prácticas de demostración de correctitud a los programadores de sistemas. El trabajo, publicado en arXiv el 3 de abril de 2025, aborda una de las
OpenAI publicó una demostración matemática que resuelve una cuestión pendiente sobre las ecuaciones de Navier-Stokes, pero el aspecto más relevante de su trabajo no ha recibido atención: la compañía presentó simultáneamente una prueba formal en Lean 4. Hasta hace poco, elaborar demostraciones formal
Durante su segunda semana en el Recurse Center, Ben Kallus intentó formalizar en Rocq el manual de álgebra abstracta de Dummit y Foote. El primer ejercicio de demostración del libro pide probar que una función es inyectiva si y solo si tiene un inverso izquierdo. Kallus comprobó que el enunciado es
MathKernel es una biblioteca de Python y servidor MCP (protocolo de contexto para modelos) que actúa como núcleo matemático multi-motor diseñado para que los modelos de lenguaje de gran tamaño (LLM, por sus siglas en inglés) puedan realizar cálculos avanzados sin sacrificar el rigor. La herramienta
Anthropic ha publicado en GitHub una demostración completa del último teorema de Fermat verificada por máquina en el asistente de pruebas Lean 4, un hito que combina más de tres décadas de matemáticas avanzadas con las técnicas más recientes de verificación formal automatizada. El repositorio, prese
Artículo explicativo sobre por qué los métodos formales de verificación no pueden aplicarse de forma generalizada al software actual. El autor parte de una hipótesis central: una vez que se dispone de una especificación formal de calidad, verificar un sistema resulta costoso pero no difícil; el verd
Proofcraft ha cerrado la demostración matemática de que el microkernel seL4, en su implementación para AArch64 (ARM de 64 bits), preserva la confidencialidad de los datos. Con las pruebas previas de corrección funcional e integridad ya finalizadas, la empresa culmina así la pila completa de garantía
En 1992, Leslie Lamport, conocido por sus trabajos en sistemas distribuidos y por haber creado LaTeX, publicó una nota titulada "Types Considered Harmful", en la que defendía que los lenguajes de especificación debían basarse en formalismos no tipados (una suerte de teoría de conjuntos) en lugar de
La verificación formal es una labor de ingeniería exigente y las propias herramientas que la realizan también son difíciles de depurar, por lo que deben probarse de forma rigurosa. Alive2 es una herramienta de validación de traducciones para LLVM IR que compara dos versiones de una función —normalme
El matemático Terence Tao anunció la apertura de Palomar, un registro de demostraciones matemáticas verificadas en el lenguaje de pruebas Lean, una iniciativa impulsada por Lean FRO e ICARM. El proyecto surge ante la proliferación de pruebas generadas por inteligencia artificial, algunas formalizada
El artículo repasa los argumentos del clásico paper de 1979 'Social Processes and Proofs of Theorems and Programs', que sostenía que la verificación formal de programas estaba abocada al fracaso, y los contrasta con la situación actual. En 1979, los autores defendían que las demostraciones matemátic
El problema de álgebra de bachillerato planteado por Alfred Tarski pregunta si toda identidad verdadera sobre la suma, la multiplicación y la exponenciación de enteros positivos se deduce a partir de una lista de once identidades elementales. El lógico Alex Wilkie demostró en los años setenta que ex
La liquidación financiera transfronteriza sigue siendo lenta y costosa, con costes medios de remesa en torno al 6% del importe enviado y solo un tercio de los pagos minoristas internacionales liquidándose en menos de una hora. Keeta es una red blockchain de reciente lanzamiento, diseñada para pagos
Depot ha utilizado el lenguaje de especificación formal TLA+ y su model checker TLC para verificar el recolector de basura de Depot Registry v2. El equipo sostiene que los errores más difíciles en sistemas distribuidos no aparecen en una sola operación, sino en intercalados concretos: dos procesos h
Un investigador en métodos formales relata cómo una prueba con la que estuvo meses torturándose casi se viene abajo por un error de signo en el código que, paradójicamente, el comprobador aceptó durante meses sin chistar. El episodio, sucedido durante la fase de rebuttal de un artículo sobre verific
El autor, ingeniero de Trust-in-Soft, describe el trabajo de auditoría estática realizado sobre SQLite, una base de datos ligera de alrededor de 113.000 líneas de código con uso intensivo de punteros, demasiado extensa para una verificación estática trivial pero respaldada por una de las suites de p
TheoremDB es un espacio de trabajo público y colaborativo pensado para la investigación matemática asistida por máquina. Su objetivo es resolver un problema habitual entre los agentes de investigación: la repetición de esfuerzos porque los intentos previos, los resultados parciales y los enfoques fa
F* (pronunciado «F star») es un lenguaje de programación de propósito general orientado a la demostración formal, que combina programación puramente funcional y con efectos. Reúne el poder expresivo de los tipos dependientes con automatización de pruebas basada en resolutores SMT y demostración inte
El kernel de Lean presentó un fallo de solidez (bug #14576) que fue detectado y corregido durante la semana del 27 de julio. El origen fue la publicación, el 25 de julio, de un repositorio con una aparente refutación de la conjetura de Collatz generada con ayuda de IA y sin "sorry", obra de Ramana K
OpenAI ha presentado diez nuevos resultados en matemáticas e informática teórica obtenidos con una versión interna de su próximo modelo principal, Astra, por un coste estimado de unos 2.000 dólares en tokens. Los avances abarcan geometría de altas dimensiones, teoría de códigos, complejidad de circu
Los métodos formales —herramientas matemáticas para especificar y verificar software— apenas se utilizan fuera de nichos académicos y de alta seguridad. Un análisis extenso repasa las razones históricas y estructurales de esta baja adopción y propone una mirada más matizada que los tópicos habituale
SpecForge es una herramienta orientada a la especificación y el análisis de sistemas híbridos mediante el lenguaje Lilo, un lenguaje de expresiones con operadores de lógica temporal como always, eventually, past e historically, que admiten intervalos de tiempo para acotar las condiciones. Sus especi
Los verificadores de tipos no solo evitan errores de programación como sumar cadenas y enteros, sino que además sustentan los asistentes de demostración, lenguajes como Lean y Rocq que validan matemáticamente teoremas. La base de esa capacidad es la correspondencia de Curry-Howard, que establece una
El repositorio "verified-3d-mesh-intersection", publicado por schildep en GitHub, presenta la que su autor describe como la primera implementación formalmente verificada de una operación de geometría sólida constructiva (CSG): la intersección de mallas 3D, codificada en Lean 4 y validada contra una
La plataforma de pruebas Antithesis ha identificado errores en todas las implementaciones del protocolo de consenso Raft que ha analizado, entre ellas HashiCorp Raft, Aeron Cluster, OpenRaft y MicroRaft. Los fallos detectados violan la principal invariante del algoritmo, conocida como seguridad de l
El ingeniero y criptógrafo conocido como imperialviolet —figura vinculada al proyecto de navegador Chromium de Google— ha presentado esta semana un experimento singular: un descompresor completo del algoritmo Zstandard (zstd) implementado y verificado formalmente en el lenguaje de programación depen
El proyecto lean-zip, una implementación del algoritmo de compresión DEFLATE escrita en el lenguaje de programación Lean, consigue resultados de compresión más rápidos y con mejor ratio que miniz_oxide, la implementación de referencia en Rust puro. Sobre el corpus estándar Silesia (212 MB), lean-zip
Xavier Leroy, investigador francés del Inria y creador del lenguaje de programación OCaml, protagoniza una entrevista en profundidad en el podcast The Peterman Pod, conducido por Ryan Peterman. El episodio, de una hora y veinticuatro minutos, recorre la trayectoria de Leroy en compiladores, lenguaje
Un equipo de la empresa Basis ha empleado modelos de lenguaje de gran tamaño (LLM) para verificar formalmente el compilador y optimizador de nftables, el cortafuegos integrado en el núcleo de Linux desde 2014. Durante el proceso, en el que reimplementaron la herramienta en el asistente de pruebas Ro
La verificación formal permite demostrar la corrección de enunciados matemáticos escribiendo la prueba en código para que un programa la valide mecánicamente. Entre las herramientas disponibles se encuentran Rocq (antes Coq), Isabelle y Lean, esta última creada en 2013 por Leonardo de Moura en Micro
Un investigador de UC Berkeley, Phillip Kerger, logró que el modelo GPT-5.6 Sol Pro de OpenAI generara en una sola sesión ininterrumpida de 148 minutos una demostración que cierra una brecha de complejidad en optimización convexa sin derivadas que llevaba abierta desde 1996. El resultado fue verific
Este artículo explica cómo resolver el clásico problema de sincronización conocido como el puzzle de Papá Noel utilizando verificación formal mediante el model checker SPIN y el lenguaje de especificación Promela. El puzzle plantea que Papá Noel permanece dormido hasta ser despertado por los nueve r
Este ensayo examina la convergencia de dos tendencias simultáneas: la aparición de sistemas de inteligencia artificial capaces de producir matemáticas genuinas de nivel investigador, y el debilitamiento en Estados Unidos del tejido institucional que forma a las personas capaces de verificar, interpr
Un equipo de investigación presenta ESBMC-Arduino, una extensión del verificador formal ESBMC orientada a programas de autómatas programables (PLC) que se ejecutan sobre hardware abierto inspirado en Arduino, como OpenPLC, Arduino OPTA, CONTROLLINO e Industrial Shields M-Duino. La herramienta nace p
Este artículo describe un flujo de trabajo de verificación formal que toma código criptográfico Rust en producción y genera pruebas de corrección certificadas por el núcleo de Lean 4. La canalización articula tres líneas técnicas recientes en una sola cadena operativa. En primer lugar, herramientas
Kani es un verificador de modelos de código abierto diseñado para el lenguaje de programación Rust. El artículo, publicado en arXiv en julio de 2026, lo presenta como una herramienta que lleva la verificación acotada más allá de la búsqueda de errores y ofrece garantías formales de corrección. Aunqu
La empresa francesa Mistral ha presentado Leanstral 1.5, un modelo de inteligencia artificial con licencia Apache 2.0 orientado a la ingeniería de demostraciones formales en el lenguaje Lean 4. El sistema, con 119.000 millones de parámetros totales y solo 6.000 millones activos, alcanza resultados d
El equipo de dqlite en Canonical, formado por Marco Manino y Alberto Carretero, ha analizado un error de larga duración presente en el motor de base de datos SQLite desde 2010, cuya corrección se publicó en la versión 3.51.3. El fallo reside en la fase de checkpoint del modo Write Ahead Log (WAL) y,
La corrección estructural es un enfoque que modela un dominio como un grafo de nodos y aristas tipadas, donde la estructura que describe el sistema es el propio sistema. Sistemas de tipos, herramientas de construcción como Bazel, lenguajes de descripción de interfaces y bases de datos con claves for
La verificación formal permite demostrar matemáticamente que un programa cumple ciertas propiedades en todos los estados alcanzables, a diferencia del testing, que solo descarta un conjunto finito de casos. Para ello se usan lenguajes como Dafny, Lean, Rocq, Isabelle, F* o TLA+, en los que las espec
Ansatz es una librería de Clojure que permite escribir programas verificados formalmente sin salir del ecosistema de la JVM. Está construida sobre el Calculus of Inductive Constructions (CIC), la misma teoría de tipos que sustenta Lean 4, e implementa el núcleo de Lean 4 en Java. De este modo, las p
Talos es un intérprete de WebAssembly escrito en Lean 4 cuyo objetivo no es la velocidad de ejecución, sino servir como objeto formal sobre el que demostrar propiedades. La misma definición que ejecuta un programa Wasm es la que se emplea para razonar, lo que elimina la necesidad de mantener un inté
Un repositorio de GitHub ha sido publicado con una implementación formalmente verificada de un algoritmo para la intersección de polígonos, un logro significativo en el campo de la geometría computacional. El proyecto, liderado por schildep, utiliza el asistente de demostración de teoremas Lean 4 pa
ATLAS es una biblioteca masiva de matemáticas formalizadas, desarrollada por Facebook Research, que traduce libros de texto universitarios y de posgrado a código formal utilizando modelos de lenguaje grande (LLMs). Su importancia radica en acelerar el proceso de verificación matemática, permitiendo
Sostactic es una herramienta innovadora que extiende las capacidades de los sistemas de demostración de teoremas como Lean 4 para probar desigualdades polinómicas. Tradicionalmente, probar estas desigualdades en Lean ha sido limitado por tácticas como `nlinarith` y `positivity`. Sostactic supera est
Después de más de 40 años de investigación, el sistema de verificación formal conocido anteriormente como Coq Proof Assistant ha sido renombrado como Rocq Prover. Desarrollado inicialmente en 1984 por Thierry Coquand y Gérard Huet en INRIA-Rocquencourt, y posteriormente ampliado por Christine Paulin
El artículo de Kiran Gopinathan aborda un problema fundamental en el desarrollo de software con múltiples agentes impulsados por modelos de lenguaje grandes (LLMs): la coordinación. La idea predominante es que las futuras generaciones de modelos de IA, posiblemente llegando a la Inteligencia Artific
Un equipo de investigadores ha descubierto una vulnerabilidad crítica en el entorno de desarrollo Lean 4, a pesar de que una implementación de zlib (lean-zip) había sido formalmente verificada como correcta por Lean. El hallazgo, realizado por Kiran Gopinathan utilizando un agente Claude y herramien
Este artículo del blog de loskutoff.com explora el uso de Model-Based Testing (MBT) para simular y verificar el complejo sistema de combate de Dungeons & Dragons (D&D). El objetivo es ir más allá de las pruebas básicas y validar la viabilidad completa del juego, especialmente en escenarios con inter
Un investigador español, Francisco, ha desarrollado P2PCLAW, una red peer-to-peer innovadora que permite a agentes de inteligencia artificial y a investigadores compartir resultados científicos y validar afirmaciones a través de pruebas matemáticas formales. La plataforma, construida con GUN.js e IP
Mistral AI ha lanzado Leanstral, la primera base de código open-source diseñada para agentes de codificación en Lean 4. Leanstral busca abordar una limitación clave en el desarrollo de IA: la necesidad de revisión humana exhaustiva en tareas de codificación de alto riesgo. El modelo, con 6 mil millo
Un desarrollador ha presentado Aura-State, un nuevo marco de código abierto en Python diseñado para eliminar las alucinaciones y errores en los flujos de trabajo de modelos de lenguaje grandes (LLM). El marco, creado por un investigador identificado como munshi007, aborda el problema de la gestión d
Verified Spec-Driven Development (VSDD) es una metodología de ingeniería de software innovadora que combina tres enfoques probados: Spec-Driven Development (SDD), Test-Driven Development (TDD) y Verification-Driven Development (VDD). Su objetivo es crear software de alta calidad, verificable y con u
Investigadores han presentado 'Lean Collab', un nuevo sistema colaborativo para la demostración de teoremas utilizando Lean 4 y la red neuronal Ensue. La herramienta busca acelerar la verificación formal, permitiendo que múltiples agentes trabajen en la resolución de problemas matemáticos complejos