41 noticias
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