El model checking de estados finitos —la verificación de sistemas mediante la exploración exhaustiva de todos sus estados posibles— ha sido técnicamente superado desde mediados de los años noventa por el model checking simbólico, capaz de manejar tamaños de modelo muy superiores. Sin embargo, sigue utilizándose porque cualquier ingeniero de software entiende una búsqueda en anchura o en profundidad, puede estimar el espacio de estados y ajustar su modelo cuando la explosión combinatoria lo desborda, y porque los verificadores simbólicos resultan opacos y presentan "cliffs" de rendimiento impredecibles.
El artículo examina qué papel puede desempeñar esta técnica ahora que los demostradores automáticos de teoremas, mejorados notablemente en 2026, ofrecen una nueva opción: pagar a empresas de IA por una demostración de corrección incomprensible pero, en principio, fiable. En este nuevo escenario, el autor sostiene que el model checking de estados finitos solo conservará relevancia si se aplica a la ingeniería de pruebas sobre artefactos reales, mediante pruebas basadas en modelos, validación de trazas o, sobre todo, pruebas de simulación determinista como las que ofrece Antithesis. Para que esta última opción funcione en proyectos de código abierto se necesitan cinco componentes: especificación de acciones, especificación de invariantes, control reproducible del sistema bajo prueba, capacidad de hacer instantáneas y restaurarlas, y abstracción que evite modificar el sistema. Los dos primeros los aportan lenguajes como TLA+ o Quint; los tres últimos aún no tienen solución abierta completa, salvo la emulación determinista de CPU y los hipervisores deterministas.