sel4

Un ingeniero de Google implementó un descompresor de Zstandard en Lean con pruebas formales generadas por un LLM, motivado por el altísimo costo histórico de verificar software como seL4. El experimento explora si la inteligencia artificial puede volver práctico un enfoque que hasta ahora era territorio de unos pocos equipos con presupuesto casi ilimitado.