Blog / BABYLON-60
Qué comprueba Lean y qué falta comprobar al ejecutar
Una propiedad formal depende de sus definiciones y supuestos; su correspondencia con el ejecutor exige evidencia adicional.
Leer el enunciado antes del resultado
Una demostración tiene un enunciado preciso dentro de un modelo. AX0 representa estados y eventos de autorización mediante una función de transición. Para entender una propiedad de despacho hay que leer qué estados existen, qué transiciones se admiten y cómo se representa una autorización consumida. Una compilación correcta permite comprobar el desarrollo formal correspondiente; no añade al modelo recursos, fallos o actores que sus definiciones no contienen. El alcance empieza en esas definiciones.
Examinar las dependencias de la prueba
Lean permite declarar axiomas y consultar de cuáles depende un teorema. Esa auditoría importa: una hipótesis falsa puede hacer inútil una conclusión aunque el archivo compile. Conviene revisar los axiomas, los huecos de prueba y los mecanismos de evaluación usados, además de fijar la versión del compilador. La documentación de Lean explica esta base de confianza. Ninguna de estas comprobaciones constituye una medición de latencia, consumo eléctrico o comportamiento del sistema operativo.
Conectar el modelo con la implementación
El paso siguiente exige justificar qué estructuras y operaciones del programa corresponden a cada elemento del modelo. Después hay que evaluar serialización, concurrencia, persistencia y rutas de error que puedan romper esa relación. Un test dirigido aporta evidencia sobre el caso ejecutado; una campaña adversarial amplía los casos explorados. Presentar estos niveles por separado permite usar una prueba formal sin atribuirle una certificación del binario completo, del hardware o de todas las configuraciones posibles.